I tried adding the exclamation point to the end of the pushed' line, but if
gave me a paser error saying free types here not allowed. I have provided
exactly the what the paragraph looked like I tried to parse and the error
that was reported in the errorEncountered document.

I went back to just having the two exclamation points on pushed and
Button_State, in the predicate and declaration section of the schema box
respectively, and this generated a monster of subgoals when I tried the
provided proof strategy. Obviously there should not be that much to prove,
especially when everything is the same, except for push just being set to
the empty set. I have also gone back and reviewed Jacky's "The Way of Zed"
and he uses the delta operator to signify there are changes being made to
the states, though he never discusses initialization, but there appears to
be some disconnect between the authors, though I know Spivey and Woodcock
should probably be followed so I like to stick with what they say is best

As for the Init and State blocks that I am trying to and have proven,
should there be a change there so that the proof is not of precondition but
of consistency? As you have mentioned, and I have agreed with, it is really
pointless to do the precondition proofs for the states when they are static
and not changing, everything remains the same, and they are only showing
the information provided is consistent.


On Sat, Sep 22, 2012 at 4:07 AM, Roger Bishop Jones <> wrote:

> Jon,
> On Saturday 22 Sep 2012 00:11, Jon Lockhart wrote:
> > I tried what you mentioned after Phil brought it up and
> > if you try to do State' and then push' = {} the system
> > throws an error saying "No free types allowed in
> > predicates" which to me means that push is not
> > accessible in the predicate section.
> Should be pushed'={}!
> 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