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
where you currently have
  Δ State

I strongly recommend reading chapter 12 of Using Z, available at

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!


Proofpower mailing list

Reply via email to