Jon,
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
definition.
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
meet.
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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
