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

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

Appreciate all your help in this matter.


On Sun, Oct 14, 2012 at 4:07 AM, Roger Bishop Jones <> 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

Attachment: elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data

Attachment: errorEncountered.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to