Re: [ProofPower] Initialisation convention

2012-09-23 Thread Phil Clayton 

On 22/09/12 10:45, Roger Bishop Jones wrote:

I see that Potter Sinclair and Till An Introduction to
Formal Specification Using Z 1991 use the primed version of
the convention, and offer the following rationale (p43):

Here we use Vocab' as the variable to suggest that
initialisation is like an operation which produces after
objects which are acceptable as starting values for the
persistent objects of the system.
Admittedly in this very simple case this seems a complicated
way of saying that the system must start with an empty
vocabulary.

(but note that they did not actually use an operation, the
initial state is defined as a bare after-state).

Possibly the priming of initial state began here.


By making initialization an operation without a before state, the 
initialization can be used with schema operators such as composition and 
pre, e.g.


  Init ⨟ Op

  pre Init

the latter being another way to write the following:
  ∃ Init ∙ true
  ∃ State' ∙ Init

Phil


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Initialisation convention

2012-09-23 Thread Roger Bishop Jones 
Phil,

On Sunday 23 Sep 2012 21:11, Phil Clayton wrote:

 By making initialization an operation without a before
 state, the initialization can be used with schema
 operators such as composition and pre, e.g.
 
Init ⨟ Op
 
pre Init
 
 the latter being another way to write the following:
∃ Init ∙ true
∃ State' ∙ Init

That had occurred to me.
But it didn't seem to me a particularly good idea.

One could generally state the non-emptyness of some schema S 
as pre S', but surely its clearer to say ∃ S ∙ true.
(and Init /\ Op does the same under Spivey's convention as  
Init ⨟ Op under the other).

There doesn't seem to be much to chose between them.

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

2012-09-23 Thread Jon Lockhart 
Roger,

I tried adding the exclamation point to the end of the pushed' line, but if
gave me a paser error saying free types here not allowed. I have provided
exactly the what the paragraph looked like I tried to parse and the error
that was reported in the errorEncountered document.

I went back to just having the two exclamation points on pushed and
Button_State, in the predicate and declaration section of the schema box
respectively, and this generated a monster of subgoals when I tried the
provided proof strategy. Obviously there should not be that much to prove,
especially when everything is the same, except for push just being set to
the empty set. I have also gone back and reviewed Jacky's The Way of Zed
and he uses the delta operator to signify there are changes being made to
the states, though he never discusses initialization, but there appears to
be some disconnect between the authors, though I know Spivey and Woodcock
should probably be followed so I like to stick with what they say is best
practice.

As for the Init and State blocks that I am trying to and have proven,
should there be a change there so that the proof is not of precondition but
of consistency? As you have mentioned, and I have agreed with, it is really
pointless to do the precondition proofs for the states when they are static
and not changing, everything remains the same, and they are only showing
the information provided is consistent.

Thanks,
Jon


On Sat, Sep 22, 2012 at 4:07 AM, Roger Bishop Jones r...@rbjones.com wrote:

 Jon,

 On Saturday 22 Sep 2012 00:11, Jon Lockhart wrote:

  I tried what you mentioned after Phil brought it up and
  if you try to do State' and then push' = {} the system
  throws an error saying No free types allowed in
  predicates which to me means that push is not
  accessible in the predicate section.

 Should be pushed'={}!

 Roger



elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data


errorEncountered.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com