Jon,
On 20/09/12 17:59, Jon Lockhart wrote:
So based on what you have
said does that mean then that pushed = {} should be changed to pushed' =
{} since it would be a consequence of the Init operation running at
start up?
I had a quick read yesterday but no time to reply. My initial reaction
was you meant pushed' = {}.
However, for initialization, you don't have an initial state, so your
schema should just have
State'
where you currently have
Δ State
I strongly recommend reading chapter 12 of Using Z, available at
http://www.usingz.com/
If this change is necessary, and of course I will apply it to the other
two init operations, would the pre operator then be more useful in being
applied to this operation?
pre Init is certainly worth establishing: it is useful to know whether
the Init operation can be achieved. Note that with the above change to
use State', pre Init is either true or false as there are no unprimed
variables. You want to know that it is not false. As there is no
initial state, pre Init may be written
∃ State' ∙ Init
However, I see you're calculating
pre Button_State
pre Elevator_State
pre Floor_State
which is pointless. These schemas are not operations: they have no
concept of before state and after state. You'll see that none have
primed variables. Not surprisingly, you're finding
pre X_State = X_State
I also recommend chapter 14 of Using Z. The whole book is worth a read,
in fact!
Phil
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
