# Re: [ProofPower] Trying to Prove my Zed Specifications

```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

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?
>>
>
> 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
```