Community,

After some discussion with my advisors, and after taking a hard look at the
project we are trying to apply Zed and its proofs too, we came to the
conclusion that we did not need something as complicated as the original
controller I was working on. Though showing the great depth in what the
language could accomplish, it was really beyond what we need. I am still
working on it though so that I can refine it to be simplier and still fit
all the necessary information in.

In any case I have constructed a newer, much simpler specification, using
the Vending Machine example from the Zed tutorial. This was much closer to
our needs, though I wanted to work with my elevator as a learning process
in application from what I had learned form the Vending Machine. I get to a
great point, but then I seem to be stuck, and I can't seem to give the
right LEMMA_T insertion to get the system to solve the last 3 pieces of the
conclusion. I have spent a good while on subtle rewrites and reordering
with no success. I have attached the file for convinence. Any assistance in
some quick things to alliviate the isue I am having would be greatly
appreciated.

File is attached.

Regards,
Jon Lockhart
On Mon, Oct 22, 2012 at 12:49 PM, Jon Lockhart <jal...@bucknell.edu> wrote:

> 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: newElevatorSpec.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