As for the change to the Intial Condition block I changed to what I have
read for literature over here, which is what Jacky claims is best practice.
I only switched it back to the original so that I could work from what was
original to the specifciation before moving to ProofPower and becuase since
I had moved back to working on rewriting the state properties into static
and dynamic areas, I had forgotten the discussion of why we switched to
using the prime on the State variable name in the Init operation. It is
quite an easy change back, so I will more for the reason, as you have
mentioned, I rather be consistent with what Spivey and Woodcock have done
over say Jacky.

This brings me to the next point. I realized from the output we had
switched to a horizontal schema notation, as for work I had seen in my
readings and from the other outputs I had worked with, but I thought
the braces around the schema replacement were of some consequence. It
sounds like from your account that they are just there for sanity purposes
and should look at it like I did any other variable in the previous proofs
and just provide proper witness to the system to show the proof. I assume I
acheive this by using the "there_exists" tactic like I have on the other
existance proofs I have shown.

The other question I have is is there any harm, or looking at it the other
way any need, to use the precondition proof on intialization operations if
I am using an existance proof already? The reason I was going with the
precondition proofs as my starting base was because they were the proofs
that were used in your example specification in the paper that is on the
ProofPower site.

As for your final point, you are quite correct in that the specification I
have written is a functional specification describing what the system must
accomplish, but not how those objectives can be accomplished, that is what
I was intending for code. Essentially this specification document was
constructed from a set of requirements, so a requirements specification,
from a customer, and I took those and constructed this specification to
describe what the elevator must do to meet the needs of the customer. As
for the question about certain aspects of the elevator, making sure all
floors in a direction serviced, or you are able to get off, I think I could
see a way, possibly, to state this in a schema notation, but in proving
such a claim I am not sure on. My idea of using the schema may be incorrect
as well.


On Tue, Oct 16, 2012 at 4:21 AM, Roger Bishop Jones <> wrote:

> 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

Reply via email to