Specification Syntax
This section describes the syntax of the specification language, which is independent of the target language. Thus, unless otherwise stated, all features are supported for all input languages.
In this part of the tutorial, we will take a look at how specifications are expressed in VerCors. While this tutorial provides more detailed explanations of the various constructs, a concise list can be found in the PVL Syntax Reference in the annex. The specification language is similar to JML.
Depending on the input language, specification are embedded into the target code in two different ways:
In most languages, such as Java and C, the specifications are provided in special comments.
These special comments are either line comments starting with //@, or block comments wrapped in /*@ and @*/.
Since these are simply a kind of comment, regular compilers ignore them and can still compile the program.
However, the @ signals VerCors to interpret them as annotations.
Note that this style of comment comes from JML, so VerCors is not the only tool using them.
However, the exact interpretation of the comments may vary between tools, so a valid specification in VerCors may not be recognised by another tool and vice versa.
As an example, a method pre-condition (see following section) can look like this:
//@ requires x>0;
public int increment(int x) { /* ... */ }
/*@
requires x>0;
requires y>0;
@*/
public int add(int x, int y) { /* ... */ }Tip Always remember to place the @!
It can be aggravating to spend significant time debugging, just to realise that parts of the specification were put in regular comments and ignored by the tool.
For PVL, the specifications are inserted directly into the code, without the special comments around them:
requires x>0;
int increment(int x) { /* ... */ }
requires x>0;
requires y>0;
int add(int x, int y) { /* ... */ }
Given that the syntax is otherwise identical, we will use the commented version in the rest of the tutorial, to make the separation between specifications and target code more obvious. The examples in this chapter are in Java, but you can find the respective examples in other languages on the website (as well as a Java file of all the examples below).
Most annotation constructs have to end with a semicolon.
In principle, we can distinguish two kinds of annotations: Specifications in the form of method contracts that specify the observable behaviour of the respective method; and auxiliary annotations that guide the prover towards its goal and are for example used inside a method's body, or to define helper functions. We will first look at the former, then at the latter, and conclude with a description of the kind of expressions that VerCors supports (e.g. boolean connectives). For the earlier parts, it suffices to know that expressions in VerCors specifications are an extension of whatever expressions the target language supports.
Method contracts specify the behaviour of the method that is visible to the calling environment, by means of pre-conditions and post-conditions.
Pre-conditions use the keyword requires and restrict the situations in which the method can be invoked, e.g. restricting parameters to be non-null.
Post-conditions use the keyword ensures and describe the behaviour of the method by defining the program state after the call finishes.
The method contract is placed above the method header, and these keywords can only be used in combination with a method header.
Two useful keywords to define the post-state (i.e. the state after the method finishes) are \result to refer to the return value of the (non-void) method, and \old(expr) to refer to the value of expr before the method's execution.
class Test {
/*@
requires x >= 0;
requires y >= 0;
ensures \result == x+y;
ensures \result >= 0;
@*/
public int add(int x, int y) {
return x+y;
}
/*@
requires xs != null;
ensures \result != null;
ensures \result.length == \old(xs.length)+1;
ensures \result.length > 0;
@*/
public int[] append(int[] xs, int y) {
int[] xsCopy = new int[xs.length + 1];
/* ... */
return xsCopy;
}
}Recall that VerCors analyses methods in isolation, purely based on their contract and independent from any actual calling contexts.
It tries to prove that if the pre-condition is satisfied before the method body is executed, then the post-condition holds afterwards.
In the example of the add method above, if the input parameters are non-negative, then the result is, too.
Note that the pre-condition x>=0 is not actually required for executing the method body, but it is necessary to prove the post-condition.
In contrast, in the example of append, the pre-condition xs!=null is actually needed for \old(xs.length) to be well-defined, and potentially to prove absence of null-pointer dereferences in the method body.
Note that, to fully specify the correct behaviour of append, one would have to compare the values inside of xs and \result.
Since these values are stored on the heap (and not on the stack like the reference xs itself), this would require access permissions, which will be introduced in the next chapter "Permissions".
Note Method contracts must not have side effects, so for example calls to (non-pure) methods are forbidden inside contracts.
Pre- and post-conditions are processed in-order, so for example swapping the order of two pre-conditions could result in a failed verification (e.g. you need to specify that an integer variable is within range before you can use it as an array index in another pre-condition).
Note that unsatisfiable pre-conditions (e.g. contradictory conditions, or simply false) can lead to unexpected results, because the implication "if pre-condition before, then post-condition after" becomes trivially true for any post-condition, and VerCors is able to prove any arbitrary statement.
Sometimes, the same expression is needed as a pre- and as a post-condition, for example the fact that a global variable is not null.
In that case, the keyword context can be used as a short-hand notation: context xs != null; stands for requires xs!=null; ensures xs!=null;.
An even further reaching short-hand is context_everywhere expr;, which adds expr as a pre- and as a post-condition, as well as a loop invariant for all loops inside the method body (see below).
When method bodies become more complicated than the toy examples above, it becomes more difficult for VerCors to prove by itself that the post-conditions hold after executing the method, and additional annotations are needed inside the method body to guide the verification. These can take the form of loop invariants, assumptions and assertions, or ghost code. Ghost code can also occur outside of methods, for instance to define helper functions.
Loop invariants are similar to the context in a method contracts, but for loops:
They specify expressions that must hold before entering the loop (like a pre-condition), as well as after each loop iteration, incl. the last iteration (like a post-condition).
Loop invariants use the keyword loop_invariant and are placed above the loop header:
//@ requires a>0 && b>0;
//@ ensures \result == a*b;
public int mult(int a, int b) {
int res = 0;
//@ loop_invariant res == i*a;
//@ loop_invariant i <= b;
for (int i=0; i<b; i++) {
res = res + a;
}
return res;
}Let us examine why this program verifies (you can skip this paragraph if you are familiar with software verification and loop invariants):
The first loop invariant holds before we start the loop, because we initialise both i and res to zero, and 0 == 0*a is true.
Then in each iteration, we increase i by one and res by a, so if res == i*a held before the iteration, then it will also hold afterwards.
Looking at the second invariant, we see that it holds before the loop execution because i is initialised to zero and b is required to be greater than zero.
To understand why the invariant holds after each iteration, we also have to consider the loop condition, i<b.
This condition has to be true at the beginning of the iteration, otherwise the loop would have stopped iterating.
Since i and b are integers and i<b at the beginning of the iteration, an increment of i by one during the iteration will ensure that at the end of the iteration, i<=b still holds.
Note that if i or b were floating point numbers, i might have gone from b-0.5 to b+0.5, and we would not have been able to assert the loop invariant.
Likewise, any increment by more than one could step over b.
Only the combination of all these factors lets us assert the invariant at the end of the loop iteration.
When the loop stops iterating, we know three things: Each of the two loop invariants holds, and the loop condition does no longer hold (otherwise we would still be iterating).
Note that the combination of the second loop invariant and the negated loop condition, i<=b && !(i<b), ensures that i==b.
Combining that with the first invariant ensures the post-condition of the method.
Remember that VerCors checks for partial correctness, so there is no check whether the loop actually stops iterating at some point. It just asserts that if the loop stops, then the post-condition holds.
As mentioned above, context_everywhere expr; in the method contract will implicitly add expr as a loop invariant to all loops in the method body.
This can be useful for expressions that hold for the entirety of the method, e.g. in the case of xs!=null; but it can also be a subtle cause for errors if it adds invariants to a loop that were not intended there (especially in the case of multiple loops).
For example, a method to insert an element into a sorted array may add the new value at the end, and then step by step restore the ordering of the array; in that case, adding a sortedness property as context_everywhere would not verify.
Sometimes, VerCors has trouble deriving a post-condition from the given code and established facts (like pre-conditions), and it requires explicitly specifying an intermediate step to guide the verification.
VerCors first proves these intermediate steps, and then can use them to derive the desired facts.
This can be done with the keyword assert:
//@ ensures a==0 ? \result == 0 : \result >= 10;
public int mult10(int a) {
int res = a;
if (res < 0) {
res = 0-res;
}
//@ assert res >= 0;
return 10*res;
}(Note that VerCors would be able to verify this example even without the assertion, but this demonstrates how to use assert.)
Tip Assertions can also be useful for debugging:
If VerCors fails to prove the post-condition, adding assert statements throughout the method body can help to pinpoint where the verification fails, either because of a shortcoming of VerCors or because of an actual error in the code.
Additionally, assert false; should always fail, so if the verification does not seem to terminate, adding such statements throughout the method can show where VerCors gets stuck.
Finally, remember that a contradiction e.g. in the pre-conditions can imply anything; even false.
So assert false; can be used to check that no such contradiction occurred: If it verifies, something went seriously wrong.
While assertions add additional proof obligations, assumptions introduce additional facts that VerCors just takes for granted afterwards, similar to pre-conditions.
This is done via the keyword assume.
This can be dangerous if the assumptions contradict the actual state of the program:
int x = 2;
//@ assume x == 1;
int y = x + 3;
//@ assert y == 4;This snippet verifies, even though the actual value of y at the end is 5.
However, based on the (wrong) assumptions that x==1 on Line 2, the assertion holds.
Therefore, assumptions should be used with caution!
Nevertheless, assumptions can be useful, e.g. for debugging purposes. Also, while still being in the process of verifying the code, it can be useful to assume certain basic facts to prove the bigger picture, and then drill deeper and prove that the assumed facts actually hold.
VerCors also supports a refute statement, which is the opposite of assert.
Internally, refute expr; is transformed into assert !(expr);, i.e. asserting the negation.
Note that a failing assert expr; is not equivalent to a successful refute expr;.
For example, if we know nothing about the value of a variable a, then both assert a>0; and refute a>0; will fail, as a could be greater than zero, but it also could be less.
Recall that annotations must never have side-effects on the program state, otherwise the results of methods would be different between VerCors (which takes the annotations into account) and the compiler (which treats them as comments). However, it can be useful to extend the program state, for example introducing additional helper variables to keep track of intermediate results. This helper code, which only exists for the purpose of verification, is called ghost code, and the respective variables form the ghost state.
Ghost code can occur inside method bodies, but also outside, for instance as global ghost variables.
In principle, ghost code can be any construct that the target language supports; for example when verifying Java programs, you could define ghost classes, and in C programs, you may use pointers in ghost code.
Additionally, the ghost code can use the extensions that the specification language adds to the target language, such as the new type seq<T> (see section "Expressions" below).
Keep in mind that ghost code does not exist for the compiler, so it cannot have side effects on the program state, and "real" code cannot refer e.g. to ghost variables. However, it is possible to read from "regular" variables (e.g. to create a ghost variable with the same value).
When using constructs from the target language (such as variable declarations), the keyword ghost is required before the use of the construct.
Here is an example for ghost code inside a method:
/*@
requires x>=0 && y>=0;
ensures \result == (x<y ? 5*x : 5*y);
@*/
public int minTimes5(int x, int y) {
//@ ghost int min = (x<y ? x : y);
int res = 0;
//@ loop_invariant i<=5;
//@ loop_invariant res == i*min;
//@ loop_invariant min<=x && min<=y && (min==x || min==y);
for (int i=0; i<5; i++) {
if (x<y) {
res = res + x;
} else {
res = res + y;
}
}
/*@
ghost if (x<y) {
assert res == 5*x;
} else {
assert res == 5*y;
}
@*/
return res;
}Note the definition of a ghost variable min at the beginning of the method, and the ghost if statement at its end.
You can use ghost code not only within methods but also to declare entire ghost methods:
/*@
ghost
requires x > 0;
ensures \result == (cond ? x+y : x);
static int cond_add(bool cond, int x, int y) {
if (cond) {
return x+y;
} else {
return x;
}
}
@*/
//@ requires val1 > 0 && val2>0 && z==val1+val2;
void some_method(int val1, int val2, int z) {
//@ ghost int z2 = cond_add(val2>0, val1, val2);
//@ assert z == z2;
}The conditional addition cond_add is defined as a ghost method.
Otherwise, it looks like any normal method, including having a method contract (in this case, just a single precondition).
Note that the precondition is not wrapped in the special comment //@, like the precondition of some_method is, because the entire ghost method already is inside a special comment /*@.
We then use this ghost method in the body of some_method (but only inside annotations!).
Functions are, in a way, a special kind of ghost methods.
They look like any method, but they are pure by design (as signified by the keyword pure) and their body is a single expression following an =, rather than a block of statements:
/*@
requires x > 0;
static pure int cond_add(bool cond, int x, int y)
= cond ? x+y : x;
@*/Note that the ghost keyword is not used:
It is only required when using a construct from the target language (e.g. if, variable declarations, etc), not for specification-internal constructs like defining a function.
However, using a stand-alone call statement to call the function (e.g. invoke a lemma directly and not in an assert) still needs the ghost keyword, as method calls are constructs from the target language: //@ ghost myLemma();.
The important distinction to normal methods, apart from the fact that they have just one expression, is that functions must be pure, i.e. must be without side-effects, even on the ghost state.
Thus, the body cannot contain for instance calls to non-pure methods.
Remember that in VerCors, only the contract of a method is used to reason about the behaviour of a method call, the actual behaviour of the method body is not taken into account at this point. For functions, this restriction is not as strict: For simple functions like the one above, VerCors actually uses the "real" behaviour of the function to analyse the behaviour of a call to that function. Thus, the behaviour does not need to be specified explicitly in a post-condition, like it does for other methods. However, this only works for simple functions, and for example a recursive function may still need a post-condition specifying its behaviour.
You can also add the pure keyword to a "real" method.
This indicates that the method does not have side-effects, and can therefore be used e.g. in method contracts, while still being accessible by the "real" code.
However, for a method to be pure, it has to be actually without side-effects, therefore only a limited number of constructs are allowed in methods that are designated pure: if statements, return statements and variable declarations.
/*@
requires x > 0;
@*/
static /*@ pure @*/ int cond_add(boolean cond, int x, int y) {
if (cond) {
return x+y;
} else {
return x;
}
}Ghost functions and methods do not require a body.
Sometimes, you are only interested in the assertions that a function or method gives in its post-condition, and do not care about the actual implementation.
In such a case, you can omit the body, turning the method or function abstract.
Given that method calls are usually reasoned about only based on the contract, the call site does not see a difference between an abstract method and a "real" method.
However, this removes the assurance that it is actually possible to derive the post-condition from the pre-condition by some computation.
Consider a post-condition false:
The call site will simply assume that the method establishes its post-condition, and treat it as a known fact.
Normally, verifying the method body will check that the post-condition is actually fulfilled; but for an abstract method, this check is missing.
Since false implies everything, this can easily lead to unsoundness.
Therefore, from the perspective of correctness, it is always better to have a body proving that the post-condition can actually be established based on the pre-condition.
However, making a method abstract relieves VerCors from the effort to check that the method body actually adheres to the contract. Therefore, it can be an interesting option to speed up the re-run of an analysis: Once you proved that a method can indeed derive its post-condition, you can turn the method abstract and focus on other parts of the code without checking this method every time you re-run the analysis.
Syntactically, an abstract method or function has a semicolon in place of its body:
//@ requires a>0 && b>0;
//@ ensures \result == a*b;
public int mult(int a, int b);
// commented out body for the sake of speeding up the analysis:
//{
// int res = 0;
// // loop_invariant res == i*a;
// // loop_invariant i <= b;
// for (int i=0; i<b; i++) {
// res += a;
// }
// return res;
//}
/*@
requires a>0 && b>0;
ensures \result == a+b;
public pure int add(int a, int b);
@*/Note that VerCors can also work with abstract methods that are not ghost methods (like mult in the example above), but your compiler may complain about missing method definitions.
Inline functions are like macros in C:
You can write an expression that occurs frequently in your code as a macro and then use it as if it were a function; but before verifying the program, VerCors replaces every call to the inline function with the function's body as if you had written out the body in place of the function call.
Therefore, during the analysis, the "real" behaviour of the function is taken into account, rather than just the specification of the function's contract.
However, inline functions are only possible if the body of the function is simple enough; for example a recursive function cannot be used in that way, otherwise there would be an infinite loop of replacing a function call with the body, which again contains a call.
Inline functions are declared using the inline keyword.
//@ pure inline int min(int x, int y) = (x<y ? x : y);Note that the inline keyword is also used for inline predicates (see chapter "Predicates"), which are a similar concept.
You can extend the header of an existing method, by adding additional parameters and return values to a method.
This is done by using the given and yields keywords in the method contract, respectively.
To assign and retrieve the values when calling the method, use given and yields symmetrically:
/*@
given int x;
given int y;
yields int modified_x;
requires x > 0;
ensures modified_x > 0;
@*/
int some_method(boolean real_arg) {
int res = 0;
/* ... */
//@ ghost modified_x = x + 1;
/* ... */
return res;
}
void other_method() {
//@ ghost int some_ghost;
int some_result = some_method(true) /*@ given {y=3, x=2} @*/ /*@ yields {some_ghost=modified_x} @*/;
}There are several points of interest in this example:
Note that the pre- and post-condition of some_method can reference the ghost parameter and result just like normal parameters.
If the ghost parameters and results are not just primitive integers, but heap objects, then permissions are needed to access them, just like with normal parameters and results (see following chapter).
There is no explicit return statement for the ghost result; instead, the ghost result is whatever value the variable has when the method returns.
Therefore, make sure when your method returns that you always have a defined value assigned to your ghost result variable!
In other_method, the given keyword is followed by a list of bindings to the ghost parameters.
The parameters are named, so the assignment can be in any order, and need not adhere to the order in which the ghost parameters are defined.
Make sure to assign a value to each ghost parameter!
Otherwise, the method will be missing a parameter, just as if you called a method void foo(int x) as foo();.
Similarly, the yields keyword is followed by a block of bindings that retrieve the yielded values. The yielded values may only be immediately assigned to a local variable.
The respective local variable, some_ghost, must be a ghost variable, otherwise you would affect the "real" program state from inside an annotation. Note that it is not required to have an output for every yielded value.
Both the given and the yields are placed in a specification comment between the method call and the respective semicolon.
As mentioned above, 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 chapter "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 chapters 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 chapter.
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 chapter "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));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 that in practice, you would also have to specify permissions to access the values in the array. More on that in the next chapter.
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). Note that, depending on the circumstances, spaces are necessary around the ...
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.
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)(∃varDecl+; (cond ;)? expr)
The IntelliJ plugin Spec & Math Symbols may be useful to type these symbols.
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.)
Note that 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.
Also note that 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.
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]:}))
We recommend the following sources for more examples and explanations of how triggers work.
- 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 Datatypes 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.
Tutorial
- Introduction
- Installing and Running VerCors
- Prototypical Verification Language
- Specification Syntax
- Permissions
- GPGPU Verification
- Axiomatic Data Types
- Arrays and Pointers
- Parallel Blocks
- Atomics and Locks
- Process Algebra Models
- Predicates
- Inheritance
- Exceptions & Goto
- VerCors by Error
- VeyMont
- Advanced Concepts
- Annex
- Case Studies
Developing for VerCors