Well I will look into those further steps and dicuss the options with my
advisor as soon as I finish my work on the operations I have.

I am having trouble proving these operations now, starting with the first
one. I am using the precondition proof, and I believe I have set it up
correctly, and I get to a single subgoal and I now need to do an existance
proof, but I can't seem to write the write tactic to show all that was left
behind. Any suggestions on what I would need to ask to complete the goal?

I believe I should also switch in the operation the states to have primes
rather than deltas correct?

File is attached.


On Thu, Oct 18, 2012 at 5:46 PM, Roger Bishop Jones <> wrote:

> On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote:
> > After fixing the correction you pointed out, I was able
> > to get the existance proofs completed and I removed the
> > precondition proofs for those init operations. You can
> > see this in the attached specification file.
> You are now using after states for initial conditions, so an
> existential is the best way to express the consistency of
> these conditions.
> However, you are including extra undecorated components in
> some of the initial state schemas, and I am not aware of a
> precedent for this.
> Its not clear what this is intended to mean.
> I suspect that these names might possibly be better as
> global variables than as local to the initial state schemas,
> but it depends what you are intending to say here.
> > Now this
> > brings up a previous question again, along with a new
> > one. 1) Is it necessary to have the precondtion proofs
> > with the exsistance proofs in the specification? If not
> > necessary is it wise to use both, or are both redundant
> > in terms of what they are showing and not necessary?
> Not necessary for the initial state.
> > 2)
> > I am now on to the first main operation of the
> > specification, and I have a precondition proof outlined,
> > albeit some changes are required of it, to begin proving
> > properties of said operation. Should I stick with the
> > precondition proof for this and the other opertations or
> > is there another proof I should be using? What other
> > proofs just on the operations should I be looking to
> > use?
> Precondition proofs are simply a consistency check.
> They tell you when the operations have a result.
> I have already made some suggestions about what other kinds
> of thing you might want to prove.
> Generally proofs may be used either to validate your
> specification (ideally against some other more abstract
> specification), or to validate code against the specification,
> or to validate refinement steps which add more detail or move
> the spec closer to the code.
> Which of these you do is up to you or to you customers.
> Roger

Attachment: elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to