Roger, Understood, I will make sure to keep all that in mind when I working on the precondition proofs for the operations. The proof could was skeletoned in when I was working on the earlier material b/c I thought it would make things easier when I was able to return to the operations, but since changes have been made that altered the amount of information necessary in those proofs, I certainly need to rewrite them and massage them.
I guess I didn't quite understand or comprehend properly the second point you were trying to make. I inserted an existance proof like I had done for the state schemas and I unfortunately get a very interesting goal after the rewrite, as seen in the error zip attached. This makes me wonder if it would be better to attempt to use the precondition proof code found underneath the start of the existance proof for trying to prove properties about the init operations, and then further of course into the system opertaions. The second question I have is a more general one, and this may be difficult to answer since I am still green at proving properties of formal specifications. Say for example I do the precondition proofs and those all work out. What else can we say about the operations in this system before we exhaust the possibilities and I move on to coding, and verification there. Appreciate all your help in this matter. Thanks, Jon On Sun, Oct 14, 2012 at 4:07 AM, Roger Bishop Jones <r...@rbjones.com> wrote: > Jon, > > On Sunday 14 Oct 2012 04:52, you wrote: > > > Any direction on how to finish these up so I may move on > > to the actual operations would be greatly appreciated. > > Two points to keep in mind. > > First, ProofPower does not automatically rewrite with any of > the specifications which you have put in, you have to tell it > which you want it to rewrite with, and in your remaining > precondition proofs there are more specifications which you > have to include in the rewrite. > It is possible to make a proof context which expands the > default set of rewrites, but at this stage you are probably > better just using cut and paste on the lists of global > variable names used in the rewrites. > > Second, when proving the non-emptyness of a schema, as in > the initial conditions, you have to think of the schema as a > set of bindings, consider the conditions which you have > placed on which bindings belong to the schema, and then > think of a way of writing down a binding which can be proven > to satisfy the conditions. > That will be your witness, then you just have to do the > proof. > Again, make sure you rewrite with everything you need to > use. > > Roger >
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
errorEncountered.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
