On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote: > After fixing the correction you pointed out, I was able > to get the existance proofs completed and I removed the > precondition proofs for those init operations. You can > see this in the attached specification file.
You are now using after states for initial conditions, so an existential is the best way to express the consistency of these conditions. However, you are including extra undecorated components in some of the initial state schemas, and I am not aware of a precedent for this. Its not clear what this is intended to mean. I suspect that these names might possibly be better as global variables than as local to the initial state schemas, but it depends what you are intending to say here. > Now this > brings up a previous question again, along with a new > one. 1) Is it necessary to have the precondtion proofs > with the exsistance proofs in the specification? If not > necessary is it wise to use both, or are both redundant > in terms of what they are showing and not necessary? Not necessary for the initial state. > 2) > I am now on to the first main operation of the > specification, and I have a precondition proof outlined, > albeit some changes are required of it, to begin proving > properties of said operation. Should I stick with the > precondition proof for this and the other opertations or > is there another proof I should be using? What other > proofs just on the operations should I be looking to > use? Precondition proofs are simply a consistency check. They tell you when the operations have a result. I have already made some suggestions about what other kinds of thing you might want to prove. Generally proofs may be used either to validate your specification (ideally against some other more abstract specification), or to validate code against the specification, or to validate refinement steps which add more detail or move the spec closer to the code. Which of these you do is up to you or to you customers. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
