Specification Syntax Expressions & Quantifiers in Annotations

Expressions

As mentioned before, expressions in specifications are an extension of the expressions available in the target language. So if you analyse a Java program, you can use expressions like a&&b or x==y+1 in the specifications just like in Java. However, specifications must be free of side-effects (on the program state) and for example calls to non-pure methods are not allowed.

VerCors extends the expressions of the target language by a few more features that you can use in specifications. One of them is the implication operator ==>, which works like you would expect from a logical implication. A common usage is requires x!=null ==> <some statement about fields of x>. Note that the implication binds less than equality or conjunction, so a==>b&&c is equivalent to a==>(b&&c). You need to explicitly use parentheses if the operators shall associate differently.

A related new operator is the null-coalescing operator ?.. It can be used as expr?.fun(args), which is a shorthand for expr!=null ==> expr.fun(args). One use-case, where this comes in handy, is when using predicates in the place of the function fun (see section Predicates).

Two other new operators are ** and -* from separation logic. ** is the separating conjunct, while -* is the separating implication (or "magic wand"). For more on this, see the sections on Permissions and Magic Wands.

The target language is also extended to include new data types. A simple case is the boolean type bool, which can be useful in specifications if the target language has no boolean type (e.g. old C). If the target language does support boolean (e.g. Java), this is not needed (but can be used nonetheless). More interestingly, the new types include generic axiomatic data types such as set<T> and option<T> (with T being a type). For more information on them and their supported operations (such as getting the size, and indexing elements), see the respective section.

An important new type are fractions, frac. VerCors uses concurrent separation logic (CSL) to manage the ownership and permissions to access heap locations. A permission is a value from the interval (0,1], and the type frac represents such a value. To give a value to a variable of type frac, the new operator of fractional division can be used: While 2/3 indicates the classical integer division, which in this example gives 0, using the backslash instead gives a fraction: 2\3. For more on this topic, including some additional keywords for short-hand notations, see the section Permissions.

Sometimes, you might create complicated expressions and want to use helper variables to simplify them. However, certain constructs only allow for expressions, and not for statements such as variable declarations. To alleviate that, there is the \let construct, which defines a variable just for a single expression: ( \let type name = expr1 ; expr2 ), where type is the type of the helper variable, name its name, expr1 defines its value, and expr2 the complicated expression that you can now simplify by using the helper variable. Example:

//@ assert (\let int abs_x = (x<0 ? -x : x); y==(z==null ? abs_x : 5*abs_x));

Quantifiers

Note that most target languages, such as Java and C, support array types, such as int[]. Sometimes, you might want to reason about all elements of the array. To do that, VerCors supports using quantifiers in the specifications: (\forall varDecl, varDecl...; cond; expr). The syntax is similar to the header of a for loop: varDecl declares a variable (e.g. int i); cond is a boolean expression describing a boundary condition, restricting the declared variable to the applicable cases (e.g. defining the range of the integer 0<=i && i<arr.length); and expr is the boolean expression you are interested in, such as a statement you want to assert. Note that the parentheses are mandatory. Here is an example to specify that all elements in the given array are positive:

//@ requires arr != null;
//@ requires (\forall int i ; 0<=i && i<arr.length ; arr[i]>0);
void foo(int[] arr) { /* ... */ }

[!Note] In practice, you would also have to specify permissions to access the values in the array. More on that in the next section.

[!Tip] If you want to quantify over more than one variable (e.g. saying arr1[i] != arr2[j] for all i and j), do not use nesting, this commonly hurts proof performance. Instead, use a list of bindings: (\forall int i, int j; 0<=i && i<arr1.length && 0<=j && j<arr2.length; arr1[i]!=arr2[j]).

If your boundary condition is an interval (like in the examples above), you can use the shorter notation (\forall type name = e1 .. e2 ; expr), where type must be an integral type (e.g. int), name is the name of the quantified variable, e1 and e2 are expressions defining the interval bounds (lower bound inclusive, upper bound exclusive) and expr is the expression you are interested in: (\forall int i = 0 .. arr.length ; arr[i]>0).

[!Important] Depending on the circumstances, spaces are necessary around the .. because of unambiguous parsing.

You may freely mix normal bindings and range bindings, and omit the condition as you like. For example, all these quantifiers are equivalent:

• (\forall int i, int j; 0 <= i && i < n && i < j && j < n ==> xs[i] < xs[j])
• (\forall int i=0..n, int j; i < j && j < n; xs[i] < xs[j])
• (\forall int i=0..n, int j=i+1..n; xs[i] < xs[j])

There also is an \exists quantifier analogous to the forall quantifier: (\exists varDecl, ...; cond; expr). For instance, we could use a similar example as above, but requiring that at least one array element is positive:

//@ requires arr != null;
//@ requires (\exists int i ; 0<=i && i<arr.length ; arr[i]>0);
void foo(int[] arr) { /* ... */ }

Again, note that in practice, you would also have to specify permissions to access the values in the array.

Note

\forall quantifiers are easier to reason about than \exists, because they can be applied indiscriminately whenever an element is encountered, while \exists needs to find the element to which it can be applied. Therefore, \exists quantifiers are more likely to cause problems with VerCors (e.g. non-termination of the analysis), and they should be used with care!

Note

Further sections explain advanced concepts: new users may want to skip those._

Alternative quantifier syntax

In case brevity is needed for readability, you can use the appropriate unicode symbols instead of \forall and \exists:

• (∀varDecl+; (cond ;)? expr)
• (∃varDecl+; (cond ;)? expr)

For \forall* the following alternative notations are available:

• (∀*varDecl+; (cond ;)? expr)
• (✻varDecl+; (cond;)? expr)

The IntelliJ plugin Spec & Math Symbols may be useful to type these symbols.

Triggers

A quantifier (\forall int i = 0 .. arr.length ; arr[i]>0) is a rather generic piece of knowledge; to apply it to a concrete case, for example when encountering arr[1], the quantifier must be instantiated. This basically replaces the quantified variable(s), in this case i, with concrete values. But this is only done when necessary, so when the concrete case arr[1] is actually encountered. Recognising that the quantifier must be instantiated was fairly easy in this case, but for more complex expression it can become rather difficult. In those cases, VerCors might use heuristics, and even randomisation. This can lead to VerCors verifying a program successfully, and when you call it again with the exact same program, the analysis takes forever. So if you experience such behaviour, quantified expressions are a likely cause.

To avoid that, you can explicitly tell VerCors what kind of expression should cause instantiating the quantifier, disabling the internal heuristics. This is called a trigger (or pattern, e.g. by Z3); for more information see the Viper tutorial on triggers. In VerCors, to mark a part of an expression as a trigger, it is enclosed in {: and :}:

//@ requires arr!=null && arr.length>3;
//@ requires (\forall int i ; 0<=i && i<arr.length ; {: arr[i] :} > 0);
void foo(int[] arr) {
  assert arr[3]>0;   // the trigger recognises "arr[3]" and instantiates the quantifier, setting i to 3
}

(Again, Permissions were omitted.)

[!Important] The trigger must involve all quantified variables. So if you have a quantifier with multiple bindings (\forall int i, int j; ... ; expr), a trigger in expr must be about both i and j.

[!Warning] You cannot use arithmetic expressions or relations as triggers. Most other operators e.g. about sequences and sets may appear in triggers. For instance in the example above, {: arr[i]>0 :} would not be a valid trigger.

[!Warning] A wrong choice of triggers can lead to failed verifications of true statements:

/*@ pure @*/ int f(int a, int b);
    
//@ requires x>0;
//@ requires (\forall int k ; 0<=k && k<=x ; {: f(k, y) :} == 0);
//@ requires (\forall int k ; 0<=k && k<=x ; {: f(k, y) :} == 0 ==> f(k, z) == 0);
void bar(int x, int y, int z) {
    //@ assert f(x, y) == 0;     // this assertion verifies, because "f(x,y)" triggers the first quantifier
    //@ assert f(x/2, z) == 0;   // this assertion fails, even though the quantifiers includes this knowledge
}

In this example, the first quantifier asserts that f(x/2, y) == 0. From that, the second quantifier could derive f(x/2, z) == 0, so the second assertion should hold. However, the second quantifier has no trigger for f(k,z), so the quantifier does not get instantiated and the knowledge remains hidden. Removing the trigger around f(k,y) in the second quantifier leads to a successful verification, because without explicit triggers, VerCors' heuristics finds the correct trigger f(k,z) automatically.

Advanced trigger syntax

It is possible to specify multiple triggers for a single quantifier. In this case, the solver requires all triggers to be present before instantiating the quantifier. This also relaxes the requirement that all bindings must occur in a trigger: instead they must collectively occur in the set of all triggers. For example, a quantifier might state a pairwise equality:

(forall int i, int j; 0 <= i && i < |xs| &&
  0 <= j && j < |ys|;
  {:xs[i]:} + {:ys[j]:} == i + j)

This quantifier is only instantiated when both a term of the shape xs[?] and a term of the shape ys[?] is encountered by the solver. {xs[i], ys[i]} is also referred to as a trigger set.

In some cases it is useful to specify multiple trigger sets. In that case, all terms must be matched of any of the trigger sets. By default, a trigger is part of trigger set 0. For example:

(∀`seq`<T> xs, int i, T t;
    0 <= i && i < seq_length(xs) ==> 
    {:1:seq_length({:2:seq_update(xs, i, t):}):} ==
    {:2:seq_length(xs):})

This quantifier is instantiated when a term of the shape seq_length(seq_update(xs, i, t)) is encountered, or both a term of the shape seq_update(xs, i, t) and seq_length(xs). In such a case, it is required that the xs appearing in both patterns are equal before the quantifier is instantiated.

Finally, nested quantifiers are essentially instantiated separately: in principle the inner quantifier is never instantiated, unless the outer quantifier is instantiated. When specifying a trigger that is not meant for the innermost quantifier, you can use some number of < symbols to indicate the trigger belongs to the quantifier that many levels up. For example:

(∀int i; (∀int j; {:<:xs[i]:} == {:xs[j]:}))

Other trigger sources

We recommend the following sources for more examples and explanations of how triggers work.

• The paper "Trigger Selection Strategies to Stabilize Program Verifiers" gives an accessible and thorough introduction of triggers. They also describes problems of triggers, and automated solutions. These automated solutions can also be applied manually to PVL programs.
  • pdf, doi
• Dafny FAQ: How does Dafny handle quantifiers? I've heard about "triggers", what are those?
• Viper tutorial on triggers
• Stack Overflow: quantifiers - What are triggers in Dafny/Boogie?
• Extending Support for Axiomatic Data Types in VerCors, Section 2.3. Masters thesis by Ömer Şakar. Includes a visual explanation of the workings of triggers using Axiom Profiler, a quantifier instantiation debugging tool.