> Sure but I don't like using PluCal procedure because you need to manage the stack in your proof then and it is
> boring. I have just come across the Skip _expression_. I will try if we can use it for the discussed purpose.
Yes it works. But it adds an extra state. One might think about a false label called "done:" that would be merged
with the "Done" state. (I say that in case somebody wants to make changes to PlusCal, that's all.)
Another clause that I would add to PlusCal is the clause "precondition" because the clause "variable" is not
enough.
For instance if we had:
--algorithm test
variable v = 0
precondition VALIDPOINTER(p)
etc.
we would have the translation:
Init ==
/\ v = 0
/\ VALIDPOINTER(p)
--
FL