4 Expressions and operators🔗

Boogie has a single expression language, used identically in axioms, function bodies, procedure specifications, assertions, assumptions, assignments, loop invariants and attribute arguments. Every expression has a type; there are no statements-as-expressions except for the code expression (Code expressions), and no side effects anywhere.

This chapter describes the grammar of expressions, the precedence and associativity of every operator, the typing rule for each one, and the constructs whose behaviour is surprising or undocumented. All syntax is taken from Source/Core/BoogiePL.atg; all behaviour was observed by running the tool.

4.1 The expression grammar🔗

The expression productions form a chain, each level binding more tightly than the one above it. The following is the grammar as it appears in BoogiePL.atg, with the embedded C# semantic actions removed.

Expression           = ImpliesExpression { EquivOp ImpliesExpression } .

EquivOp              = "<==>" | '⇔' .

ImpliesExpression    = LogicalExpression

[ ImpliesOp ImpliesExpression

| ExpliesOp LogicalExpression

{ ExpliesOp LogicalExpression } ] .

ImpliesOp            = "==>" | '⇒' .

ExpliesOp            = "<==" | '⇐' .

LogicalExpression    = RelationalExpression

[ AndOp RelationalExpression { AndOp RelationalExpression }

| OrOp  RelationalExpression { OrOp  RelationalExpression } ] .

AndOp                = "&&" | '∧' .

OrOp                 = "||" | '∨' .

RelationalExpression = BvTerm [ RelOp BvTerm ] .

RelOp                = "==" | "<" | ">" | "<=" | ">=" | "!="

| '≠' | '≤' | '≥' .

BvTerm               = Term { "++" Term } .

Term                 = Factor { AddOp Factor } .

AddOp                = "+" | "-" .

Factor               = Power { MulOp Power } .

MulOp                = "*" | "div" | "mod" | "/" .

Power                = IsConstructor [ "**" Power ] .

IsConstructor        = UnaryExpression [ "is" Ident ] .

UnaryExpression      = "-" UnaryExpression

| NegOp UnaryExpression

| CoercionExpression .

NegOp                = "!" | '¬' .

CoercionExpression   = ArrayExpression { ":" ( Type | Nat ) } .

ArrayExpression      = AtomExpression

{ "[" [ Expression { "," Expression } [ ":=" Expression ]

| ":=" Expression ] "]"

| "->" ( Ident | "(" Ident ":=" Expression ")" ) } .

The comments in the grammar record two of the recursions explicitly: recurse because implication is right-associative, and recurse because exponentation is right-associative (the misspelling is in the source).

The atoms are:

AtomExpression = "false" | "true"

| ("roundNearestTiesToEven" | "RNE")

| ("roundNearestTiesToAway" | "RNA")

| ("roundTowardPositive"    | "RTP")

| ("roundTowardNegative"    | "RTN")

| ("roundTowardZero"        | "RTZ")

| Nat | Dec | Float | BvLit | string

| Ident [ "(" [ Expressions ] ")" ]

| "old"  "(" Expression ")"

| "int"  "(" Expression ")"

| "real" "(" Expression ")"

| "(" ( Expression

| Forall QuantifierBody

| Exists QuantifierBody

| Lambda QuantifierBody

| LetExpr ) ")"

| IfThenElseExpression

| CodeExpression .

Expressions          = Expression { "," Expression } .

IfThenElseExpression = "if" Expression "then" Expression "else" Expression .

Forall = "forall" | '∀' .   Exists = "exists" | '∃' .

Lambda = "lambda" | 'λ' .   QSep   = "::"     | '•' .

Two things follow immediately from this shape. First, quantifiers, lambdas and let expressions are only reachable through the parenthesised alternative, so their enclosing parentheses are part of the syntax, not optional grouping. Second, a function application is only recognised when an open parenthesis follows an identifier (whitespace between them is irrelevant — the lookahead is on tokens, so zero () is still a call); a function name on its own is not an expression.

function zero(): int;

procedure P()

{

assert zero == 0;

}

fapp2.bpl(4,9): Error: undeclared identifier: zero

1 name resolution errors detected in fapp2.bpl

4.2 Precedence and associativity🔗

The table below is derived from the nesting of the productions above, from loosest to tightest binding. It agrees with the binding strengths the pretty-printer uses (AbsyExpr.cs), which run from 0x00 for <==> to 0x90 for map selection.

Note where ++ sits: it is looser than +, so a + b ++ c groups as (a + b) ++ c. No runnable program can show this, because no arithmetic operator is defined on bit vectors, but the pretty-printer confirms the parse: /print echoes assert 1 + 2 ++ a == a; unparenthesised, whereas the other grouping would have printed as 1 + (2 ++ a).

Note also that is binds more tightly than every arithmetic operator but less tightly than the unary operators, and that the type coercion : T binds more tightly than unary minus, so -x : int is -(x : int).

Some of these can be checked directly:

procedure P()

{

assert 10 - 3 - 2 == 5;         // '-' groups to the left

assert 100 div 5 div 2 == 10;   // 'div' groups to the left

assert 2 + 3 * 4 == 14;         // '*' binds tighter than '+'

assert 2 - 3 + 4 == 3;          // '+' and '-' have equal binding power

assert -2 + 3 == 1;             // unary '-' binds tighter than binary '+'

assert 1 < 2 && 3 < 4;          // '<' binds tighter than '&&'

assert !false && true;          // parses as (!false) && true

}

procedure Q()

{

assert !true && false;          // error: parses as (!true) && false

}

ex-assoc.bpl(14,3): Error: this assertion could not be proved

Execution trace:

ex-assoc.bpl(14,3): anon0

Boogie program verifier finished with 1 verified, 1 error

The rest can be read off the pretty-printer, which re-inserts exactly the parentheses the parse requires. Running /print on

procedure P(p: bool, q: bool, r: bool, x: real, y: real, z: real)

{

assert p ==> q ==> r;

assert (p ==> q) ==> r;

assert p <== q <== r;

assert x ** y ** z == 0.0;

assert (x ** y) ** z == 0.0;

assert -x ** y == 0.0;

}

boogie /noVerify /print:- ex-print.bpl

The full output also repeats the banner, the bare procedure declaration and the usual trailing summary line; the implementation body is:

implementation P(p: bool, q: bool, r: bool, x: real, y: real, z: real)

{

assert p ==> q ==> r;

assert (p ==> q) ==> r;

assert r ==> q ==> p;

assert x ** (y ** z) == 0e0;

assert x ** y ** z == 0e0;

assert -x ** y == 0e0;

}

So ==> is right-associative (the left-nested form needs parentheses), a <== b <== c means c ==> (b ==> a), ** is right-associative, and unary minus binds tighter than **.

The printer prints both p <==> (q <==> r) and (p <==> q) <==> r as p <==> q <==> r, and likewise for && and ||; those regroupings are harmless because the operators are logically associative.

4.2.1 Operators that cannot be chained🔗

A relational operator may appear at most once per level, so a chained comparison is a parse error:

procedure P(a: int, b: int, c: int)

{

assert a < b < c;

}

ex-rel.bpl(3,16): error: ";" expected

1 parse errors detected in ex-rel.bpl

&& and || have equal binding power and cannot be mixed without parentheses. The grammar has no production for the mixture, so the failure is reported as an unexpected token:

procedure P(p: bool, q: bool, r: bool)

{

assert p && q || r;

}

ex-andor.bpl(3,17): error: ";" expected

1 parse errors detected in ex-andor.bpl

==> and <== also live at the same level and cannot be mixed, but here the parser produces a dedicated message:

procedure P(p: bool, q: bool, r: bool)

{

assert p ==> q <== r;

}

ex-imp.bpl(3,18): error: illegal mixture of ==> and <==, use parentheses to disambiguate

1 parse errors detected in ex-imp.bpl

4.2.2 Two parsing traps🔗

is binds looser than !. IsConstructor takes a UnaryExpression as its operand, so !c is Red means (!c) is Red, which is a type error whenever c is a datatype:

datatype Color { Red(), Green(shade: int) }

procedure P(c: Color, d: Color)

{

assert c is Red && d is Green;   // 'is' binds tighter than '&&'

}

procedure Q(c: Color)

{

assert !c is Red;                // parses as (!c) is Red

}

ex-isprec.bpl(10,9): Error: invalid argument type (Color) to unary operator !

1 type checking errors detected in ex-isprec.bpl

Write !(c is Red).

The else-branch of an if-then-else expression is a full expression. Because IfThenElseExpression ends with an unbracketed Expression, an unparenthesised if-then-else swallows everything to its right:

procedure P(p: bool)

{

// The else-branch is a full expression, so it swallows what follows.

assert 1 + if p then 2 else 3 == 3;

}

ex-ite.bpl(4,13): Error: branches of if-then-else have incompatible types int and bool

1 type checking errors detected in ex-ite.bpl

The expression parsed as 1 + (if p then 2 else (3 == 3)). Always parenthesise an if-then-else that is not the last thing in its expression.

4.3 Boolean operators🔗

<==>, ==>, <==, &&, || require both operands to unify with bool and produce bool; ! requires and produces bool.

a <== b is not a separate node in the AST: the parser builds Expr.Binary(Imp, b, a), so an explies is an implication with its operands swapped, as the /print output above shows.

Equality on two booleans is silently rewritten during type checking: BinaryOperator.ResolveOverloading turns a == b into a <==> b and a != b into a <==> !b when both sides are bool. This is only visible in the encoding, but it means == and <==> are the same operator on booleans, differing only in precedence.

4.4 Relational operators🔗

== and != are checked liberally, exactly as the paper describes: the two operand types need only be unifiable, i.e. there must exist some instantiation of the free type variables that makes them equal. So a type variable may be compared against a concrete type, but two distinct uninterpreted types may not.

type C, D;

// Equality only asks that the two sides be unifiable, so a type variable may

// be compared against a concrete type.

function polyEq<a>(x: a, y: int): bool { x == y }

procedure P(c: C, d: D)

{

assert c == d;      // error: C and D do not unify

}

ex-eq.bpl(9,11): Error: invalid argument types (C and D) to binary operator ==

1 type checking errors detected in ex-eq.bpl

<, <=, >, >= accept two ints, two reals, or two floats of the same format, and produce bool. They do not mix int and real: i >= 0.0 with i: int is a type error. Real division / is the one operator that does mix them; see Real division: /.

The paper’s RelOp also lists <:, the partial-order operator. It no longer exists:

type C;

const a: C;

const b: C;

axiom a <: b;

subtype.bpl(4,10): error: invalid UnaryExpression

1 parse errors detected in subtype.bpl

4.5 Arithmetic🔗

+, - and * accept two ints (giving int), two reals (giving real), or two floats of the same significand and exponent width (giving that float type). Unary - accepts only int and real, so unary minus on a float is rejected even though binary minus is accepted.

procedure P(f: float24e8, g: float24e8)

{

assert f + g == g + f;     // '+', '-', '*' and '/' are defined on floats

assert f - g == f - g;

assert f * g == g * f;

assert f / g == f / g;

assert f < g || g <= f;

}

procedure Q(f: float24e8)

{

assert -f == -f;           // error: unary '-' is not defined on floats

assert f div f == f;       // error: 'div' and 'mod' are int-only

}

ex-float.bpl(12,9): Error: invalid argument type (float24e8) to unary operator -

ex-float.bpl(12,15): Error: invalid argument type (float24e8) to unary operator -

ex-float.bpl(13,11): Error: invalid argument types (float24e8 and float24e8) to binary operator div

3 type checking errors detected in ex-float.bpl

4.5.1 Integer division and modulo: div and mod🔗

div and mod take two ints and produce an int. They are translated straight to the SMT-LIB Int operators of the same names, which are the Euclidean division and remainder: for a non-zero divisor b, a mod b is always non-negative and smaller than the absolute value of b, and a == b * (a div b) + (a mod b).

procedure Literals()

{

assert  7 div  2 ==  3 &&  7 mod  2 == 1;

assert -7 div  2 == -4 && -7 mod  2 == 1;

assert  7 div -2 == -3 &&  7 mod -2 == 1;

assert -7 div -2 ==  4 && -7 mod -2 == 1;

}

procedure Euclidean(a: int, b: int)

requires b != 0;

{

assert a == b * (a div b) + (a mod b);

assert 0 <= a mod b;

assert a mod b < (if 0 < b then b else -b);

}

Boogie program verifier finished with 2 verified, 0 errors

Note that this is neither C’s truncating semantics nor Java’s: with a negative dividend -7 div 2 is -4, not -3, and -7 mod 2 is 1, not -1. Front ends that need the source language’s semantics must define their own functions and axiomatise them.

Division by zero. SMT-LIB specifies div and mod as total functions, but leaves their value completely unconstrained when the divisor is zero. Boogie inherits that: a div 0 is a well-formed int-valued expression that equals itself, but nothing else about it is provable. The same holds for real division by 0.0.

procedure P(a: int)

{

assert a div 0 == a div 0;   // fine: 'div' is a total function

}

procedure Q(a: int)

{

assert a div 0 == 0;         // error: nothing is known about it

}

procedure R(a: real)

{

assert a / 0.0 == 0.0;       // error: same for real division

}

ex-divzero.bpl(8,3): Error: this assertion could not be proved

Execution trace:

ex-divzero.bpl(8,3): anon0

ex-divzero.bpl(13,3): Error: this assertion could not be proved

Execution trace:

ex-divzero.bpl(13,3): anon0

Boogie program verifier finished with 1 verified, 2 errors

Paper divergence. Section 4.0 of This is Boogie 2 says that Boogie provides / and % for integer division and modulo and gives them no meaning, to be axiomatised per source language. That is no longer true on two counts. The operators are spelled div and mod (% is not a token at all), and they have a fixed, Euclidean meaning inherited from the prover. / still exists but now means real division.

4.5.2 Real division: /🔗

/ accepts any combination of int and real operands and always produces a real; int operands are wrapped in to_real on the way to the prover. It also accepts two floats of the same format, in which case it is float division and produces that float type.

procedure P(i: int, r: real)

{

assert 7 / 2 == 3.5;         // '/' on two ints still yields a real

assert 1.0 / 2 == 0.5;       // mixed operands are accepted

assert i / 1 == real(i);

assert r / 1.0 == r;

}

Boogie program verifier finished with 1 verified, 0 errors

Because the result is always real, 7 / 2 == 3 is a type error, not a truth about truncation.

4.5.3 Exponentiation: **🔗

** requires both operands to be real and produces a real. There is no integer exponentiation and no mixed form.

procedure P(i: int, r: real)

{

assert i ** i == 0;     // error: '**' is real-only

assert i ** r == 0.0;   // error

assert r ** r == 0.0;   // well-typed

}

ex-powtype.bpl(3,11): Error: invalid argument types (int and int) to binary operator **

ex-powtype.bpl(4,11): Error: invalid argument types (int and real) to binary operator **

2 type checking errors detected in ex-powtype.bpl

4.5.4 Coercions between int and real🔗

int(e) and real(e) are the only numeric conversions, and they are syntactic forms rather than functions — int and real are type keywords, so the parenthesis is mandatory and the construct cannot be partially applied.

real(e) requires e : int and yields real; it becomes SMT-LIB to_real. int(e) requires e : real and yields int; it becomes SMT-LIB to_int, which is the floor, not truncation towards zero.

procedure P()

{

assert int(2.7) == 2;

assert int(-2.7) == -3;      // int() rounds towards negative infinity

assert real(3) == 3.0;

assert int(real(5)) == 5;

}

procedure Q(i: int, r: real)

{

assert int(i) == i;          // error: int() wants a real

assert real(r) == r;         // error: real() wants an int

}

ex-intreal.bpl(11,9): Error: argument type int does not match expected type real

ex-intreal.bpl(12,9): Error: argument type real does not match expected type int

2 type checking errors detected in ex-intreal.bpl

Note in particular that the coercions are not idempotent as forms: int(int(r)) and real(real(i)) are both type errors.

4.6 Type coercion: e : T🔗

e : T does not convert anything. It checks that T unifies with the type of e and gives the whole expression the type T, which is how an otherwise ambiguous polymorphic expression is pinned down. It is written postfix and may be repeated.

type C, D;

const c: C;

const d: D;

axiom (c : C) == c;      // ok

axiom (c : D) == d;      // error

axiom (15 : D) == d;     // error

ex-typecoerce.bpl(6,9): Error: C cannot be coerced to D

ex-typecoerce.bpl(7,10): Error: int cannot be coerced to D

2 type checking errors detected in ex-typecoerce.bpl

The grammar carries an explicit warning about this production: a type may begin with < (a polymorphic map type) but may also be followed by < (a comparison), and the parser always prefers to read more type. So a coercion followed by < does not parse:

type C;

const x: int;

axiom (x : int) > 0;     // ok

axiom x : C < 0;         // '<' is read as the start of a map type

ex-coerce-lt.bpl(4,15): error: invalid Ident

1 parse errors detected in ex-coerce-lt.bpl

Parenthesise the coercion when a < follows.

The same : token is reused inside square brackets for bitvector extraction: in CoercionExpression the alternative ":" Nat builds a BvBounds node rather than a coercion, which ArrayExpression then recognises. That is why the operands of an extraction must be integer literals — the parser reports arguments of extract need to be integer literals otherwise — and why parentheses around bitvector bounds are explicitly rejected.

4.7 Map selection and update🔗

a[i1, ..., in] selects; a[i1, ..., in := e] returns a map that agrees with a everywhere except at i1, ..., in, where it is e. Neither form modifies a. Both are postfix and chain left to right, and both bind more tightly than every other operator.

Selection on a polymorphic map instantiates the map’s type parameters afresh at each occurrence:

type Ref;

type Field _;

const f: Field int;

const g: Field bool;

procedure P(heap: <a>[Ref, Field a]a, o: Ref)

{

assert heap[o, f] + 1 == heap[o, f] + 1;

assert heap[o, g] || !heap[o, g];

assert heap[o, f := 3][o, f] == 3;

}

Boogie program verifier finished with 1 verified, 0 errors

The result type of an update is the type of the map being updated, and the right-hand side must have the type that the corresponding selection would have:

procedure Q(heap: <a>[Ref, Field a]a, o: Ref)

{

assert heap[o, f := true][o, f];   // error

}

ex-polymap.bpl(16,22): Error: right-hand side in map store with wrong type: bool (expected: int)

1 type checking errors detected in ex-polymap.bpl

The four ways to get a map expression wrong all have distinct messages:

procedure P(a: [int, int]int, b: [int]int, x: int)

{

assert a[1] == 0;          // error: wrong arity

assert x[1] == 0;          // error: not a map

assert b[1 := true][1];    // error: rhs type

assert b[true] == 0;       // error: index type

}

ex-maperr.bpl(3,10): Error: wrong number of arguments in map select: 1 instead of 2

ex-maperr.bpl(4,9): Error: map select applied to a non-map: x

ex-maperr.bpl(5,16): Error: right-hand side in map store with wrong type: bool (expected: int)

ex-maperr.bpl(6,11): Error: invalid type for argument 0 in map select: bool (expected: int)

4 type checking errors detected in ex-maperr.bpl

Ordinary select-of-store reasoning works as expected:

type Color;

const unique red: Color;

procedure P(a: [int, Color]int, m: [int][int]int)

{

assert a[5, red := 7][5, red] == 7;

assert a[5, red := 7][6, red] == a[6, red];

assert m[0][1] == m[0][1];

assert m[0 := m[0][1 := 3]][0][1] == 3;

}

Boogie program verifier finished with 1 verified, 0 errors

4.7.1 Extensionality🔗

Paper divergence. Section 4.1 of the paper states that maps do not necessarily satisfy extensionality, and gives b[j := b[j]] == b as an example of something that need not hold. By default that is no longer true: Boogie uses the prover’s array theory, which is extensional.

procedure P(b: [int]int, j: int)

{

assert b[j := b[j]] == b;

}

procedure Q(b: [int]int, c: [int]int)

requires (forall i: int :: b[i] == c[i]);

{

assert b == c;

}

Boogie program verifier finished with 2 verified, 0 errors

Passing /useArrayAxioms switches back to the axiomatisation the paper describes, and both assertions then fail:

boogie /useArrayAxioms ex-mapext.bpl

ex-mapext.bpl(3,3): Error: this assertion could not be proved

Execution trace:

ex-mapext.bpl(3,3): anon0

ex-mapext.bpl(9,3): Error: this assertion could not be proved

Execution trace:

ex-mapext.bpl(9,3): anon0

Boogie program verifier finished with 0 verified, 2 errors

Programs that must remain portable across both settings should not rely on extensionality.

4.8 Bitvector concatenation and extraction🔗

b ++ c concatenates, with the left operand supplying the high bits, and b[N:M] extracts the N - M bits of b starting at bit M (a half-open interval, so b[24:18] ++ b[18:7] == b[24:7]). N and M must be integer literals. Concatenation is left-associative and sits just above the relational operators in precedence; extraction is a postfix form at the same level as map selection.

procedure P(b: bv6, c: bv3)

{

assert (13bv6 ++ 4bv3)[5:2] == 3bv3;

assert (b ++ c)[9:3] == b;

}

procedure Q(b: bv32)

{

assert b[24:18] ++ b[18:7] == b[24:7];   // a repeated bound fuses

}

Boogie program verifier finished with 2 verified, 0 errors

The bitvector types themselves, and the {:bvbuiltin} mechanism for mapping Boogie functions onto the prover’s native bitvector operations, are covered in Bitvectors, floating point and rounding modes.

4.9 old expressions🔗

old(e) denotes the value of e in the pre-state. It is a syntactic form, not a function: the parentheses are part of the grammar.

old may only appear in a two-state context. Those are the postconditions of a non-pure procedure, the body of an implementation, and the argument of an attribute (which temporarily promotes a one-state context to a two-state one). Preconditions, axioms, function bodies and constant where clauses are not two-state contexts.

old is the identity on everything except global variables — it distributes to the leaves and does nothing to locals, parameters and out-parameters — and it is idempotent.

var g: int;

var h: int;

procedure P(x: int) returns (r: int)

modifies g;

ensures g == old(g) + x;

ensures old(g + h) == old(g) + old(h);

{

var b: int;

g := g + x;

assert old(g) + x == g;

assert old(old(g)) == old(g);   // old is idempotent

assert old(b) == b;             // old is the identity on locals

r := 0;

}

Boogie program verifier finished with 1 verified, 0 errors

Outside a two-state context the resolver refuses it. Note that an axiom is a stateless context, in which even a bare global variable is illegal, so both errors are reported:

var g: int;

procedure P()

requires old(g) == 0;   // error: a precondition is a one-state context

{

}

axiom old(g) == 0;        // error: an axiom is a stateless context

ex-oldbad.bpl(4,11): Error: old expressions allowed only in two-state contexts

ex-oldbad.bpl(8,6): Error: old expressions allowed only in two-state contexts

ex-oldbad.bpl(8,10): Error: cannot refer to a global variable in this context: g

3 name resolution errors detected in ex-oldbad.bpl

4.10 If-then-else expressions🔗

if c then a else b requires c : bool and requires the two branches to have unifiable types; the result has the type of the then-branch. Unlike the statement form, there is no elseif and the else branch is mandatory.

procedure P(p: bool, a: int, b: int)

{

assert (if p then a else b) == (if p then a else b);

assert (if true then 1 else 2) == 1;

assert 1 + (if p then 2 else 3) >= 3;

}

procedure Q(p: bool)

{

assert (if p then 1 else true) == 1;   // error

}

ex-ite2.bpl(10,10): Error: branches of if-then-else have incompatible types int and bool

1 type checking errors detected in ex-ite2.bpl

See Two parsing traps for the greedy else-branch.

4.11 Quantifiers🔗

QuantifierBody = ( TypeParams [ BoundVars ] | BoundVars )

QSep { AttributeOrTrigger } Expression .

A quantifier binds a list of variables, optionally preceded by a list of type variables, and its body must have type bool. The whole expression has type bool. The surrounding parentheses are required by the grammar.

Note that the type-parameter list may appear without any value parameters, so a quantifier that binds only types is legal.

type Barrel _;

function Q<a>(int, Barrel a): bool;

function R(int): bool;

axiom (forall <a> x: int, y: Barrel a :: Q(x, y));            // ok

axiom (forall x: int :: (forall <a> y: Barrel a :: Q(x, y))); // ok

axiom (forall <a> :: (forall y: Barrel a :: Q(0, y)));        // type-only binder

axiom (forall <a> x: int :: (exists y: Barrel a :: Q(x, y))); // accepted

axiom (forall <a> x: int :: { R(x) } (exists y: Barrel a :: Q(x, y)));  // error

ex-typequant.bpl(9,28): Error: trigger does not mention a, which does not occur in variables types either

1 type checking errors detected in ex-typequant.bpl

Paper divergence. Section 4.4 says every bound type variable must be mentioned somewhere in the types of the bound value variables, and gives (forall <a> x: int :: (forall y: Barrel a :: Q(x, y))) as an error. The implementation only checks this when the quantifier carries a positive trigger (QuantifierExpr.Typecheck loops over Triggers to report it). Without a trigger, an unmentioned type variable is silently accepted, as the fourth axiom above shows. Lambdas are checked unconditionally — see Lambda expressions.

4.11.1 Scoping of bound variables🔗

Paper divergence. Section 4.4 says bound variables must be distinct from each other and from local variables, parameters and other bound variables in scope, but explicitly permits reusing the name of a constant or a global. The implementation enforces only the first part of that: a name may not be declared twice in the same binder list, but a quantifier may freely shadow a parameter, a local or an enclosing bound variable (as well as a constant or a global, which the paper already allows).

const g: int;

var h: int;

function f(int): bool;

axiom (forall g: int :: f(g));   // may shadow a constant

axiom (forall h: int :: f(h));   // may shadow a global

procedure P(x: int)

{

var y: int;

assert (forall x: int :: f(x));                     // shadows a parameter

assert (forall y: int :: f(y));                     // shadows a local

assert (forall z: int :: (exists z: int :: f(z)));  // nested rebinding

}

Boogie program verifier finished with 1 verified, 0 errors

The shadowing is real, not merely tolerated: the inner binding wins.

procedure P(x: int)

requires x == 0;

{

assert (forall x: int :: x == 0);   // the bound x hides the parameter

}

ex-shadow.bpl(4,3): Error: this assertion could not be proved

Execution trace:

ex-shadow.bpl(4,3): anon0

Boogie program verifier finished with 0 verified, 1 error

4.11.2 Adjacent quantifiers are merged🔗

If a quantifier’s body is a quantifier of the same kind and neither carries a trigger, QuantifierExpr.MergeAdjacentQuantifier fuses them into a single quantifier over the concatenated binder list, to give the prover a better chance of picking a trigger. The merge is observable, because the two binder lists then have to be consistent with each other:

function f(int, int): bool;

// Adjacent trigger-free quantifiers of the same kind are merged into one,

// which puts both z's into a single binder list.

axiom (forall z: int :: (forall z: int :: f(z, z)));

ex-merge.bpl(5,32): Error: more than one declaration of variable name: z

1 name resolution errors detected in ex-merge.bpl

Replacing the inner forall with an exists, or adding a trigger to either quantifier, suppresses the merge and the program is accepted.

4.11.3 Triggers🔗

A trigger is written as a braced list of expressions after the ::, with no leading : to distinguish it from an attribute. Several braced groups may follow, in any order, interleaved with attributes.

AttributeOrTrigger = "{" ( ":" Ident [ AttributeParameter { "," AttributeParameter } ]

| Expression { "," Expression } ) "}" .

Each braced group is one alternative trigger; several expressions inside a single group form a multi-trigger, all of whose terms must be present before the quantifier fires.

function f(int): int;

function g(int): int;

axiom (forall x: int :: { f(x) } f(x) == x);                    // one trigger

axiom (forall x: int :: { f(x) } { g(x) } f(x) == g(x));        // two alternatives

axiom (forall x: int, y: int :: { f(x), g(y) } f(x) == g(y));   // one multi-trigger

axiom (forall x: int :: { f(x + 1) } { f(x) != 0 } f(x) == x);  // arithmetic and '!='

axiom (forall m: [int]int, x: int :: { m[x] } m[x] == x);       // map select

Boogie program verifier finished with 0 verified, 0 errors

Legality rules. Trigger.Resolve runs the trigger expressions in trigger mode, in which BinaryOperator.Resolve, UnaryOperator.Resolve and BinderExpr.Resolve reject certain operators. The complete set of restrictions is:

• a trigger term may not be a bare identifier — the test is e is IdentifierExpr, so a bound variable, a constant and a global are all rejected alike, even as one term of a multi-trigger;

• every positive trigger must mention every bound variable of the quantifier;

• == is rejected, but != is allowed;

• <, <=, >, >= are rejected;

• &&, ||, ==>, <==> and ! are rejected;

• quantifiers and lambdas are rejected — a lambda is reported with the message quantifiers are not allowed in triggers, since the check lives in the shared BinderExpr.Resolve.

Arithmetic (+, -, *, div, mod, /, **), function application, map selection, old and datatype accessors are all permitted.

function f(int): int;

axiom (forall x: int :: { x } f(x) == x);                 // just a variable

axiom (forall x: int, y: int :: { f(x) } f(x) == y);      // omits y

axiom (forall x: int :: { f(x) == 0 } f(x) == x);         // equality

axiom (forall x: int :: { f(x) < 0 } f(x) == x);          // comparison

axiom (forall x: int :: { f(x) == 0 && true } f(x) == x); // boolean operator

axiom (forall x: int :: { (forall y: int :: f(y) == x) } f(x) == x);  // quantifier

ex-trigbad.bpl(3,26): Error: a matching pattern must be more than just a variable by itself: x

ex-trigbad.bpl(4,32): Error: trigger must mention all quantified variables, but does not mention: y

ex-trigbad.bpl(5,31): Error: equality is not allowed in triggers

ex-trigbad.bpl(6,31): Error: arithmetic comparisons are not allowed in triggers

ex-trigbad.bpl(7,36): Error: boolean operators are not allowed in triggers

ex-trigbad.bpl(7,31): Error: equality is not allowed in triggers

ex-trigbad.bpl(8,27): Error: quantifiers are not allowed in triggers

ex-trigbad.bpl(8,49): Error: equality is not allowed in triggers

8 name resolution errors detected in ex-trigbad.bpl

Why != is allowed. A trigger of the shape E != literal is not sent to the prover as written. SMTLibLineariser strips the comparison and emits only E as the pattern. Writing { f(x) != 0 } is therefore a way of spelling the pattern f(x); it produces exactly

:pattern ( (f x))

in the prover log. This behaviour is undocumented.

Effect of a trigger. A quantified axiom only contributes to a proof when its trigger matches a term the prover already has. The following pair differ only in the trigger:

function f(int): int;

function h(int): int;

axiom (forall x: int :: { f(x) }    f(x) == x);

axiom (forall x: int :: { h(h(x)) } h(x) == x);

procedure P()

{

assert f(3) == 3;    // the trigger f(x) matches the term f(3)

}

procedure Q()

{

assert h(3) == 3;    // error: no h(h(...)) term exists, so nothing fires

}

ex-trigeffect.bpl(14,3): Error: this assertion could not be proved

Execution trace:

ex-trigeffect.bpl(14,3): anon0

Boogie program verifier finished with 1 verified, 1 error

4.11.4 Negative triggers: {:nopats E}🔗

{:nopats E} looks like an attribute but is handled by the parser as a negative trigger: it tells the prover never to use E as a matching pattern. It becomes an SMT-LIB :no-pattern annotation. If a quantifier has any positive trigger, the negative ones are dropped, because Z3 ignores :no-pattern in the presence of :pattern and warns.

{:nopats} takes exactly one expression argument. Anything else is rejected:

function f(int): bool;

function g(int): bool;

axiom (forall x: int :: {:nopats f(x)} {:nopats g(x)} f(x) && g(x));   // ok

axiom (forall x: int :: {:nopats f(x), g(x)} f(x));                    // error

axiom (forall x: int :: {:nopats "f"} f(x));                           // error

ex-nopats.bpl(5,43): error: the 'nopats' quantifier attribute expects a string-literal parameter

ex-nopats.bpl(6,34): error: the 'nopats' quantifier attribute expects a string-literal parameter

2 parse errors detected in ex-nopats.bpl

Negative triggers are also inserted without being written. The check lives in the resolver, not the parser: at the end of QuantifierExpr.Resolve, if the quantifier has no positive trigger, ApplyNeverTriggers walks the body and adds a :no-pattern for every application of a function declared {:never_pattern}.

4.12 Lambda expressions🔗

A lambda has the same syntax as a quantifier, with lambda in place of forall, and denotes a map. (lambda x1: T1, ..., xn: Tn :: e) has type [T1, ..., Tn]U where U is the type of e; with type parameters <a> it has the polymorphic map type <a>[T1, ..., Tn]U. A lambda may mention variables from the enclosing scope.

procedure P(k: int)

{

var m: [int]int;

var n: [int, int]int;

var id: <a>[a]a;

m := (lambda i: int :: i + k);   // captures k

assert m[5] == 5 + k;

n := (lambda i: int, j: int :: i * j);

assert n[3, 4] == 12;

id := (lambda <a> y: a :: y);

assert id[3] == 3;

}

Boogie program verifier finished with 1 verified, 0 errors

Triggers are rejected outright in a lambda — the check is in the parser, so it is a parse error rather than a resolution error:

procedure P()

{

var m: [int]int;

m := (lambda i: int :: { i } i + 1);   // error: triggers not allowed

}

ex-lambdabad.bpl(4,36): error: triggers not allowed in lambda expressions

1 parse errors detected in ex-lambdabad.bpl

Unlike quantifiers, a lambda’s bound type variables must occur in the types of its parameters, and the check does not depend on triggers:

procedure P()

{

var m: [int]bool;

m := (lambda <a> x: int :: true);   // error: 'a' is unused

}

ex-lambdatv.bpl(4,8): Error: the type variable a does not occur in types of the lambda parameters

1 type checking errors detected in ex-lambdatv.bpl

4.12.1 Lambda lifting🔗

Lambdas do not survive into the verification condition. Before verification, each lambda is replaced by a call to a generated function whose parameters are the lambda’s free variables, together with a defining axiom whose trigger is the selection from that function. /printLambdaLifting together with /print shows the result:

procedure P(x: int)

{

var c: [int]int;

c := (lambda i: int :: i + x);

assert c[0] == x;

}

boogie /noVerify /print:- /printLambdaLifting ex-lift.bpl

/printLambdaLifting makes /print emit the whole program twice, once before lifting (where the body still reads c := (lambda i: int :: i + x);) and once after. Omitting the two banners, the two procedure declarations, the first copy and the trailing summary, the second copy is:

implementation P(x: int)

{

var c: [int]int;

c := lambda#0(x);

assert c[0] == x;

}

// auto-generated lambda function

function lambda#0(l#0: int) : [int]int

uses {

axiom (forall l#0: int, i: int :: { lambda#0(l#0)[i] } lambda#0(l#0)[i] == i + l#0);

}

The practical consequence is that reasoning about a lambda goes through a triggered axiom: facts about (lambda ...) are only available at indices that appear as selections in the query.

4.13 let expressions🔗

LetExpr = "var" LetVar { "," LetVar } ":=" Expression { "," Expression } ";"

{ Attribute } Expression .

LetVar  = { Attribute } Ident .

(var x := e; body) binds x to e in body. The bound variables are untyped in the source; their types are taken from the right-hand sides during type checking. The expression has the type of body. Like quantifiers, a let is only reachable through the parenthesised alternative, so the parentheses are mandatory, and the semicolon between the bindings and the body is part of the syntax.

Multiple bindings are simultaneous, not sequential: the right-hand sides are resolved in the enclosing scope, before the new names are pushed. Nesting gives the sequential behaviour.

procedure P(a: int, b: int)

{

assert (var x := a + b; x * x) == (a + b) * (a + b);

assert (var x, y := a, b; x - y) == a - b;

assert (var x := 1; (var y := x + 1; y)) == 2;   // nesting is fine

}

Boogie program verifier finished with 1 verified, 0 errors

procedure P()

{

assert (var x, y := 1, x + 1; y) == 2;   // error: bindings are simultaneous

}

procedure Q()

{

assert (var x := 1, 2; x) == 1;          // error: arity mismatch

}

ex-letbad.bpl(3,25): Error: undeclared identifier: x

ex-letbad.bpl(8,10): Error: number of left-hand sides does not match number of right-hand sides

2 name resolution errors detected in ex-letbad.bpl

A let is translated to an SMT-LIB let, so the right-hand side is shared rather than duplicated.

4.14 Code expressions🔗

CodeExpression = "|{" { LocalVars } SpecBlock { SpecBlock } "}|" .

SpecBlock      = Ident ":" { LabelOrCmd }

( "goto" { Attribute } Idents

| "return" { Attribute } Expression ) ";" .

A code expression is an imperative block graph used as a boolean expression. It is written between |{ and }|, may declare local variables, and consists of one or more labelled blocks. Each block ends either in a goto to other blocks of the same code expression or in return E, where E must have type bool. Execution starts at the first block. The whole expression has type bool.

Code expressions are not mentioned in This is Boogie 2 at all.

Inside a block, the full set of simple commands is available: assert, assume, havoc, assignment, call, measure, reveal/hide and push/pop. A block may carry only one label.

procedure P()

{

assert |{ A: return true; }|;

assert |{ var x: bool; A: x := true; return x; }|;

assert |{ var x: int; A: havoc x; return x == x; }|;

}

procedure Q(x: int, y: int)

requires |{ var z: bool;

Start: goto A, B;

A: assume 0 <= x; z := true;  goto R;

B: assume x < 0;  z := false; goto R;

R: return z;

}|;

{

assert 0 <= x;

}

Boogie program verifier finished with 2 verified, 0 errors

A procedure call inside a code expression works too, and the callee’s specification is used as it would be anywhere else:

procedure Yes() returns (r: bool);

ensures r;

procedure No() returns (r: bool);

ensures !r;

procedure P()

{

assert |{ var b: bool; A: call b := Yes(); return b; }|;

}

procedure Q()

{

assert |{ var b: bool; A: call b := No(); return b; }|;   // error

}

ex-codecall.bpl(14,3): Error: this assertion could not be proved

Execution trace:

ex-codecall.bpl(14,3): anon0

Boogie program verifier finished with 1 verified, 1 error

4.14.1 Meaning🔗

CodeExprConversionClosure.CodeExprToVerificationCondition builds the verification condition of the block graph exactly as it would for a procedure body: predecessors are computed, the blocks are passified, and the weakest precondition is generated. The local variables are then quantified over the resulting formula, and the polarity of the occurrence decides which quantifier is used.

In an asserted (positive) position, a code expression means every execution reaches a return E with E true, and every assert inside it holds. In an assumed (negative) position it means some execution does. The two are not the same predicate, so the same code expression carries different information depending on where it appears.

procedure P()

{

assert |{ A: assert false; return true; }|;   // the inner assert is checked

}

procedure Positive()

{

assert |{ var x: bool; A: return x; }|;       // x is universally quantified

}

procedure Negative()

{

assume |{ var x: bool; A: return x; }|;       // x is existentially quantified

assert false;

}

ex-codebad.bpl(3,3): Error: this assertion could not be proved

Execution trace:

ex-codebad.bpl(3,3): anon0

ex-codebad.bpl(8,3): Error: this assertion could not be proved

Execution trace:

ex-codebad.bpl(8,3): anon0

ex-codebad.bpl(14,3): Error: this assertion could not be proved

Execution trace:

ex-codebad.bpl(13,3): anon0

Boogie program verifier finished with 0 verified, 3 errors

Positive fails because x is arbitrary; Negative fails because the assumption is vacuously satisfiable and yields nothing. Both are sound approximations, but they mean a code expression is not a plain predicate you can move across a negation.

Note also that CodeExpr.ComputeFreeVariables is a no-op: the comment reads Treat a BlockExpr as if it has no free variables at all. Passes that depend on free-variable computation therefore do not see inside a code expression.

4.14.2 Errors🔗

procedure P()

{

assert |{ A: B: return true; }|;   // two labels in one block

}

ex-codeerr.bpl(3,17): error: SpecBlock's can only have one label

1 parse errors detected in ex-codeerr.bpl

procedure P()

{

assert |{ A: goto B; }|;   // no such block

}

ex-codeerr2.bpl(3,15): Error: goto to unknown block: B

1 name resolution errors detected in ex-codeerr2.bpl

procedure P()

{

assert |{ A: return 3; }|;   // the returned expression must be bool

}

ex-codeerr3.bpl(3,22): Error: a return expression must be of type bool (got: int)

1 type checking errors detected in ex-codeerr3.bpl

4.15 Datatype expressions🔗

Three expression forms operate on algebraic datatypes. They postdate the paper entirely.

e is C tests whether e was built with constructor C; it produces bool. e->f selects the field named f; the field may belong to several constructors, which are required to declare it at the same type. e->(f := v) returns a copy of e with field f replaced; when f is shared by several constructors, the update is expanded into a chain of is-guarded conditionals, so it keeps whichever constructor the value already had.

All three are part of the postfix level, so they chain left to right and bind more tightly than everything else except each other. A constructor is applied like an ordinary function.

datatype Pair { Pair(a: int, b: int) }

datatype Wrap { Wrap(p: Pair) }

datatype Split { Left(i: int), Right(i: int) }

procedure P(w: Wrap, ps: [int]Pair, s: Split)

{

assert Wrap(Pair(1, 2))->p->b == 2;             // '->' chains left to right

assert w->(p := Pair(1, 2))->p->a == 1;         // field update yields a new value

assert ps[0]->a == ps[0]->a;                    // select then field access

assert s->(i := 7)->i == 7;                     // shared field name

assert s is Left  ==> s->(i := 7) == Left(7);

assert s is Right ==> s->(i := 7) == Right(7);

}

Boogie program verifier finished with 1 verified, 0 errors

Resolution of is and -> is deferred to type checking, because the datatype is not known until then. The errors are reported there:

datatype Split { Left(i: int), Right(i: int) }

type T;

procedure P(s: Split, t: T)

{

assert s->j == 0;      // no such field

assert s is Middle;    // no such constructor

assert t is Left;      // not a datatype

}

ex-dterr.bpl(6,12): Error: datatype Split does not have a field with name j

ex-dterr.bpl(7,14): Error: datatype Split does not have a constructor with name Middle

ex-dterr.bpl(8,14): Error: is-constructor must be applied to a datatype, T is not a datatype

3 type checking errors detected in ex-dterr.bpl

A field name shared by two constructors must be declared at the same type in both; the error is reported on the datatype declaration, not on the use:

datatype S { A(i: int), B(i: bool) }

procedure P(s: S) { assert s->i == s->i; }

dtshared.bpl(1,26): Error: type mismatch between field i and identically-named field in constructor A

1 type checking errors detected in dtshared.bpl

Datatype declarations themselves are covered in Algebraic datatypes.

4.16 Type checking of expressions🔗

Type checking runs after name resolution, over the whole program. It is a unification process: each expression node computes its type from the types of its children, and type variables and unresolved type proxies are unified along the way. Conversions are essentially never implicit: there is none between bitvector widths and none between float formats, and int and real mix only in the operands of / (Real division: /), which silently wraps an int operand in to_real. Everywhere else a conversion is written out with int(...) or real(...).

The failure messages follow a fixed shape. A binary operator reports invalid argument types (T1 and T2) to binary operator OP; a unary operator reports invalid argument type (T) to unary operator OP; int/real report argument type T does not match expected type U; a coercion reports T cannot be coerced to U.

Section 5 of This is Boogie 2 singles out two rules as the only interesting ones, and both still hold.

Map selection and update operate on polymorphic maps, so the rule has to find an instantiation σ of the map’s type parameters that makes the actual index types match the declared domain types, and then reports the range type under that same σ. See Map selection and update.

Equality is checked liberally: a == b is well-typed whenever the two operand types are unifiable, even if they are not equal as written. The paper’s reading of that is worth keeping in mind: a == b means the two sides evaluate not only to the same value but to values of the same type. See Relational operators.

Everything else is routine: a quantifier body and a code expression must be bool, a lambda’s type is the map type built from its parameter types and its body type, a let takes the type of its body, and an if-then-else takes the type of its then-branch after unifying the two branches.

4.17 Divergences from This is Boogie 2🔗

• Integer division and modulo are div and mod, not / and %, and they have a fixed Euclidean meaning rather than none (paper 4.0).

• / is real division and always produces a real; ** is real exponentiation. Neither exists in the paper.

• Maps are extensional by default; the paper says they are not (paper 4.1). /useArrayAxioms restores the paper’s behaviour.

• The subtype operator <: of the paper’s RelOp no longer exists.

• Bound variables may shadow parameters, locals and enclosing bound variables; the paper forbids it (paper 4.4).

• A bound type variable that does not occur in the types of the bound variables is only reported when the quantifier has a trigger; the paper says it is always an error (paper 4.4).

• if-then-else expressions, lambda, let, code expressions, the datatype forms is and ->, the int/real coercions, floats and strings all postdate the paper.