Roger, Thank you for getting back to me. I will certainly look into using the "axiomatic" block in Z similar to the structure found in the Vending Machine example. It may take me a little to figure out how to structure it appropriately. I will dicuss this concept with my advisers and see what we can come up with. If I run into any troubles or road blocks I will be certain to post them here to get people's thoughts.
Regards, Jon On Mon, Nov 12, 2012 at 4:19 AM, Roger Bishop Jones <r...@rbjones.com> wrote: > Jon, > > > Now I am on to another portion of the same specification > > which I am having difficulty with. I believe it is > > simaliar to the Vending Machine example where it is > > shown that the Vending Machine doesn't undercharge. What > > I would like to show is things like, from Up and Down > > you can only get to Countdown or Stop, from Stop you can > > only go to Up or Down, etc. So these would honestly be > > operation transistions. > > > Is an axiom the best way to > > handle this like in the Vending Machine example? Is > > there a better way you could see for this? > > I hope you mean an "axiomatic specification" of the required > condition rather than an axiom. > (which since you are not using axiomatic mode doesn't get > translated into an axiom). > You are here just defining the condition you want to prove. > > This is as you say, the procedure adopted in the Vending > Machine example, and should be OK in your application. > > Then you just set your goal using this newly defined concept > (whatever it is) and go about its proof. > > Roger >
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
