Predicates

TODO: Clarify usage of "resource" and "predicates"

This section discusses syntax and semantics of resources and predicates. First a motivating example is given why predicates are needed. Then an overview is given of the syntax and semantics of predicates. The introductory example is then rewritten using predicates. Finally, we discuss some internal and reserved predicates, and finish this part of the tutorial with a brief overview of advanced usages of predicates and known problems.

In this section, the language used for the code examples is Java. However, the concepts presented apply to PVL as well.

Why predicates?

Permissions are useful for indicating access rights and modifications to data. But, adding permissions to private members in the contract leaks implementation details. Consider the following example:

class Counter {
  int count;
  
  //@ context Perm(count, write);
  //@ ensures count == \old(count) + n;
  void increment(int n);
}

class MyProgram {
  //@ requires c != null;
  //@ requires Perm(c.count, write);
  //@ requires c.count == 0;
  void foo(Counter c) {
    //@ assert c.count == 0;
    c.increment(2);
    //@ assert c.count == 2;
  }
}

It is clear from the contract of increment that it modifies the internal state of the Counter object. Therefore, when Counter changes its internal layout, client code will have to be modified as well. For example, if in the previous example Counter adds some internal field, the client code will also have to be changed. This is shown in the next example:

class CounterExtended {
  int count;
  int numIncrements;
  
  //@ context Perm(count, write) ** Perm(numIncrements, write);
  //@ ensures count == \old(count) + n
  //@ ensures numIncrements == \old(numIncrements) + 1;
  void increment(int n);
}

class MyProgram {
  //@ requires c != null;
  //@ requires Perm(c.count, write);
  //@ requires c.count == 0;
  void foo(Counter c) {
    //@ assert c.count == 0;
    c.increment(2);
    //@ assert c.count == 2;
  }
}

It is desirable that permissions are managed such that client code does not depend on irrelevant details, to avoid this rippling effect of modifications. Predicates help with this.

Predicate syntax and usage

A predicate is declared as follows:

//@ resource myPredicate(int a, bool b, ...) = body;

A predicate consists of the name of the predicate, zero or more arguments, and a body where arguments can be used. In Java, the declaration must be written as a verification annotation (e.g. using //@). In PVL, it is a plain declaration.

To create a predicate instance, the contents of the predicate body must be exchanged for a predicate instance. This is called "folding". Specifically, folding a predicate means any permissions present in the predicate body are removed from the program state. In return, an instance of the predicate is added to the state. In the following example folding is shown. The method foo receives a permission for the field x. At the end of the method, the permission for this field x has been exchanged for an instance of the predicate state. Note how the permission for x and the predicate state are mutually exclusive: both cannot be in the program state simultaneously.

int x;

//@ resource state(int val) = Perm(x, write) ** x == val;

//@ requires Perm(x, write) ** x == n;
//@ ensures state(n);
void foo(int n) {
    // Now we have Perm(x, write).
    //@ fold state(n);
    // Now Perm(x, write) is gone, but state(n) is present.
}

A predicate can also be "unfolded". This exchanges a predicate instance for its body.

int x;

//@ resource state(int val) = Perm(x, write) ** x == val;

//@ requires state(n);
//@ ensures Perm(x, write) ** x == n;
void foo(int n) {
    // Now we have state(n);
    //@ unfold state(n);
    // Now state(n) is gone, but Perm(x, write) is present.
}

The previous two examples also show that fields of the current class can be used in the predicate body. This is because a predicate instance is implicitly bound to an instance of the class it is defined in. The following example verifies, because the this part of the predicate instance is implicit. It also shows how to name predicates on objects other than this.

class Cell {
    int x;

    //@ resource state(int val) = Perm(x, Write) ** x == val;

    // "this" is implicit:
    //@ requires this.state(n);
    //@ ensures state(n);
    void foo(int n) {

    }

    // Predicates can appear on distinct objects too:
    //@ given int n;
    //@ given int m;
    //@ context other.state(m);
    //@ requires state(n)
    //@ ensures state(n+m);
    void combine(Cell other) {
        //@ unfold state(n);
        //@ unfold other.state(m);
        x += other.x;
        //@ fold other.state(m);
        //@ fold state(n+m);
    }
}

Predicates can be used anywhere Perm can be used, and hence must also be composed using the separating conjunction (**) operator.

The Counter example, now with predicates

In the next snippet we redefine the Counter class to use predicates, instead of plain permissions:

class Counter {
  int count;

  //@ resource state(int val) = Perm(count, write) ** count == val;
  
  //@ given int oldCount;
  //@ requires state(oldCount);
  //@ ensures state(oldCount + n);
  void increment(int n);
}

class MyProgram {
  //@ requires c != null ** c.state(0);
  //@ ensures c.state(2);
  void foo(Counter c) {
    //@ assert c.state(0);
    c.increment(2) /*@ with { oldCount = 0; } @*/;
    //@ assert c.state(2);
  }
}

The client only uses the predicate when expressing how it manipulates the counter. Therefore, the counter class is now free to change its internal composition without affecting any of its clients. This is possible because only relevant details are exposed through the predicate. In this case, this is the value of the counter. For example, adding a plain field does not break the client.

If the interface of Counter changes, the client code will have to change too. However, the client code does not have to manage any extra permissions: it only has to specify how it uses the interface from CounterExtended. The next example shows this.

class CounterExtended {
  int count;
  int numIncrements;

  /*@ resource state(int val, int val2) = Perm(count, write) ** count == val 
        ** Perm(numIncrements, write) ** numIncrements = val2;
    @*/
  
  //@ given int oldCount;
  //@ given int oldIncrements;
  //@ requires state(oldCount, oldIncrements);
  //@ ensures state(oldCount + n, oldIncrements + 1);
  void increment(int n);
}

class MyProgram {
  //@ given int oldIncrements;
  //@ requires c != null ** c.state(0, oldIncrements);
  //@ ensures c.state(2, oldIncrements + 1);
  void foo(Counter c) {
    //@ assert c.state(0, oldIncrements);
    c.increment(2) /*@ with { oldCount = 0; oldIncrements = oldIncrements; } @*/;
    //@ assert c.state(2, oldIncrements + 1);
  }
}

To summarise, predicates are very effective at hiding implementation details. They allow encapsulation. However, predicates do not protect the client from breaking changes. If the interface changes, any clients will have to change too.

Reserved/internal predicates

There are a few situations where VerCors attaches special meanings to certain predicate names.

For atomics/locks

For atomics and locks a predicate lock_invariant is defined. This predicate cannot be folded/unfolded, and has to be manipulated through locking and unlocking.

Additionally, it can be checked if a lock is currently held through the held(x) syntax. held is in this case effectively a predicate that cannot be unfolded. Therefore, any semantics and techniques for manipulating predicates discussed in this part of the tutorial can be applied to held, such as splitting and scaling, except for folding and unfolding.

For more information, see the Atomics and Locks section.

Threads

A thread can be in several states, such as idle and running. The syntax for this is idle(thread) and running(thread). idle and running are effectively predicates that cannot be unfolded. Therefore, any semantics and techniques for manipulating predicates discussed in this part of the tutorial can be applied to held (such as splitting and scaling).

See the PVL Syntax Reference section for more details.

Advanced usage of predicates

Unfolding predicates within expressions using \unfolding

Sometimes it is necessary to briefly open a predicate within an expression, for example, to temporarily gain access to a field. This can be achieved using the \unfolding operator. It has the following concrete syntax:

\unfolding myPredicate(arg1, arg2, ...) \in expression

It takes the instance of the predicate that needs unfolding, followed by \in, and then an expression in which the predicate must be unfolded. After evaluating the internal expression, the predicate is folded again, without any changes to the predicate or the program state.

Below is an example usage of \unfolding in a Cell class where the predicate does not have a parameter for the value inside the Cell. To work around this, \unfolding is used.

class Cell {
  //@ ensures state() ** \unfolding state() \in x == 0;
  Cell() {
    x = 0;
    //@ fold state();
  }

  //@ resource state() = Perm(x, write);
  int x;
}

public static void main() {
  Cell c = new Cell();
  //@ assert \unfolding c.state() \in c.x == 0;
}

Recursive predicates

Predicates can directly and indirectly recurse without problems, provided they are not inline. This can be used to for example model permissions over data structures with a size that cannot be known statically, such as a linked list. In the below code example, an instance of state predicate of the class LinkedListNode contains the permission for one field, as well as permissions for all fields of the tail of the list. Additionally, the argument of the state predicate reflects the numbers stored in the linked list.

class LinkedListNode {
  //@ resource state(seq<int> data) = Perm(v, write) ** Perm(next, write) ** v == data[0] ** (next != null ==> next.state(tail(data)));

  int v;
  LinkedListNode next;
}

Scaling & splitting

VerCors offers syntax to specify fractions of predicates, similar to how permissions can be specified in fractions. This can be useful to, for example, allow one half of a state predicate to be passed to one thread, and one to another. For a predicate state(args) on a variable x, the syntax for specifying a fraction f of the predicate is: [f]x.state(args). The code below shows an example of how scaling can be used.

class Cell {
  //@ ensures state(0);
  Cell() {
    //@ fold state(0);
  }

  //@ resource state(int v) = Perm(x, write) ** v == x;
  int x;
}

//@ requires [1\2]c.state(0);
public void startThread(Cell c);

public static void main() {
  Cell c = new Cell();
  // Constructing a cell yields a state predicate
  //@ assert c.state(0);
  // We can split this into fractions of a predicate
  //@ assert [1\2]c.state(0) ** [1\2]c.state(0);

  // startThread will claim half of the predicate
  startThread(c);

  // The other half can be used for something else
  //@ assert [1\2]c.state(0);
}

Inline predicates

Predicates can be given the inline attribute:

class C {
  //@ inline resource state() = Perm(x, write);
  int x;
}

If the inline attribute is given to a predicate, VerCors will inline the definition of that predicate wherever the predicate occurs. This means that the following code snippet:

//@ requires c.state();
void foo(C c) {
  //@ assert c.state();
}

Is equal to:

//@ requires Perm(c.x, write);
void foo(C c) {
  //@ assert Perm(c.x, write);
}

Because of this inlining semantics, inline predicates cannot be recursive. However, besides that limitation they are equal to regular predicates, and hence support arguments and scaling.

Furthermore, because of this inlining semantics, folding and unfolding inline predicates do not change the program state. However, for the ease of flexibility, VerCors allows them, interpreting them as a check for whether or not the contents of a predicate is present.

Inheritance

Inheritance is not yet supported for predicates.

Known problems

VerCors crashes when predicates are unfolded

When using predicates, VerCors might yield the following error:

Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.NoSuchElementException: None.get
  Cause: java.util.concurrent.ExecutionException: java.util.NoSuchElementException: None.get

This is because the current implementation of Java inheritance in VerCors is incomplete. There are two workarounds for this.

First, a predicate declaration can be marked as final. This ensures that the inheritance-related logic in VerCors is not applied to that predicate, which means it can be used as described in this chapter. In the code below we show an example usage of this workaround.

int x;

//@ final resource state(int val) = Perm(x, write) ** x == val;

//@ requires Perm(x, write) ** x == n;
//@ ensures state(n);
void foo(int n) {
    //@ fold state(n);
}

Second, if a class has many predicates, or the first workaround does not seem to work, the whole class can be marked as final. This ensures the inheritance-related logic in VerCors is not applied to the class at all.

Both workarounds do not change the semantics of Java code that does not use inheritance.

Finally, if neither of the workarounds work, please file an issue.

Interaction between loop conditions and predicates

Consider the following example:

//@ resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant \unfolding wrapX(i) \in 5 <= x && x <= 10;
  while (x < 10) {
    //@ unfold wrapX(i);
    x++;
    //@ ghost i++;
    //@ fold wrapX(i);
  } 
}

This will give an error on the while condition, stating that there is no permission for x. This is to be expected, since permission for x is contained in the predicate wrapX(i). Since we did not give instructions to unfold it, the loop condition cannot access x. Intuitively, the following extra syntax should work:

//@ resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant \unfolding wrapX(i) \in 5 <= x && x <= 10;
  while (/*@ \unfolding wrapX(i) \in @*/ x < 10) {
    //@ unfold wrapX(i);
    x++;
    //@ ghost i++;
    //@ fold wrapX(i);
  } 
}

However, this syntax is currently not supported by VerCors. Instead, it is recommended to use an inline predicate if possible (see the Inline Predicates section for more info). Applying this workaround results in the following program:

//@ inline resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant 5 <= x && x <= 10;
  while (x < 10) {
    x++;
    //@ ghost i++;
  } 
}

Alternatively, the condition can be lifted into its own boolean variable as in the example below. However, this 1) leads to verbose code, and 2) requires modification of non-ghost code.

This example needs a bit of revision, as p below changes, compared to the condition of the previous example

//@ resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  // Put the loop condition in a separate variable. This requires unfolding the predicate temporarily.
  //@ unfold wrapX(5);
  boolean p = 5 <= x && x < 10;
  //@ fold wrapX(5);

  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant \unfolding wrapX(i) \in 5 <= x && x <= 10;
  // Require that loop maintains that p equals the previous loop condition
  //@ loop_invariant p == \unfolding wrapX(i) \in (5 <= x && x < 10);
  while (p) {
    //@ unfold wrapX(i);
    x++;
    //@ ghost i++;

    // Before the while loop ends, check the loop condition manually
    // And put the result in p again.
    p = 5 <= x && x < 10;
    //@ fold wrapX(i);
  }

  //@ assert wrapX(10);
}