[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] End labels

> 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
For instance if we had:
--algorithm test
variable v = 0
precondition VALIDPOINTER(p)
we would have the translation:
Init ==
  /\ v = 0