Re: [ProofPower] Trying to Prove my Zed Specifications
Roger,
Well based on what you have just told me, I would feel that my Init
paragraphs that I have written are a form of Operation. When the system is
initialized these should be the first set of operations that are run to
make sure the subsets of consequence are set to the proper starting
parameters. The others we do not care what there values are initialized to
and are hence not in the Init paragraphs. 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?
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?
Regards,
Jon
On Thu, Sep 20, 2012 at 9:59 AM, Roger Bishop Jones
rogerbishopjo...@btinternet.com wrote:
Jon,
On Wednesday 19 Sep 2012 22:26, Jon Lockhart wrote:
I thought that might come up, the idea that I missed
pushed = {}. Since this is describing an initialization
section for the system, would pushed = {} need to be a
precondition? What I mean is is that when the subset
pushed is created or generated, the system may very well
fill it with garbage, but when the system initializes
pushed must be set to the empty set. Does this then
still need to be a precondition or does this become just
a by product I have to prove of showing the
preconditions of the init operation?
The precondition operator is really only relevant to schemas
which are operations, i.e. in which there is a before and
after state and possibly some outputs.
i.e. in which there are components ending ' and possibly
some ending with ?
When applied to such a schema the precondition operator
tells you essentially the domain of the operation, i.e. all
the possible combinations of before state and input
variables (and actually any other junk) under which some
possible after state and output values are specified.
The initial state is not an operation, its just a state, so
the notion of precondition is not really applicable.
When you apply the precondition operator to a schema it
obtains its result by existentially quantifying over the new
state and output components.
If there are none, then this has no effect.
This explains why pushed={} is in your precondition.
You can find a description of the Pre operation in the
ProofPower-Z reference manual in the section on schema
expressions.
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
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
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
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.netwrote:
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.**comhttp://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
