Jon,
On Sunday 23 Sep 2012 22:32, Jon Lockhart wrote:
> 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.
The perils of not carefully quoting!
The exclamation mark was not intended to be in the formal
text, it was just my exclamation.
The point I was making was just that you had said "push'={}"
and it should have been "pushed'={}"!
> 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.
Should be "pushed"!
Make sure you have no occurrences of "push" and if you still
have a problem with the proof post it.
> 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 practice.
I don't have access to Jacky's book so I can't comment.
> 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.
Yes, try proving:
∃ Init ∙ true
and
∃ State ∙ true
Both should be trivial proofs.
Roger
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
