Re: [ProofPower] Trying to Prove my Zed Specifications
> > Roger, > > Thanks, I overlooked the symbol I had used, I appreciate that, that > cleared the proof right up. > > Any thoughts on my email before those? > > Regards, > Jon > On Wed, Oct 17, 2012 at 2:21 AM, Roger Bishop Jones wrote: > >> On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: >> >> > Attached is my latest attempt. With both the delta >> > operator and priming Button_State, with the existance >> > and precondition proof, I run into a wall. I get close, >> > but can't seem to give it the right witness to solve >> > this simple init operation. >> >> The binding display for your witness uses "=" but should use >> "=^" (equal with hat). >> >> 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
Re: [ProofPower] Trying to Prove my Zed Specifications
Roger, 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. 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? 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? Regards, Jon On Wed, Oct 17, 2012 at 1:16 PM, Jon Lockhart wrote: > Roger, > > Thanks, I overlooked the symbol I had used, I appreciate that, that > cleared the proof right up. > > Any thoughts on my email before those? > > Regards, > Jon > On Wed, Oct 17, 2012 at 2:21 AM, Roger Bishop Jones wrote: > >> On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: >> >> > Attached is my latest attempt. With both the delta >> > operator and priming Button_State, with the existance >> > and precondition proof, I run into a wall. I get close, >> > but can't seem to give it the right witness to solve >> > this simple init operation. >> >> The binding display for your witness uses "=" but should use >> "=^" (equal with hat). >> >> Roger >> > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
Roger, Thanks, I overlooked the symbol I had used, I appreciate that, that cleared the proof right up. Any thoughts on my email before those? Regards, Jon On Wed, Oct 17, 2012 at 2:21 AM, Roger Bishop Jones wrote: > On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: > > > Attached is my latest attempt. With both the delta > > operator and priming Button_State, with the existance > > and precondition proof, I run into a wall. I get close, > > but can't seem to give it the right witness to solve > > this simple init operation. > > The binding display for your witness uses "=" but should use > "=^" (equal with hat). > > Roger > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
