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 > > > > > > >
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
