feat: Introduce :older attribute

[RustanLeino]

This PR introduces a new parameter modifier, older, which can be used with the parameters of a predicate to say that, if the predicate returns true, then the parameters declared as older are necessarily equally old as or older than the other parameters.

The updated reference manual contains a section that motivates and describes older. That's the text aimed at users. Here is a smaller--but not terribly motivated--example, along with an implementation-centric explanation:

For a predicate

predicate P(older x: X, y: Y)

the older modifier claims

forall h: Heap :: IsAlloc(y, h) && P(x, y) ==> IsAlloc(x, h)

That is, if the predicate returns true, then in any heap where y is allocated, then so is x --- in short, x is older than y.

The reason for wanting to declare a predicate with older parameters is so that the predicate can be used as a way to ensure a quantified expression does not depend on the allocation state. For example,

function F(y: Y): int {
  if forall x: X :: P(x, y) ==> G(x, y) == 3 then
    100
  else
    0
}

Here is another example, using an iset comprehension:

function Collection(y: Y): iset<X> {
  iset x: X | P(x, y)
}

Dafny does not allow a function to depend on the allocation state; that is, the act of allocating more objects should not change the value of a function. But if X is a type that contains references, then, at first glance, it looks as if this function does depend on the allocation state. For instance, if X is a class type, then allocating more X objects gives more candidate values for the iset comprehension to consider, and if those X objects satisfy the P constraint, then the iset would become larger. By using the older modifier on P's parameter x, it becomes known that any x that satisfies P(x, y) in this comprehension is older than y. Thus, the iset comprehension, in fact, does not depend on the allocation state.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

Do I understand correctly that using {:older}, a Dafny user can write

predicate {:older x} P(x: X, y: Y) {
 .. body ..
}

instead of

predicate P(x: X, y: Y) 
  ensures forall h: Heap :: IsAlloc(y, h) && P(x, y) ==> IsAlloc(x, h)
{
 .. body ..
}

Or is that not possible because Heap and IsAlloc are not accessible in user space? Would it be an option to make those accessible in certain circumstances? And if Heap and IsAlloc are available, could there be library functions that do something similar to {:older} ?

---

How often do we expect {:older} to be used? Can you give some indication of how the cost vs benefit of having this attribute? I'm sure I'm missing all the context for this PR so sorry for that.

Also would it be possible to implement this change are purely an extension to the Dafny compiler, with all the code being in a separate file? Given that it's adding an attribute that seems like it should not be a problem. I think that having the code not be intertwined with the existing code would lower the cost of having it by a lot.

[robin-aws]

+1 to @keyboardDrummer's questions - I get the motivation of being able to ensure a pure expression does not depend on future allocations, but I'm definitely not convinced this feature is the best way to deliver that functionality.

[keyboardDrummer]

The reason for wanting to declare a predicate with :older is so that the predicate can be used as a way to ensure a quantified expression does not depend on the allocation state.

Would it also be possible to use reads clauses to indicate this? Something like:

function F(y: Y): int
 reads <things older than y, or maybe things accessible from y?> {
  if forall x: X :: G(x, y) == 3 then
    100
  else
    0
}

[RustanLeino]

Here are two cryptic answers to questions brought up above:

• IsAlloc and Heap refer to things in the internal encoding of Dafny into Boogie. They are not available directly to Dafny programmers.
• It's not possible to encode the situation using Dafny's current reads clauses.

To understand the situation better, let me write down the motivation. (please stand by)

[RustanLeino]

Motivation

Let me lead up to the motivation, starting with some background information about memory safety, references, quantifiers, and functions.

Quantifications implicitly quantify over allocated state

Dafny is a memory-safe programming language. Consequently, every object reference is either null or points to an allocated object. In other words, every reference (pointer) is valid. There is no way for a program to get hold of a pointer to un-allocated memory.

This property should carry over to comprehensions and quantifications as well. (Everything I'll say about quantifications applies to comprehensions in general; for example, set comprehensions. But I'll just say "quantifications" to stay more focused.) So, in Dafny, if C is an object type, then

forall c: C :: ...

quantifies over all references to allocated C objects.

What I said applies not just to object types, but to any type that contains a reference. For example, given

datatype List<T> = Nil | Cons(T, List<T>)

the type List<int> does not contain references, but the type List<C> does (where C is an object type). So, a quantification

forall cs: List<C> :: ...

quantifies over all lists whose every C reference is allocated.

Functions are not allowed to depend on the allocation state

Consider the following attempted program:

class Cell {
  const data: int
  constructor (x: int) {
    this.data := x;
  }
}

function P() {
  forall cell: Cell :: c.data == 10 // Dafny does not allow this quantifier in a function
}

method M() returns (c: Cell)
  requires P()
  ensures P()
{
  c := new Cell(8);
}

It would be bad if this program would verify, because P does not hold at the end of M. (You might also reasonably ask how any program can live up to the precondition of M. I don't know of such a way. But P() does hold in some possible program states, so we do want to make sure M ensures its postcondition given its precondition.)

If a function were allowed to depend on the allocation state (like the attempted P does above), then any object allocation could potentially change the value returned by the function. This would make it difficult to specify and verify programs, especially considering that any method is allowed to allocate new objects.

Instead, Dafny bans quantification over any reference-containing type in function bodies. Thus, Dafny rejects the program above. The check is enforced syntactically by the resolver--even before the program gets to the verifier.

Allowing some quantifications over reference-containing types

There are cases where Dafny's ban of quantifications over reference-containing types (henceforth called The Ban) is too strict. For example, suppose you want to define a predicate that says a given relation is transitive. You might write:

predicate Transitive<X>(R: (X, X) -> bool) {
  forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) // Dafny does not allow this quantifier in a function
}

Alas, The Ban forbids the predicate, since it may be that type X contains reference. You are, however, allowed to write this predicate if you restrict the type parameter X to types that do not contain references. This is expressed by the somewhat cryptic-looking (!new) type characteristic:

predicate Transitive<X(!new)>(R: (X, X) -> bool) {
  forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z) // since X is declared with (!new), the quantification is allowed
}

Allowing more quantifications

Dafny's syntactic check that enforces The Ban is not quite as strict as I've described it. It allows quantifications if the bound variables are limited to things that are allocated already. For example, you are allowed to write

predicate Transitive<X>(R: (X, X) -> bool, universe: set<X>) {
  forall x, y, z ::
    x in universe && y in universe && z in universe ==>
    R(x, y) && R(y, z) ==> R(x, z)
}

(note the absence of (!new) in this definition). The justification for allowing this quantifier in a function is, roughly speaking, that x, y, and z range over values that are necessarily allocated. More precisely, the fact that x, y, and z are allocated follows from the fact that the parameter universe is allocated. This means that the following program snippet always verifies:

var b0 := Transitive(R, U);
var c := new Cell(8);
var b1 := Transitive(R, U);
assert b0 == b1;

Stated differently, Transitive(R, U) does not depend on any object allocated after the allocation state of U. In other words, x, y, and z range over values that are allocated before U. That is, x, y, and z are older (in the allocation-state order) than U.

User-declared "older" relations

Here is a simple, typical quantification that is allowed in a function:

predicate AllZeros(S: set<Cell>) {
  forall c :: c in S ==> c.data == 0
}

As I mentioned above, the syntactic scan performed by the enforcement of The Ban detects the expression c in S in the antecedent of the quantifier, and this shows that c is "older" than parameter S, and therefore the quantification is allowed.

But what if you wanted to write the expression c in S in another function? For example, what if you wrote the following?

predicate AllZeros(S: set<Cell>) {
  forall c :: InMySet(c, S) ==> c.data == 0
}

predicate InMySet(c: Cell, S: set<Cell>) {
  c in S
}

This is not allowed, because the syntactic check performed by The Ban doesn't trace through the call to InMySet.

This PR introduces an attribute that lets The Ban understand user-defined predicates as ones that ensure something about "older". The idea is that you declare InMySet as

predicate {:older c} InMySet(c: Cell, S: set<Cell>) {
  c in S
}

which expresses that

InMySet(c, S) implies that c is older than S. (*)

This PR introduces the {:older} attribute and adds the semantic check that (*) holds. It also changes The Ban to look for {:older} attributes. So, with this PR, the updated InMySet above allows the AllZeros predicate.

Note that this design lets The Ban remain a syntactic check (it looks for the {:older} attribute), whereas the meaning of {:older} is enforced by the verifier.

Why bother?

Predicate InMySet above is too simple to motivate the effort of supporting {:older}. Here is an example (originally from Test/dafny1/SchorrWaite.dfy, and also included in this PR as Test/dafny0/OlderVerification.dfy) that could not be done without {:older}:

class Node {
  var children: seq<Node>
}

datatype Path<T> = Empty | Extend(Path, T)

predicate Reachable(source: Node, sink: Node, S: set<Node>)
  reads S
{
  exists via: Path<Node> :: ReachableVia(source, via, sink, S) // allowed because of {:older p} on ReachableVia
}

predicate {:older p} ReachableVia(source: Node, p: Path<Node>, sink: Node, S: set<Node>)
  reads S
  decreases p
{
  match p
  case Empty => source == sink
  case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)
}

Since Node is a class type, Path<Node> is a reference-containing type. Therefore, The Ban will scrutinize the quantifier in Reachable. Bound variable via is passed in as parameter p to ReachableVia. Since ReachableVia is declared with {:older p}, The Ban is satisfied that the quantification in Reachable does not depend on the allocation state.

A final note: If this was a problem in Test/dafny1/SchorrWaite.dfy, how come the Schorr-Waite program has been in the test suite for 10 years without needing {:older}? Because of bug #1419, which is being fixed in PR #1924. The fix depends on this PR in order for the test suite to go through.

[keyboardDrummer]

Thanks for the great explanation. It helps a lot. That said though, I'm still not confident about any thoughts I have on this topic, but I'll share them anyways. Please bear with me.

Quantifications implicitly quantify over allocated state

Is that to make the proofs more tractable?

What if quantifications also implicitly quantify over readable state? In your example, Reachable already specifies reads S. Can't that mean that the instances of via in exists via: Path<Node> are limited to those containing references from S ?

Or differently, shouldn't quantifier variables always be older than the parameters of the function containing the quantifier? Why do I still need to specify an older annotation?

---

In your example, the n in S in

case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)

already causes references in p to be older than S. Is it not possible to let the verifier propagate that information up to the quantifier without needing the developer to use the older attribute?

---

Would it be possible to use an expression instead of an attribute for this, to make it more flexible? Like

predicate Reachable(source: Node, sink: Node, S: set<Node>)
  reads S
{
  exists via: Path<Node> :: older(via, S) && ReachableVia(source, via, sink, S)
}

predicate ReachableVia(source: Node, p: Path<Node>, sink: Node, S: set<Node>)
  reads S
  decreases p
{
  match p
  case Empty => source == sink
  case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)
}

Or

predicate Reachable(source: Node, sink: Node, S: set<Node>)
  reads S
{
  exists via: Path<Node> :: ReachableVia(source, via, sink, S)
}

predicate ReachableVia(source: Node, p: Path<Node>, sink: Node, S: set<Node>)
  reads S
  decreases p
  ensures ReachableVia(source, p, sink, S) ==> older(via, S)
{
  match p
  case Empty => source == sink
  case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)
}

[MikaelMayer]

This is a fantastic detailed explanation on why we need {:older}.

Something isn't quite right though on your last example:
It's impossible for p to be "older" than the parameters source and sink, because the path has to be allocated after these two nodes are allocated.
Can you please clarify on that?

[RustanLeino]

@keyboardDrummer

Quantifications implicitly quantify over allocated state

Is that to make the proofs more tractable?

No, it's part of story of claiming that the language is memory safe.

---

What if quantifications also implicitly quantify over readable state? In your example, Reachable already specifies reads S. Can't that mean that the instances of via in exists via: Path<Node> are limited to those containing references from S ?

This is an intriguing idea, which I have not considered before. The "implicitly" part of the suggestion is rather subtle, since a function like AllZeros, which has an empty reads clause, would then always return true. To make AllZeros say what is intended, you'd have to declare it with reads S, despite the fact that it doesn't read any mutable state. Similarly, a function like

predicate ContainsNothingButC(c: C, S: set<C>) {
  forall x :: x in S ==> x == c
}

would need to declare reads S, despite the fact that it does not read anything in the heap. A variation of the idea would be to use a separate declaration, say allocreads, instead of reads. Both AllZeros and ContainsNothingButC would then declare allocreads S and an empty reads clause. But allocreads is still subtle.

To make things less subtle, another variation of the idea would be to use the reads (or allocreads) clause not as an implicit bound for quantifiers, but an enforced bound--that it, there would be a proof obligation that what you quantify over is a subset of allocreads. To verify this proof obligation for Reachable, you would then need to know that ReachableVia(source, via, sink, S) implies that via is allocated. In other words, you would need {:older p}.

A different idea, which I have considered before, is introduce a specification that says the function can depend on the allocated state. (The syntax I have imagined for this is reads **.). Quantifications would still implicitly quantify over allocated state, and reads ** permits the function to do so. A function declared with reads ** would get a different frame axiom (in the Boogie encoding). When I have thought of this before, I have thought that reads ** implicitly includes reads *. That is, reads * (which exists in Dafny today) says that the function may depend on the state of any allocated object, and reads ** says that it may also depend on the allocation state. But your idea makes me think that ** would be better off just referring to the allocation state (not the allocation state plus *). Anyhow, I have suggested the reads ** feature on several occasions in the past, but the need for adding something like it was never big enough (probably because quantifying over the allocation state is a strange and dubious thing to do).

---

Or differently, shouldn't quantifier variables always be older than the parameters of the function containing the quantifier? Why do I still need to specify an older annotation?

Yes, I believe they should be. If the quantifier variables are older than the parameters, then the quantification does not depend on the allocation state. More precisely, I think the desired condition is that the quantifier variables are older than some parameter. But how do you encode this (into Boogie)? You'd have to arrange pass in the maximum allocation state (that is, the newest allocation time) of the parameters. For example, in

var b0 := MyPredicate(x, y, z);
var c := new MyClass();
var b1 := MyPredicate(x, y, z);

the two calls to MyPredicate are supposed to use the same quantification bound, so the verifier needs to know to pass in the same "max allocate state" parameter to both calls.

---

In your example, the n in S in

case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)

already causes references in p to be older than S. Is it not possible to let the verifier propagate that information up to the quantifier without needing the developer to use the older attribute?

Indeed, this is why the proof obligation for {:older p} works out. It would be difficult to infer this information syntactically, especially since ReachableVia is recursive. (Modules Reachable2 and Reachable3 in Test/dafny0/OlderVerification.dfy have some examples that make the inference even trickier.)

---

Would it be possible to use an expression instead of an attribute for this, to make it more flexible? Like
...
exists via: Path<Node> :: older(via, S) && ReachableVia(source, via, sink, S)
...
Or
predicate ReachableVia(source: Node, p: Path<Node>, sink: Node, S: set<Node>)
reads S
decreases p
ensures ReachableVia(source, p, sink, S) ==> older(via, S)

Such an older(via, S) as a conjunct of the quantification makes it possible for The Ban to syntactically detect, but it requires the Boogie encoding to pass in the allocation time of S. This is possible, but will require changes throughout the Dafny verifier.

The postcondition of ReachableVia expresses the desired property semantically. A downside is that the syntactic check of The Ban needs to look at the postcondition and pretty much insist that it have this exact form. That seems more brittle than using an attribute.

[RustanLeino]

@MikaelMayer

Something isn't quite right though on your last example: It's impossible for p to be "older" than the parameters source and sink, because the path has to be allocated after these two nodes are allocated. Can you please clarify on that?

Yikes! Let me think about this one.

[RustanLeino]

@MikaelMayer Thanks for your observation. I believe the semantic property is encoded correctly and the /help message is stated correctly, but the error message was not right. I rephrased the error message, hoping the new phrasing will make it clear.

In a nutshell, previously, the error message implied that (when the predicate returns true, then) each :older parameter must be (equally old or) older than each of the other parameters. More accurately, the actual condition is that each :older parameter must be older than one of the other parameters. Even that isn't right, because there may be no other parameters and the :older parameter may be, say, an integer, which is always allocated. So, the accurate condition is

• If the predicate returns true in a state where all the other parameters are allocated, then the :older parameters are also allocated in that state.

I changed the error message to say you must prove that

• :older parameters are not newer than any other parameter when the predicate returns true

[keyboardDrummer]

Have you considered making older a keyword that can be placed in front of the parameter of a predicate?

[keyboardDrummer]

I don't like to ask this, but could you follow-up with moving all bounds-related code from Resolver.cs to a separate file?

Also, in this PR, could you put this new block of code in a separate method?

[RustanLeino]

Good idea. I moved all bounds-discovery code into a separate file, and also moved the FunctionCallExpr block into a separate method.

[RustanLeino]

Have you considered making older a keyword that can be placed in front of the parameter of a predicate?

The fact that {:older} is helping the syntactic The Ban check makes it seem more attribute-like to me. In this regard, {:older} is similar to {:abstemious}, which is also used syntactically in order to allow more co-recursive functions. (Documentation for {:abstemious} is on our to-do list.)

The enforcement of {:older} includes a semantic check, which I admit is not as attribute-like. But the only reason to want this semantic check is to make sure the information used by the syntactic The Ban check is accurate.

Another attribute that might be construed as on the border between syntax and semantics is {:termination false}. However, I see it as a temporary band-aid until we implement the real semantic checks, so I wouldn't place much weight on it as a precedence.

An attribute that I think should be replaced by a keyword in the language is {:opaque}. Not only is {:opaque} central to information hiding in the language, but it's weird that {:opaque} is an attribute and reveal is a keyword.

So, I still favor {:older} as an attribute. What do you think?

[keyboardDrummer]

@RustanLeino Is the following a correct understanding of the origin of the problem?

A function with a reads clause takes an implicit heap parameter. We want to restrict references that originate from quantifiers to those that are allocated in the implicitly passed in heap, to provide memory safety. However, we want the result of the function to only depend on its explicit parameters, so we have to restrict references originating from quantifiers further to a subset that's entirely determined by the explicit parameters.

---

Given the above, wouldn't it be possible to always pass a modified version of the heap to functions, where the modified heap consists of only objects reachable from the function's explicit parameters? That way if the heap changes in ways unrelated to the function's explicit parameters, such as new objects being allocated, then the modified heap passed to the function does not change.

---

One I don't understand is why functions that don't have a reads clause, so they don't take an implicit heap, still have restrictions on their quantifiers. For example:

predicate AllZeros(S: set<Cell>) {
  forall c : Cell :: c in S ==> c.data == 0
}

gives the definition axiom:

function _module.__default.AllZeros#requires(Set Box) : bool;

// definition axiom for _module.__default.AllZeros for all literals (revealed)
axiom 1 <= $FunctionContextHeight
   ==> (forall S#0: Set Box :: 
    {:weight 3} { _module.__default.AllZeros(Lit(S#0)) } 
    _module.__default.AllZeros#canCall(Lit(S#0))
         || (1 != $FunctionContextHeight && $Is(S#0, TSet(Tclass._module.Cell())))
       ==> _module.__default.AllZeros(Lit(S#0))
         == (forall c#1: ref :: 
          { _module.Cell.data(c#1) } { S#0[$Box(c#1)] } 
          $Is(c#1, Tclass._module.Cell())
             ==> 
            Lit(S#0)[$Box(c#1)]
             ==> _module.Cell.data(c#1) == LitInt(0)));

function _module.__default.AllZeros#requires does not take a heap argument, so I would think the problem this PR relates to does not apply. But if I remove the c in S to get

predicate AllZeros(S: set<Cell>) {
  forall c : Cell :: c.data == 0
}

there's still a "a forall expression involved in a predicate definition is not allowed to depend on the set of allocated references" error message. Is this an occurrence of The Ban being too strict?

Also, in Boogie I don't see where the references from quantifiers are restricted to being allocated. Is that always done implicitly, in this case by the c in S that The Ban enforces?

[keyboardDrummer]

Isn't any nested function a local worker function?

[RustanLeino]

Yes, that's what the comment (redundantly) says.

[keyboardDrummer]

Thanks for explanation. I regret that we're asking Dafny users to understand yet another concept, that of {:older}, but I don't see an alternative. I feel this problem is related to #1702, since both are about how to get the values for a quantifier, although that one has problems during compilation and here we have problems during verification.

Is it really important to be able to draw values from the allocated heap, like you do in the motivating example? Can your motivating example not be replaced by:

predicate Reachable(source: Node, sink: Node, S: set<Node>)
  reads source
  reads S
  decreases S
{
  if source == sink then
    true
  else
    exists step: Node | step in S && step in source.children :: Reachable(step, sink, S - {step})
}

?

---

Regarding the syntax. You mention

The other complication is that there needs to be a way to mark the receiver parameter (this) with {:older}

Can the user not workaround that by making the callable static and the receiver explicit? If yes, then I'm not sure we need to solve this problem.

static {:older _this} function F(_this: C, x: X, y: Y): Z

The smaller complication is that Dafny currently doesn't allow parameters to have attributes.

Why would you want it to be an attribute, instead of a modifier keyword on parameters?

function F(older x: X, y: Y): Z

---

One thing I'm missing in error messages on quantifiers is the suggestion to {:older}. For example,

function Collection<X>(S: set<X>): iset<List<X>> {
  iset xs: List<X> | ElementsContainedIn(xs, S) // error: needs {:older xs} on ElementsContainedIn
}

Gives the error message:

Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references

How does the user find out they should use {:older} ?

---

Regarding the documentation, for me the motivating example you provided:

class Node {
  var children: seq<Node>
}

datatype Path<T> = Empty | Extend(Path, T)

predicate Reachable(source: Node, sink: Node, S: set<Node>)
  reads S
{
  exists via: Path<Node> :: ReachableVia(source, via, sink, S) // allowed because of {:older p} on ReachableVia
}

predicate {:older p} ReachableVia(source: Node, p: Path<Node>, sink: Node, S: set<Node>)
  reads S
  decreases p
{
  match p
  case Empty => source == sink
  case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)
}

to provide more clarity than just

predicate {:older} P(x: X, y Y)

function F(y: Y): int {
  if forall x: X :: P(x, y) ==> G(x, y) == 3 then
    100
  else
    0
}

Because the motivating example makes it clear why we can't add x in <Z> in the quantifier, and how the {:older} annotation can be proven, but the latter example does not.

[keyboardDrummer]

Added some minor comments. I'm OOTO from the 26th PST time to the end of the week. If you want to make more changes, feel free to have someone else review just those. I'm approving the current ones.

[keyboardDrummer]

Nitpick: consider using linq:

if (f.Formals.Any(formal => formal.IsOlder)) {
  reporter.Error(MessageSource.Resolver, formal.tok, "only predicates and two-state predicates are allowed 'older' parameters");
}

[RustanLeino]

The code produces one error for each older formal. This could be done with an .Iter(formal => { ... }), but for that, I think the current foreach is more readable.

[keyboardDrummer]

Nitpick: consider using LINQ

var olderBound = xs.Zip(ys).FirstOrDefault(t => t.First.IsOlder && t.Second.Resolved is IdentifierExpr ide && ide.Var == (IVariable)boundVariable);
if (olderBound != null) {
  bounds.Add(new ComprehensionExpr.OlderBoundedPool());
}

[keyboardDrummer]

Nitpick: C# also supports returning tuples with elegant syntax, which seems to be preferred over using out parameters (link), so you could also write:

(int olderParameterCount, Bpl.Expr olderCondition) OlderCondition(
  Function f, Bpl.Expr funcAppl, List<Bpl.Variable> inParams) {

}

[keyboardDrummer]

Consider naming this IsOlderObligation, so later on you can write IsOlderObligation instead of PODesc.IsOlder. The latter contains enough acronyms that I have to look up what it means.

[keyboardDrummer]

Is this intentional?

[keyboardDrummer]

Congrats!

[keyboardDrummer]

"already", what is the current time? I think it's not the time at which the predicate is called, because if I do two predicate calls with equivalent arguments, then the quantifier references must be allocated before the first call, even when evaluating the second call.

Shouldn't this say "More precisely, the object references that a quantifier may range
over must be shown to be confined to object references that were allocated before one of the parameters passed to the predicate." ?

[cpitclaudel]

Add a return here maybe (for clarity?)

[cpitclaudel]

No need for else

[cpitclaudel]

This whole if could be a case

[cpitclaudel]

Purely stylistic, but I would flip the condition and move the Add out of the if: `if (contains) { Error(); } Add

[cpitclaudel]

I would inline all these.

[cpitclaudel]

Maybe mention the name of the parameter? Parameter… is marked older but may be newer than all non-'older' parameters when predicate … returns 'true' ?