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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 17 Dec 2014 09:59:38 -0800 (PST)*References*: <212fbe7b-b820-4387-add1-d0556bbca058@googlegroups.com>

iflbl:

if FEOF(x) = EOF

then

ret := 0;

goto endlbl;

end if

endiflbl:

ret := 1

endlbl: <---- Here is the problem

end algorithm

You can simply replace "goto endlbl" by "goto Done" and

remove the bogus label "endlbl".

remove the bogus label "endlbl".

----

For such a simple case your proposed condition can equivalently be

replaced by a set-valued initialization such as variable p \in

ValidPointer

It depends what you mean by the predicate VALIDPOINTER. It might be

more complex. Or more generally, it might be a predicate with no

meaning declared by a constant and intended to be used with an opaque

data

If VALIDPOINTER is a constant _expression_, then it makes no sense to

make it a precondition. It should be asserted in the TLA+ module

with an ASSUME. If VALIDPOINTER(p) is an arbitrary predicate, for

example,

VALIDPOINTER(p) == \E S : p = SUBSET S

and you want to write

variable p ;

precondition VALIDPOINTER(p)

then I'm sorry, PlusCal is not the language for you; you'll have to

write it in TLA+. There are many more interesting specs that can be

written in TLA+ and are difficult or practically impossible to write

in PlusCal. (And, as in this case, can't be checked by TLC.)

On the other hand, if you want to write

VALIDPOINTER(p) ==

\E m, n \in Nat : IsPrime(m) /\ IsPrime(n) /\ p = m + n

then, as Stephan pointed out, you can easily write

variable p \in {i \in Nat : VALIDPOINTER(i)}

**Follow-Ups**:**Re: End labels***From:*fl

**References**:**End labels***From:*fl

- Prev by Date:
**Re: [tlaplus] End labels** - Next by Date:
**Re: End labels** - Previous by thread:
**Re: [tlaplus] End labels** - Next by thread:
**Re: End labels** - Index(es):