Roger,
Thanks for the help and the info. After your explanation I better
understand what you are saying and I do agree with the point you are trying
to make. I will have to look into that further.
Phil,
Thank you for the insight and help. From the book, examples, and papers I
have read, I was developing my specification on what they had done and said
was best practice in Zed. I do agree that proving the state declaration
when there was no change was odd, but that is what other had done and that
is just what I stuck with.
I do like the idea of changing the pushed to a pushed' and thinking of the
Init as an operation, but I am more curious as to why we are placing the
prime on the entire state, when we are just operating on a member of the
state? The delta should signify based on the Zed notation that a change is
occurring to the state, but it doesn't mean that that whole state has to
change. I am just thinking that placing the prime on the whole state may
affect what I am trying to say in the Init operation, if that makes sense.
If you be willing to provide further assistance and clarification as I make
adjustments that be great.
Also, I appreciate the book link. I will def take a look at it and probably
add it to the Zed book I already have, "The Way of Zed".
Thanks,
Jon Lockhart
On Thu, Sep 20, 2012 at 4:10 PM, Phil Clayton <phil.clay...@lineone.net>wrote:
> 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<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>
>
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
