Community,

I am having trouble proving my 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?

File is attached.

Regards,
Jon Lockhart

---------- Forwarded message ----------
From: Jon Lockhart <jal...@bucknell.edu>
Date: Sun, Oct 21, 2012 at 6:29 PM
Subject: Re: [ProofPower] Trying to Prove my Zed Specifications
To: Roger Bishop Jones <r...@rbjones.com>
Cc: ProofPower List <proofpower@lemma-one.com>


Roger,

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.

Regards,
Jon


On Thu, Oct 18, 2012 at 5:46 PM, Roger Bishop Jones <r...@rbjones.com> 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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to