> 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
> TLC would not be able to evaluate arbitrary predicates appearing in preconditions.
Yes its true. But it is to be used with tlaps. And with tlaps I think it might be very helpful. But
it's true if such a clause were added to PlusCal it should be reported that it doesn't work with
TLC so that users are not misled.
--
FL