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.

## Advertising

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