iflbl:
if FEOF(x) = EOF
then
ret := 0;
goto endlbl;
end if
endiflbl:
ret := 1
endlbl: <---- Here is the problem
end algorithm
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)}