5.4. Allocated and fresh🔗

fresh(e) is a predicate that holds when the reference e was newly allocated by the current procedure — it did not exist in the heap on entry. It is the standard way to tell a caller that a returned reference cannot alias any object that already existed, which is what rules out aliasing between the result and the caller's pre-existing objects.

composite Node { var next: Node }

procedure allocate() returns (r: Node)
  opaque
  ensures fresh(r)
{
  r := new Node
};

fresh(e) may only target reference (composite) types. Its planned dual, allocated(e) — asserting that a reference already existed in the current state — has not been implemented yet. See the Aliasing helpers section of the Laurel Design Guide for the underlying model of allocation and how these two notions relate.