# Re: End labels

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".

----

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)}