5 Top-level declarations🔗

A Boogie program is a flat, unordered sequence of top-level declarations. There are no modules, no namespaces the programmer can open or close, and no include directives: everything a file declares is visible everywhere in that file (and in every other file passed on the same command line, since Boogie concatenates its inputs into a single program).

This chapter covers the declaration forms that describe the program’s logical vocabulary and its global state: type, const, function, axiom and var. Procedures and implementations are covered in Procedures, implementations and specifications, datatype in Algebraic datatypes, and the Civl declaration forms (action, invariant, yield procedure) in Civl: concurrency and refinement.

5.1 The shape of a program🔗

The top-level production in Source/Core/BoogiePL.atg is, with the semantic actions elided:

BoogiePL

=

{ Consts

| Function

| Axiom

| UserDefinedTypes

| Datatype

| GlobalVars

| InvariantDecl

| "yield"

(

InvariantDecl

| YieldProcedureDecl

)

| Pure

(

Procedure

| ActionDecl

)

| Implementation

}

EOF

.

A program is therefore just a repetition of declarations, in any order, followed by end of file. There is no separator between declarations; each declaration form terminates itself.

5.1.1 Namespaces🔗

Boogie keeps four separate symbol tables, populated by ResolutionContext.AddType, AddVariable, AddFunction and AddProcedure:

• Types — type constructors (type T;), type synonyms (type T = ...;) and datatypes share one table.

• Variables — constants and global variables share one table (and, inside a procedure body, so do formals and locals).

• Functions — including datatype constructors.

• Procedures — including Civl actions and yield invariants.

The tables are completely independent, so the same identifier can name a type, a constant, a function and a procedure simultaneously:

type f;

const f: int;

function f(x: int): int;

procedure f();

procedure P() { assert f(0) == f(0) && f == f; }

Boogie program verifier finished with 1 verified, 0 errors

Within a table, redeclaration is an error:

function F(x: int): int;

function F(x: int): int;

decl-dup.bpl(2,9): Error: more than one declaration of function name: F

1 name resolution errors detected in decl-dup.bpl

Constants and global variables collide because they share the variable table; the message is more than one declaration of variable name: c.

5.1.2 Declaration order does not matter🔗

Program.Resolve runs in two passes. The first pass calls Register on every top-level declaration, entering all names into the symbol tables. Only then does the second pass resolve the bodies. Consequently a declaration may be used before it is declared, and there is no forward-declaration syntax because none is needed.

axiom (forall x: int :: F(x) == G(x) + 1);

procedure P() { assert F(0) == G(0) + 1; }

function F(x: int): int;

function G(x: int): int;

Boogie program verifier finished with 1 verified, 0 errors

Source order does not even reach the solver: Checker.Setup sorts the declarations by content hash before emitting them, because /normalizeDeclarationOrder defaults to 1.

Type resolution has its own internal order, fixed by Program.ResolveTypes: type constructors first, then type synonyms (by fixed-point iteration, so synonyms may refer to each other in any order), then datatype constructors, then a well-foundedness check on datatypes.

5.1.3 Duplicate declarations: :extern and :ignore🔗

If two declarations of the same kind share a name and exactly one carries {:extern}, it is not an error: the non-:extern declaration wins, and the :extern one has {:ignore} prepended to its attributes. (If both are :extern, one of them is picked arbitrarily.) This exists so that a front end can emit a shared prelude alongside a hand-written override.

ResolutionContext.SelectNonExtern is called from the registration of every kind of named declaration — types, variables (const and var), axioms, functions and procedures — so the rule is uniform across all five namespaces. This whole file resolves without a diagnostic:

type {:extern} T;

type T;

const {:extern} c: int;

const c: int;

procedure {:extern} P();

procedure P();

boogie /noVerify decl-extern-kinds.bpl

Boogie program verifier finished with 0 verified, 0 errors

function {:extern} F(x: int, y: int): int;

function F(x: int): int;

procedure P() { assert F(1) == F(1); }

Boogie program verifier finished with 1 verified, 0 errors

The call F(1) resolves against the one-argument declaration, so the :extern two-argument declaration really is discarded.

{:ignore} can also be written by hand, on any top-level declaration. Declarations carrying it are dropped between the registration pass and the resolution pass, so they contribute nothing:

const c: int;

axiom {:ignore} c == 5;

procedure P() { assert c == 5; }

decl-ignore.bpl(4,17): Error: this assertion could not be proved

Execution trace:

decl-ignore.bpl(4,17): anon0

Boogie program verifier finished with 0 verified, 1 error

5.2 Type declarations🔗

UserDefinedTypes

=

"type"

{ Attribute }

UserDefinedType

{ "," UserDefinedType }

";"

.

UserDefinedType

=

Ident

[ WhiteSpaceIdents ]

[ "=" Type ]

.

WhiteSpaceIdents

=

Ident { Ident }

.

A UserDefinedType without = Type declares a type constructor whose arity is the number of parameter identifiers; the identifiers themselves are discarded (only the count is kept, in TypeCtorDecl.Arity). With = Type it declares a type synonym whose parameters are genuine type variables bound in the body.

type Wicket;

type Barrel a;

type Table k v = [k]v;

type IntTable = Table int int;

type {:tag "x"} A, B c;

const t: Table int bool;

const b: Barrel Wicket;

type Wicket;

type Barrel _;

type Table k v = [k]v;

type IntTable = Table int int;

type {:tag "x"} A;

type {:tag "x"} B _;

const t: Table int bool;

const b: Barrel Wicket;

Boogie program verifier finished with 0 verified, 0 errors

Two things are worth noting in that output. The parameter names of a type constructor are not retained — Barrel a prints as Barrel _. And in the multi-name form type {:tag "x"} A, B c; the attribute list belongs to the whole declaration and is copied to every name, while the parameter list belongs to the individual name: A has arity 0 and B has arity 1. This is easy to misread as declaring three types.

Trap. This is Boogie 2 gives the production TypeConstructor ::= type Attribute* finite? Id Id*;, with a finite keyword marking a type whose carrier may be finite. There is no such keyword any more — and because a type constructor’s parameters are written as whitespace-separated identifiers, the old syntax now parses as something else entirely, with no diagnostic on the declaration itself:

type finite Wicket;

const w: finite Wicket;

decl-finite.bpl(2,16): Error: undeclared type: Wicket (replacing with "bool" to continue resolving)

1 name resolution errors detected in decl-finite.bpl

type finite _;

const w: finite Wicket;

<console>(4,15): Error: undeclared type: Wicket (replacing with "bool" to continue resolving)

1 name resolution errors detected in decl-finite.bpl

(The second position is reported against the printed text, hence <console>(4,15).)

Errors:

type T = [int]T;

decl-type-cycle.bpl(1,5): Error: type synonym could not be resolved because of cycles: T (replacing body with "bool" to continue resolving)

1 name resolution errors detected in decl-type-cycle.bpl

type bv5;

decl-type-bv.bpl(1,5): Error: type name: bv5 is registered for bitvectors

1 name resolution errors detected in decl-type-bv.bpl

Any identifier of the form bv followed by digits is reserved (ResolutionContext.CheckBvNameClashes), for types and for type variables alike.

Type synonyms are expanded away during resolution and reach the solver only through the types they stand for; a type constructor becomes a declare-sort. Neither is ever pruned. See Types for the type system itself, and Algebraic datatypes for datatype.

5.3 Constant declarations🔗

Consts

=

"const"

{ Attribute }

[ "unique" ]

IdsType

( ";" | "uses" "{" { Axiom } "}" )

.

IdsType

=

Idents ":" Type

.

Idents

=

Ident { "," Ident }

.

A constant is an immutable symbol of the given type. As the grammar shows, a const declaration has exactly one type: const a, b, c: T; introduces three constants all of type T, sharing the attributes and the unique marker. There is no way to give several types in one const declaration, and — unlike var — there is no where clause:

const c: int where 0 < c;

decl-const-where.bpl(1,14): error: invalid Consts

1 parse errors detected in decl-const-where.bpl

The keyword order is fixed: attributes, then unique, then the names. const unique {:tag "x"} a: int; is a parse error.

5.3.1 unique🔗

unique makes the constant distinct from every other unique constant of the same type. It is not an axiom in the program text; the prover context collects all unique constants (DeclFreeProverContext.DeclareConstant) and emits a single assertion whose conjuncts are one distinct per type (SMTLibExprLineariser.SMTLibOpLineariser.VisitDistinctOp groups the operands by type and drops any group of fewer than two).

type Color;

const unique red, green, blue: Color;

const other: Color;

procedure P()

{

assert red != green;

assert green != blue;

assert other != red;   // not provable

}

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

Execution trace:

decl-unique.bpl(7,3): anon0

Boogie program verifier finished with 0 verified, 1 error

The grouping is visible in the solver input. For

type Color;

const unique red, green: Color;

const unique zero, one: int;

procedure P() { assert red != green && zero != one; }

(declare-sort T@Color 0)

(declare-fun red () T@Color)

(declare-fun green () T@Color)

(declare-fun zero () Int)

(declare-fun one () Int)

(assert (and (distinct red green)(distinct zero one))

)

Two consequences follow, and both surprise people.

First, unique says nothing about values that are not unique constants. A unique int constant is not distinct from 0:

const unique a: int;

const unique b: int;

procedure P()

{

assert a != b;    // provable

assert a != 0;    // not provable: 0 is not a unique constant

}

decl-unique-int.bpl(7,3): Error: this assertion could not be proved

Execution trace:

decl-unique-int.bpl(6,3): anon0

Boogie program verifier finished with 0 verified, 1 error

Second, unique on constants of an interpreted type is an easy way to make the whole program inconsistent, because the distinct assertion is unconditional background knowledge:

const unique a: int;

const unique b: int;

axiom a == 3;

axiom b == 3;

procedure P()

{

assert false;   // provable: the axioms contradict uniqueness

}

Boogie program verifier finished with 1 verified, 0 errors

5.3.2 uses clauses on constants🔗

Instead of a semicolon, a constant declaration may end in a uses block containing axioms. The axioms are ordinary top-level axioms — they are added to the program exactly as if written separately — but the declaration also records them, which gives the pruner an edge from the constant to each axiom. What that edge does is shown under uses clauses and pruning in the section on function declarations below.

const {:tag "x"} unique a, b: int uses {

axiom a < b;

axiom 0 <= a;

}

Printing this program back out shows how the axioms are attached to each name of the declaration:

const {:tag "x"} unique a: int

uses {

axiom a < b;

axiom 0 <= a;

}

const {:tag "x"} unique b: int

uses {

axiom a < b;

axiom 0 <= a;

}

Boogie program verifier finished with 0 verified, 0 errors

5.4 Orders: extends, complete and <:🔗

Section 10 of This is Boogie 2 describes a built-in partial order <:, available at every type, together with special syntax on constant declarations for placing constants in that order. None of this exists any more. The operator <:, the extends/complete order specifications, and the entire OrderingAxiomBuilder were deleted from Boogie in January 2023 (commit 88cd431, released in 2.16.1). This is the single largest divergence between the paper and the current tool in the area of declarations, and since the feature is still widely cited it is documented here in full.

5.4.1 What used to exist🔗

Until 2.16.0, Consts had an extra clause:

OrderSpec

=

"extends"

[

[ "unique" ] Ident

{ "," [ "unique" ] Ident }

]

[ "complete" ]

.

(Note that the paper writes this clause with <:; the implementation always spelled it extends. The operator <: existed separately, as a RelOp producing BinaryOperator.Opcode.Subtype.)

Today both are parse errors:

type Wicket;

const unique a, b: Wicket;

const unique c: Wicket extends a, b complete;

decl-order-gone.bpl(3,33): error: invalid Consts

1 parse errors detected in decl-order-gone.bpl

type Wicket;

const unique puny: Wicket;

axiom (forall w: Wicket :: puny <: w);

decl-subtype-gone.bpl(3,34): error: invalid UnaryExpression

decl-subtype-gone.bpl(3,37): error: ";" expected

2 parse errors detected in decl-subtype-gone.bpl

5.4.2 The axioms the feature generated🔗

Because the encoding is still useful, and because translations that targeted Boogie 2 need to be ported, here is exactly what OrderingAxiomBuilder emitted, transcribed into present-day Boogie with Sub(x, y) standing for x <: y.

The order itself was set up once per program (OrderingAxiomBuilder.Setup), polymorphically over all types:

axiom (forall x: Wicket :: Sub(x, x));

axiom (forall x, y, z: Wicket :: {Sub(x, y), Sub(y, z)}

Sub(x, y) && Sub(y, z) ==> Sub(x, z));

axiom (forall x, y: Wicket :: {Sub(x, y), Sub(y, x)}

Sub(x, y) && Sub(y, x) ==> x == y);

For a constant c declared extends p1, ..., pn (GenParentConstraints), three families of axioms were generated: each parent is a proper ancestor; nothing lies strictly between c and a parent; and the ancestors of c are exactly c together with the ancestors of its parents.

For a constant c declared complete (GenCompleteChildrenConstraints) one further axiom said that everything below c is c itself or lies below one of the constants that declared c as a parent. Note that this axiom depends on all the constant declarations in the program, so it was generated last, after the whole program had been seen.

For a parent edge marked unique (GenUniqueParentConstraint) an auxiliary function oneStep was introduced and everything below the child was required to map back to that child.

5.4.3 Worked example: extends🔗

The paper’s small example (the paper spells it <: a, b; below it is written the way Boogie 2.16.0 accepted it)

const unique a, b: Wicket;

const unique c: Wicket extends a, b;

becomes, in current Boogie:

type Wicket;

// The partial order itself.  Boogie no longer supplies one.

function Sub(Wicket, Wicket): bool;

axiom (forall x: Wicket :: Sub(x, x));

axiom (forall x, y, z: Wicket :: {Sub(x, y), Sub(y, z)}

Sub(x, y) && Sub(y, z) ==> Sub(x, z));

axiom (forall x, y: Wicket :: {Sub(x, y), Sub(y, x)}

Sub(x, y) && Sub(y, x) ==> x == y);

const unique a, b, c: Wicket;

// "const unique c: Wicket extends a, b;"

axiom c != a && Sub(c, a);

axiom c != b && Sub(c, b);

axiom (forall w: Wicket :: {Sub(c, w), Sub(w, a)}

Sub(c, w) && Sub(w, a) ==> c == w || a == w);

axiom (forall w: Wicket :: {Sub(c, w), Sub(w, b)}

Sub(c, w) && Sub(w, b) ==> c == w || b == w);

axiom (forall w: Wicket :: {Sub(c, w)}

Sub(c, w) ==> c == w || Sub(a, w) || Sub(b, w));

procedure P(w: Wicket)

{

assert Sub(c, a) && Sub(c, b);

assert Sub(c, w) ==> w == c || Sub(a, w) || Sub(b, w);

assert !Sub(a, b);

}

Boogie program verifier finished with 1 verified, 0 errors

The last assertion shows that the directness axioms have teeth. If Sub(a, b) held, then since Sub(c, a) also holds, a would lie between c and its parent b; the directness axiom for that edge would then force c == a or b == a, and both are ruled out by unique.

5.4.4 Worked example: complete🔗

The paper’s larger example, again in the implementation’s spelling

const unique a: Wicket extends complete;

const unique b: Wicket;

const unique c: Wicket extends a, b complete;

const unique d: Wicket extends c;

const unique e: Wicket;

transcribes as follows. extends with an empty parent list means "no parents", which turns the ancestor axiom into "the only thing above a is a".

type Wicket;

function Sub(Wicket, Wicket): bool;

axiom (forall x: Wicket :: Sub(x, x));

axiom (forall x, y, z: Wicket :: {Sub(x, y), Sub(y, z)}

Sub(x, y) && Sub(y, z) ==> Sub(x, z));

axiom (forall x, y: Wicket :: {Sub(x, y), Sub(y, x)}

Sub(x, y) && Sub(y, x) ==> x == y);

const unique a, b, c, d, e: Wicket;

// const unique a: Wicket extends complete;      -- no parents

axiom (forall w: Wicket :: {Sub(a, w)} Sub(a, w) ==> a == w);

// ... and a's only declared child is c

axiom (forall w: Wicket :: {Sub(w, a)} Sub(w, a) ==> w == a || Sub(w, c));

// const unique c: Wicket extends a, b complete;

axiom c != a && Sub(c, a);

axiom c != b && Sub(c, b);

axiom (forall w: Wicket :: {Sub(c, w), Sub(w, a)}

Sub(c, w) && Sub(w, a) ==> c == w || a == w);

axiom (forall w: Wicket :: {Sub(c, w), Sub(w, b)}

Sub(c, w) && Sub(w, b) ==> c == w || b == w);

axiom (forall w: Wicket :: {Sub(c, w)}

Sub(c, w) ==> c == w || Sub(a, w) || Sub(b, w));

// ... and c's only declared child is d

axiom (forall w: Wicket :: {Sub(w, c)} Sub(w, c) ==> w == c || Sub(w, d));

// const unique d: Wicket extends c;

axiom d != c && Sub(d, c);

axiom (forall w: Wicket :: {Sub(d, w), Sub(w, c)}

Sub(d, w) && Sub(w, c) ==> d == w || c == w);

axiom (forall w: Wicket :: {Sub(d, w)} Sub(d, w) ==> d == w || Sub(c, w));

procedure P()

{

assert Sub(d, a);              // transitivity through c

assert !Sub(a, b);             // a has no proper ancestors at all

assert Sub(e, a) ==> Sub(e, d);  // completeness of a, then of c

assert !Sub(b, c);             // c is strictly below b

}

Boogie program verifier finished with 1 verified, 0 errors

The third assertion illustrates what complete does and does not buy you. a is complete and its only declared child is c, and c is complete and its only declared child is d; but d is not complete, so the undeclared wicket e may still sit below d and hence below a. complete closes one level of the hierarchy, not the whole subtree.

5.4.5 Worked example: unique parent edges🔗

const unique r: Wicket;

const unique s, t: Wicket extends unique r;

type Wicket;

function Sub(Wicket, Wicket): bool;

function oneStep(Wicket, Wicket): Wicket;

axiom (forall x: Wicket :: Sub(x, x));

axiom (forall x, y, z: Wicket :: {Sub(x, y), Sub(y, z)}

Sub(x, y) && Sub(y, z) ==> Sub(x, z));

axiom (forall x, y: Wicket :: {Sub(x, y), Sub(y, x)}

Sub(x, y) && Sub(y, x) ==> x == y);

const unique r, s, t: Wicket;

// const unique s, t: Wicket extends unique r;

axiom s != r && Sub(s, r);

axiom (forall w: Wicket :: {Sub(s, w), Sub(w, r)}

Sub(s, w) && Sub(w, r) ==> s == w || r == w);

axiom (forall w: Wicket :: {Sub(s, w)} Sub(s, w) ==> s == w || Sub(r, w));

axiom (forall w: Wicket :: {Sub(w, s)} Sub(w, s) ==> oneStep(r, w) == s);

axiom t != r && Sub(t, r);

axiom (forall w: Wicket :: {Sub(t, w), Sub(w, r)}

Sub(t, w) && Sub(w, r) ==> t == w || r == w);

axiom (forall w: Wicket :: {Sub(t, w)} Sub(t, w) ==> t == w || Sub(r, w));

axiom (forall w: Wicket :: {Sub(w, t)} Sub(w, t) ==> oneStep(r, w) == t);

procedure P(x: Wicket, y: Wicket)

{

assert Sub(x, s) && Sub(y, t) ==> x != y;

}

Boogie program verifier finished with 1 verified, 0 errors

This is exactly the disjointness property the paper claims for unique edges: the sub-dags below s and below t do not overlap. The oneStep function is the trick that makes it work — anything below s maps to s and anything below t maps to t, so a shared element would force s == t.

5.4.6 Migration advice🔗

If you are porting a program written against Boogie 2’s orders:

• Declare your own relation. A binary function returning bool is the usual choice; if you need it at several types, make it polymorphic (function Sub<T>(T, T): bool;) or declare one per type.

• Add reflexivity, transitivity and antisymmetry yourself. Boogie no longer supplies them, and no solver-level partial-order support is used any more.

• Keep the triggers shown above. The old builder attached exactly these triggers, and they are what keeps the transitivity axiom from flooding the solver.

• const unique still exists and is unaffected; only the extends / complete suffix is gone.

5.5 Function declarations🔗

Function

=

[ "revealed" ]

"function" { Attribute } Ident

[ TypeParams ]

"("

[ VarOrType { "," VarOrType } ] ")"

(

"returns" "(" VarOrType ")"

|

":" Type

)

( "{" Expression "}" [ "uses" "{" { Axiom } "}" ]

| "uses" "{" { Axiom } "}"

| ";"

)

.

VarOrType

=

{ Attribute }

Type

[ ":" Type ]

.

A function is a mathematical, state-independent, total map from its arguments to a result. It may not mention global variables:

var g: int;

function F(x: int): int { x + g }

decl-fun-global.bpl(2,30): Error: cannot refer to a global variable in this context: g

1 name resolution errors detected in decl-fun-global.bpl

It may mention constants and other functions freely.

5.5.1 Signatures🔗

The result type may be written either as returns (T) (the paper’s form) or as : T (shorter, and what /print always emits). returns also permits naming the result, as in returns (r: int), but the name is not usable anywhere — the body cannot refer to it and /print drops it.

Argument declarations are unusual. VarOrType parses a Type, optionally followed by : Type; the first form is an unnamed argument and the second is a named one. After parsing, if any argument was named, the parser walks the list from right to left and repairs unnamed arguments: an unnamed argument takes its type from the argument to its right, and its own parsed "type", if it was a bare identifier, becomes its name.

type Color;

function f(a, b: int): int;

function g(int, bool) returns (int);

function h(x: int) returns (r: int);

function k(Color, b: int): int;

type Color;

function f(a: int, b: int) : int;

function g(int, bool) : int;

function h(x: int) : int;

function k(Color: int, b: int) : int;

Boogie program verifier finished with 0 verified, 0 errors

So f(a, b: int) is the C-like shorthand for two int arguments — this is not in the paper and is easy to miss. And the last line is the trap: in k(Color, b: int) the identifier Color is not read as a type. It becomes the name of an argument whose type is taken from b, so k takes two ints, and the type Color does not appear in the signature at all. No warning is issued.

The repair only fires when at least one argument is named. g(int, bool) above keeps both arguments unnamed. And the repair can fail:

• function h(x: int, bool): bool; — error: the type of the last parameter is unspecified, because the rightmost argument is unnamed and there is nothing to its right.

• function k(int, y: bool): bool; — error: expecting an identifier as parameter name, because int is a built-in type token, not an identifier, so it cannot be turned into a name.

5.5.2 Polymorphism🔗

Type parameters are written between the name and the argument list, and are bound over the argument and result types.

Every type parameter must occur somewhere in the signature:

function OnlyResult<A>(x: int): A;         // fine

function Unused<A, B>(a: A): A { a }       // B occurs nowhere

decl-fun-typeparam.bpl(2,9): Error: type variable must occur in function arguments: B

1 name resolution errors detected in decl-fun-typeparam.bpl

The paper differs here. Section 3 states that "every type identifier introduced in TypeArgs must be used ... somewhere among the types of the function’s arguments". The implementation (Type.CheckBoundVariableOccurrences, called from Function.Resolve) checks the in-parameters and the out-parameter, so a type parameter that occurs only in the result type is accepted. Such a function needs an explicit type coercion at every call site, since its type argument cannot be inferred from the actuals:

function OnlyResult<A>(x: int): A;

procedure P() { assert OnlyResult(3): int == OnlyResult(3): int; }

Boogie program verifier finished with 1 verified, 0 errors

5.5.3 Functions without bodies🔗

function F(...): T; declares an uninterpreted symbol. Everything known about it must come from axioms.

5.5.4 Function bodies and the axiom they generate🔗

A body { E } on a function with no :inline or :define attribute is sugar. Function.CreateDefinitionAxiom turns it into an axiom of the form

axiom (forall <typeparams> args :: { F(argIds): ResultType } F(argIds): ResultType == E);

with the call itself as the sole trigger, and the coercion : ResultType present so that type parameters occurring only in the result are pinned down. Arguments that were left unnamed get the fresh names _0, _1, ... . If the function has no arguments and no type parameters, no quantifier is generated at all.

function Twice(x: int): int { x + x }

function {:inline} Thrice(x: int): int { x + x + x }

function {:define} Quad(x: int): int { 4 * x }

function Five(): int { 5 }

function Id<T>(x: T): T { x }

function Twice(x: int) : int

uses {

axiom (forall x: int :: { Twice(x): int } Twice(x): int == x + x);

}

function {:inline} Thrice(x: int) : int

{

x + x + x

}

function {:define} Quad(x: int) : int

{

4 * x

}

function Five() : int

uses {

axiom Five(): int == 5;

}

function Id<T>(x: T) : T

uses {

axiom (forall<T> x: T :: { Id(x): T } Id(x): T == x);

}

Boogie program verifier finished with 0 verified, 0 errors

Notice that the generated axiom is printed inside a uses block: the definition axiom is automatically registered as a definition axiom of the function, so it is reachable from the function for pruning purposes and does not need an explicit uses clause.

Attribute leakage. CreateDefinitionAxiom is handed the function’s own attribute list and attaches it to the generated forall. A function declared function {:define false} f(x: int): bool { x > 0 } generates axiom (forall x: int :: {:define false} { f(x): bool } f(x): bool == (x > 0)); — the attribute ends up on the quantifier. For quantifier attributes such as :weight this is useful; for others it is noise.

5.5.5 Recursion🔗

Nothing checks that a function body is well founded. Recursive and mutually recursive definitions are accepted and produce exactly the axiom above:

function Fact(n: int): int { if n <= 0 then 1 else n * Fact(n - 1) }

function IsEven(n: int): bool { if n == 0 then true else IsOdd(n - 1) }

function IsOdd(n: int): bool { if n == 0 then false else IsEven(n - 1) }

procedure P()

{

assert Fact(3) == 6;

assert IsEven(4);

}

Boogie program verifier finished with 1 verified, 0 errors

The flip side is that an ill-founded definition is simply an inconsistent axiom, and Boogie will happily use it:

function F(x: int): int { F(x) + 1 }

procedure P()

{

assert 1 == 2;   // provable: the definition of F is inconsistent

}

Boogie program verifier finished with 1 verified, 0 errors

Nothing warns you. The program has no models at all, so every implementation in it verifies. Compare the well-founded case, where the definition axiom is satisfiable and the false assertion is correctly rejected:

function Fact(n: int): int { if n <= 0 then 1 else n * Fact(n - 1) }

procedure P()

{

assert Fact(3) == 6;

assert 1 == 2;

}

decl-fun-rec2.bpl(6,3): Error: this assertion could not be proved

Execution trace:

decl-fun-rec2.bpl(5,3): anon0

Boogie program verifier finished with 0 verified, 1 error

If a definition is meant to be recursive, it is worth asserting false somewhere once to confirm it is not vacuous.

5.5.6 :inline🔗

{:inline} stores the body in Function.Body instead of generating an axiom, and the body is substituted into the verification condition at translation time (Boogie2VCExpr.ApplyExpansion). The function symbol never reaches the solver.

function {:inline} Abs(x: int): int { if x < 0 then -x else x }

procedure P(y: int)

{

assert Abs(y) >= 0;

}

boogie /proverLog:inl.smt2 /env:0 decl-fun-inline.bpl

(assert (not

(=> (= (ControlFlow 0 0) 3) (let ((anon0_correct  (=> (= (ControlFlow 0 2) (- 0 1)) (>= (ite (< y 0) (- 0 y) y) 0))))

(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 3) 2) anon0_correct)))

PreconditionGeneratedEntry_correct)))

))

Inlining is unconditional — no trigger is involved — which is why :inline is the reliable choice for small definitions. It works for polymorphic functions.

:inline takes an optional Boolean argument: {:inline true} is the same as {:inline}, while {:inline false} is treated as absent, so the body becomes an ordinary definition axiom — and the attribute is then copied onto the generated quantifier:

function {:inline false} F(x: int): int { x + 1 }

function {:inline true} G(x: int): int { x + 1 }

function {:inline false} F(x: int) : int

uses {

axiom (forall x: int :: {:inline false} { F(x): int } F(x): int == x + 1);

}

function {:inline true} G(x: int) : int

{

x + 1

}

Boogie program verifier finished with 0 verified, 0 errors

A non-Boolean argument is rejected:

function {:inline 3} F(x: int): int { x + 1 }

decl-inline-nonbool.bpl(1,21): Error: Parameter to :inline attribute on a function must be Boolean

5.5.7 :define🔗

{:define} keeps the function as a symbol but emits it to the solver as an SMT-LIB define-fun rather than a declare-fun plus axiom.

function {:define} Abs(x: int): int { if x < 0 then -x else x }

procedure P(y: int)

{

assert Abs(y) >= 0;

}

boogie /proverLog:def.smt2 /env:0 decl-fun-define.bpl

(define-fun Abs ((x Int) ) Int (ite (< x 0) (- 0 x) x))

:define must be monomorphic:

function {:define} Id<T>(x: T): T { x }

decl-fun-poly-define.bpl(1,39): error: function with :define attribute has to be monomorphic

1 parse errors detected in decl-fun-poly-define.bpl

Surprise. Because a define-fun is a macro, a defined function never produces a symbol that a quantifier can trigger on. If a :define function is the only thing that would have created the term another axiom’s trigger needs, that axiom never fires:

function {:define} Double(x: int): int { 3 * x - x }

function g(int): int;

function k(int): int;

axiom (forall x: int :: Double(x) == g(x));

axiom (forall x: int :: { g(x) } g(x) < k(x));

procedure P(b: int, c: int)

{

if (*) {

assert Double(b) < k(b);   // not provable: no g(b) term is ever created

} else {

assert g(c) == 2 * c;      // mentions g(c) explicitly

assert Double(c) < k(c);   // now provable

}

}

decl-fun-define-trigger.bpl(11,5): Error: this assertion could not be proved

Execution trace:

decl-fun-define-trigger.bpl(10,3): anon0

decl-fun-define-trigger.bpl(11,5): anon3_Then

Boogie program verifier finished with 0 verified, 1 error

The same program with Double declared as a plain-bodied function verifies both branches, because there the definition axiom’s trigger Double(b) creates the g(b) term. Test/functiondefine/fundef7.bpl in the Boogie source is the upstream version of this test.

5.5.8 Attribute restrictions and the call-cycle check🔗

FunctionDependencyChecker runs after type checking and enforces four rules:

• :inline’s argument, if present, must be Boolean.

• :inline and :define may not both be present (the parser also rejects this, earlier and with a different message).

• :inline and :define functions must have a body.

• The call graph restricted to :inline and :define functions must be acyclic.

function {:inline} F(x: int): int;

function {:define} G(x: int): int;

decl-fun-attr-errors.bpl(1,19): Error: Function with :inline attribute must have a body

decl-fun-attr-errors.bpl(2,19): Error: Function with :define attribute must have a body

function {:define} foo(x: int): int { foo2(x) + 1 }

function {:inline} foo2(x: int): int { foo(x) + 2 }

decl-fun-cycle.bpl(1,19): Error: Call cycle detected among functions: foo, foo2

The dependency graph relates only :inline/:define functions to :inline/:define functions — FunctionDependencyChecker.VisitFunction descends into a body only when the enclosing function carries one of the two attributes, and VisitNAryExpr records an edge only when the callee does — so an ordinary function in the middle of the cycle breaks it as far as the checker is concerned:

function {:define} foo(x: int): int { bar(x) + 1 }

function bar(x: int): int { foo2(x) }

function {:inline} foo2(x: int): int { foo(x) + 2 }

procedure P() { assert 1 == 2; }

Boogie program verifier finished with 1 verified, 0 errors

The cycle still exists — it is just routed through an axiom rather than through a macro expansion — and the resulting axiom set is inconsistent, exactly like the ill-founded definition above. The checker is silent about it.

5.5.9 :builtin and :bvbuiltin🔗

{:builtin "s"} and {:bvbuiltin "s"} replace the function symbol with the raw SMT-LIB symbol s in the solver input. :bvbuiltin takes precedence when both are present, and is special-cased for sign_extend n / zero_extend n, which are emitted as (_ sign_extend n).

function {:builtin "abs"} Abs(x: int): int;

procedure P(y: int)

{

assert Abs(y) >= 0;

}

(=> (= (ControlFlow 0 0) 3) (let ((anon0_correct  (=> (= (ControlFlow 0 2) (- 0 1)) (>= (abs y) 0))))

with no declaration of Abs anywhere. Boogie does not check that s exists, that its arity matches, or that its sorts match; a wrong string produces a solver error rather than a Boogie error. See :bvbuiltin and the SMT-LIB bitvector operations and Reaching the string theory: :builtin for the usable symbols.

5.5.10 uses clauses and pruning🔗

A function may end in a uses block, exactly as a constant may, and may have both a body and a uses block (in that order). The axioms are ordinary top-level axioms plus an edge from the function for the pruner.

With /prune:1, only the declarations reachable from the verification condition are sent to the solver (the dependency graph and how to inspect the result are in Pruning; pruning is off by default). Axioms have no incoming edges by default, so an axiom that is not in anybody’s uses clause is reachable only through the triggers of its quantifiers. A uses clause is the way to say "this axiom belongs to that symbol":

const four: int;

const Gate: bool uses {

axiom four == 4;

}

function Consumer(x: int): int;

function Producer(x: int): bool uses {

axiom (forall x: int :: Consumer(x) == 3);

}

procedure Reaches()

requires Producer(2);

requires Gate;

ensures Consumer(4) == 3;

ensures four == 4;

{

}

procedure DoesNotReach()

ensures Consumer(4) == 3;

ensures four == 4;

{

}

boogie /prune:1 /errorTrace:0 decl-uses.bpl

decl-uses.bpl(25,1): Error: a postcondition could not be proved on this return path

decl-uses.bpl(22,3): Related location: this is the postcondition that could not be proved

decl-uses.bpl(25,1): Error: a postcondition could not be proved on this return path

decl-uses.bpl(23,3): Related location: this is the postcondition that could not be proved

Boogie program verifier finished with 1 verified, 2 errors

Reaches mentions Producer and Gate, so both uses axioms are kept. DoesNotReach mentions neither, so both are pruned — even though it mentions four and Consumer, which are only the targets of the axioms, not their owners.

Pruning is off by default. Without /prune:1 the same program reports

Boogie program verifier finished with 2 verified, 0 errors

5.5.11 revealed🔗

The optional revealed keyword before function sets Function.AlwaysRevealed. RevealedState.IsRevealed short-circuits on that flag, so such a function is exempt from all hiding — not only hide * but also an explicit hide G;, which is silently a no-op.

function F(x: int): int uses {

hideable axiom (forall x: int :: {F(x)} F(x) == x + 1);

}

revealed function G(x: int): int uses {

hideable axiom (forall x: int :: {G(x)} G(x) == x + 2);

}

procedure P()

{

hide *;

assert G(0) == 2;   // G is 'revealed', so 'hide *' does not hide it

assert F(0) == 1;   // F is hidden: not provable

}

boogie /prune:1 /errorTrace:0 decl-hideable.bpl

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

Boogie program verifier finished with 0 verified, 1 error

Hiding requires pruning. Without /prune:1 the same program reports

Boogie program verifier finished with 1 verified, 0 errors

because hide and reveal are implemented inside the pruner. See Hiding and revealing function definitions for the scoping rules of hide, reveal, push and pop, and hide, reveal, push and pop for the statement grammar.

5.6 Axiom declarations🔗

Axiom

=

[ "hideable" ]

"axiom"

{ Attribute }

Proposition ";"

.

Proposition

=

Expression

.

An axiom is a formula assumed to hold in every state. Axioms may appear at top level, or inside the uses block of a constant or function — the two are logically identical; the uses form only adds a pruning edge.

Three restrictions are enforced:

var g: int;

axiom g == 0;

decl-axiom-errors.bpl(2,6): Error: cannot refer to a global variable in this context: g

1 name resolution errors detected in decl-axiom-errors.bpl

const c: int;

axiom c + 1;

decl-axiom-type.bpl(2,0): Error: axioms must be of type bool

1 type checking errors detected in decl-axiom-type.bpl

and old(...) is rejected as well, since an axiom is not a two-state context. What an axiom may mention is constants, functions, datatype constructors, and its own bound variables.

As the paper notes, inconsistent axioms are legal and make every implementation vacuously correct. axiom false; is the extreme case; const unique on interpreted types and ill-founded function definitions are the two ways this happens by accident.

5.6.1 hideable🔗

hideable sets Axiom.CanHide. In the pruner (Pruner.GetLiveDeclarations), an edge from a function to a hideable axiom is not traversed when that function is hidden at the assertion being verified. Non-hideable axioms can never be hidden. hideable works on top-level axioms too, not just those in uses blocks — there the incoming edge comes from the axiom’s triggers:

function F(x: int): int;

hideable axiom (forall x: int :: {F(x)} F(x) == x + 1);

procedure P()

{

hide F;

assert F(1) == 2;   // hidden: not provable

}

procedure Q()

{

assert F(1) == 2;   // visible

}

boogie /prune:1 /errorTrace:0 decl-hideable-toplevel.bpl

decl-hideable-toplevel.bpl(7,3): Error: this assertion could not be proved

Boogie program verifier finished with 1 verified, 1 error

Surprise. The hidden/revealed state is computed once per verification condition, by merging (unioning) the states that reach every assertion in it. So a hide that comes after an assertion needing the axiom silently has no effect on the assertions that follow it:

function F(x: int): int;

hideable axiom (forall x: int :: {F(x)} F(x) == x + 1);

procedure P()

{

assert F(0) == 1;

hide F;

assert F(1) == 2;   // one would expect this to fail

}

boogie /prune:1 /errorTrace:0 decl-hide-merge.bpl

Boogie program verifier finished with 1 verified, 0 errors

boogie /prune:1 /vcsSplitOnEveryAssert /errorTrace:0 decl-hide-merge.bpl

decl-hide-merge.bpl(8,3): Error: this assertion could not be proved

Boogie program verifier finished with 0 verified, 1 error

5.6.2 Attributes on axioms🔗

{:name "s"} gives the axiom a name. The name is used for nothing except uniqueness checking — ResolutionContext.AddAxiom records it in a dictionary that is never read again:

const c: int;

axiom {:name "c_range"} 0 < c;

axiom {:name "c_range"} c < 10;

decl-axiom-name.bpl(3,22): Error: more than one declaration of axiom name: c_range

1 name resolution errors detected in decl-axiom-name.bpl

{:id "s"} is the attribute that actually does something: with /trackVerificationCoverage the axiom becomes a named assumption in the VC so that coverage reporting can tell whether it was needed.

{:include_dep} gives the axiom an incoming pruning edge from every declaration it references, which is the blunt instrument for migrating an existing program to /prune:1:

const four: int;

const five: int;

axiom four == 4;

axiom {:include_dep} five == 5;

procedure P()

ensures four == 4;   // pruned away: nothing points to this axiom

{

}

procedure Q()

ensures five == 5;   // kept: {:include_dep} gives the axiom an edge from 'five'

{

}

boogie /prune:1 /errorTrace:0 decl-include-dep.bpl

decl-include-dep.bpl(10,1): Error: a postcondition could not be proved on this return path

decl-include-dep.bpl(8,3): Related location: this is the postcondition that could not be proved

Boogie program verifier finished with 1 verified, 1 error

{:keep} (undocumented in /attrHelp) makes a declaration a pruning root, so it is never pruned regardless of reachability. Replacing axiom four == 4; above with

axiom {:keep} four == 4;

makes P verify too:

Boogie program verifier finished with 2 verified, 0 errors

{:ignore} drops the axiom entirely, as shown earlier.

5.6.3 :ctor no longer exists🔗

The paper does not mention :ctor, but Boogie 2.x used axiom {:ctor "T"} ... as a hint telling the monomorphizer which type constructor a polymorphic axiom should be instantiated for. It was introduced in 2020 and removed in 2023 along with the rewrite of Monomorphization.cs. Boogie never rejects unknown attributes, so writing it today is silently ignored:

type Ref;

function F<T>(x: T): int;

axiom {:ctor "Ref"} (forall x: Ref :: F(x) == 0);

procedure P(r: Ref) { assert F(r) == 0; }

Boogie program verifier finished with 1 verified, 0 errors

The same is true of any misspelled attribute anywhere in a Boogie program: there is no check, so a typo in an attribute name is silently a no-op.

5.7 Global variable declarations🔗

GlobalVars

=

"var"

{ Attribute }

IdsTypeWheres ";"

.

IdsTypeWheres

=

IdsTypeWhere { "," IdsTypeWhere }

.

IdsTypeWhere

=

Idents ":" Type

[ "where" Expression ]

.

A var declaration at top level introduces mutable global variables. Unlike const, one var declaration may introduce groups of different types, each group with its own where clause; the attribute list applies to all of them.

var {:hint} a, b: int where a < b, c: bool;

var {:hint} a: int where a < b;

var {:hint} b: int where a < b;

var {:hint} c: bool;

Boogie program verifier finished with 0 verified, 0 errors

Note that the where clause is copied verbatim to each name in its group — it is not "one clause per variable" but "the same clause on every variable of the group". Per-name attributes are not allowed here: GlobalVars uses IdsTypeWheres, not the AttributesIdsTypeWheres form used for procedure formals and bound variables, so var a: int, {:x} b: int; is a parse error.

The where expression must be of type bool, may refer to any constant, function and global variable (including ones declared later, and including the variable being declared), and may not use old:

var x: int where x == old(x);

decl-var-where-old.bpl(1,22): Error: old expressions allowed only in two-state contexts

1 name resolution errors detected in decl-var-where-old.bpl

5.7.1 What a where clause means🔗

A where clause is only ever assumed, never checked. Boogie inserts assume commands for it at exactly two kinds of place:

• At the entry of every implementation, for every global variable that has a where clause — see VerificationConditionGenerator.PassifyImpl, which collects the clauses of program.GlobalVariables and injects them before the first block. This happens whether or not the implementation mentions the variable.

• Immediately after every havoc of the variable, with the new incarnation substituted in (ConditionGeneration.TurnIntoPassiveCmd). Because a call desugars into a havoc of the callee’s modifies set, this covers call sites too.

Nothing else re-establishes it. In particular an ordinary assignment does not:

var x: int where 0 <= x;

procedure P()

modifies x;

{

assert 0 <= x;      // assumed on entry

x := -1;

assert 0 <= x;      // NOT re-assumed after assignment: fails

havoc x;

assert 0 <= x;      // re-assumed after havoc

}

decl-var-where.bpl(8,3): Error: this assertion could not be proved

Execution trace:

decl-var-where.bpl(6,3): anon0

Boogie program verifier finished with 0 verified, 1 error

and a call does:

var x: int where 0 <= x;

procedure Q();

modifies x;

procedure P()

modifies x;

{

x := -1;

call Q();

assert 0 <= x;      // re-assumed at the call, because Q modifies x

}

Boogie program verifier finished with 1 verified, 0 errors

5.7.2 The where-clause hazard🔗

Since a where clause is an assumption that is never discharged, it is a free precondition on every procedure and a free postcondition on every call. That combination lets a where clause "prove" something false about the program it is meant to describe:

var x: int where x == 0;

procedure Set()

modifies x;

{

x := 1;          // no postcondition mentions x

}

procedure Main()

modifies x;

{

call Set();

assert x == 0;   // "proved", although Set leaves x == 1

}

Boogie program verifier finished with 2 verified, 0 errors

Both procedures verify. Set is allowed to leave x at 1 because nothing checks the where clause at exit; Main is allowed to conclude x == 0 because the call havocs x and then re-assumes the clause.

The rule of thumb is that a where clause is only safe when it states a type-like invariant that every possible value of the variable satisfies by construction — typically a range restriction coming from a source language’s type system, which the front end also guarantees at every assignment. Anything that a statement could break belongs in requires/ensures/invariant instead. In the extreme, var x: int where false; makes every implementation vacuously correct.

5.7.3 Other notes on globals🔗

• Global variables are never pruned (Pruner.GetLiveDeclarations keeps everything that is not a Constant, Axiom or Function).

• {:assumption} variables must be of type bool and may not have a where clause (both checks live on Variable, so they fire on globals too); they are a local-variable feature, described in Attributes.

• {:existential true} is honoured on a const, not on a var: Houdini’s CollectExistentialConstants iterates program.Constants, and Houdini.ApplyAssignment filters OfType<Constant>(). With const {:existential true} b: bool; and /contractInfer /printAssignment Boogie reports Assignment computed by Houdini: and b = False; on a var the attribute has no effect and the variable stays an ordinary unconstrained global.

• Which globals an implementation may assign is governed by the enclosing procedure’s modifies clause; see modifies.

5.8 Summary: ordering and recursion rules🔗

• Top-level order is irrelevant. All names are registered before any declaration is resolved, and the declarations are re-sorted by content hash before reaching the solver.

• Type synonyms may refer to each other in any order; cycles are detected and reported.

• Axioms may refer to any constant or function, declared anywhere.

• Ordinary functions with bodies may be recursive and mutually recursive. Nothing checks well-foundedness; an ill-founded definition is an inconsistent axiom.

• :inline and :define functions must form an acyclic call graph among themselves. An ordinary function on the cycle defeats the check.

• Datatypes must be well founded; this is checked (Program.CheckDatatypesWellFounded).

• Duplicate names within a namespace are an error, unless at least one of the two declarations is {:extern}.

5.9 Divergences from This is Boogie 2🔗

Collected for reference; each is discussed above.

• Orders are gone. The <: operator and the extends/complete order specifications on constants (paper section 10) were removed in Boogie 2.16.1. The paper’s OrderSpec grammar uses <: where the implementation used the keyword extends.

• Type constructors have no finite modifier. The paper’s TypeConstructor ::= type Attribute* finite? Id Id*; includes a finite keyword; the current grammar and scanner have no such token, and the syntax now means something else entirely — see Type declarations above.

• Type parameters may occur only in the result type of a function. The paper requires occurrence among the arguments.

• Result types may be written : T, not only returns (T); result parameters may be named but the name is unused.

• The f(a, b: int) argument shorthand is not described in the paper.

• uses clauses, hideable, revealed, :inline, :define, :builtin, :extern, :ignore, :include_dep and :keep all postdate the paper.

• :ctor on axioms existed between 2020 and 2023 and is now silently ignored.