On Tuesday 16 Oct 2012 01:12, Jon Lockhart wrote:

> I guess I didn't quite understand or comprehend properly
> the second point you were trying to make. I inserted an
> existance proof like I had done for the state schemas
> and I unfortunately get a very interesting goal after
> the rewrite, as seen in the error zip attached.

The point I was making was very elementary, so you probably 
already understood it.
I didn't have a specific issue to address and you had already 
made a mistake in choice of witness so I thought I would 
start there.

Your present example illustrates what happens when you 
rewrite with the definition of a schema.
The first thing that happens is that the schema name is 
replaced by the horizontal schema corresponding to the 
Often the context allows this to be eliminated, typically in 
favour of the predicate obtained from the declaration and 
body parts of the schema, but in some cases as in the 
declaration part of your existential, this is not possible.

It is better when you have an existential goal to supply a 
witness before you rewrite.
When you supply the witness the declaration part disappears 
and the witness is asserted to belong to the schema. In this 
context when you rewrite with the schema definition it is 
possible to eliminate the horizontal schema.

It is not essential to supply the witness first, but if you 
don't you are likely to see these unfamiliar expressions in 
which horizontal schemas are used.

I see that you are using operations for initial conditions 
rather than following either Spivey or Woodcock with a 
before or an after state respectively.
(I don't know a reason why not, except that you are more 
likely to get comments along the lines "that's not how you 
specify initial conditions").

> This
> makes me wonder if it would be better to attempt to use
> the precondition proof code found underneath the start
> of the existance proof for trying to prove properties
> about the init operations, and then further of course
> into the system opertaions.

If you are using an operation to specify the initial 
conditions, then the consistency of your initial conditions 
is equivalent to the assertionj that the precondition of the 
operation is the before state, in this case

        pre Button_Init <=> Button_State

The existential form was recommended for the case that you 
were specifying the initial condition not as an operation
(a delta Button_state) but as a before state (a 
Button_State) or an after state (a Button_State').
However, the existential proof you have started is perfectly 
OK, you just have to carry it through without being phased 
by horizontal schemas.

> The second question I have is a more general one, and
> this may be difficult to answer since I am still green
> at proving properties of formal specifications. Say for
> example I do the precondition proofs and those all work
> out. What else can we say about the operations in this
> system before we exhaust the possibilities and I move on
> to coding, and verification there.

Before proceeding to implementation you would want to verify 
that the system as specified has the most important of the 
properties which you would expect of it.

Think of the difference between a specification of the system, 
and a specification of the requirements which the system must 

You don't have what I would call a "requirements" 
specification, you have a functional specification.
The kind of thing a requirements specification might say is 
that every request for a lift is eventually honoured, and 
that when you get in the lift you are eventually let out on 
the floor you requested.
Can you see how to state and prove such claims?

Roger Jones

Proofpower mailing list

Reply via email to