1 Introduction🔗

1.1 This reference and This is Boogie 2🔗

The canonical description of the language is K. Rustan M. Leino’s This is Boogie 2 (manuscript KRML 178, working draft of 24 June 2008). It remains the best account of why Boogie is shaped the way it is: the trace semantics, the design of the type system, the reasoning behind where clauses, free specifications and the caller/callee split. This reference does not replace it and does not try to re-derive it. Read the paper for the design; read this for what the tool does.

The paper is now old enough that a reader who follows it literally will write programs that do not parse. Three of its sections describe features that have since been removed, and a good deal of the language has been added since. The rule adopted throughout this reference is simple:

The implementation is the authority. The grammar file decides syntax, the C# source decides behaviour, and the paper decides design intent. Where the paper and the tool disagree, the tool wins and the difference is stated explicitly.

Every chapter states its divergences explicitly, in almost every case in a closing section called Divergences from This is Boogie 2. (The exception is Command-line reference, which the paper does not touch at all; it says so in its own opening.)

1.2 What the paper describes that no longer exists🔗

• Orders (paper section 10). The partial-order operator <:, the extends clause on constants and the complete keyword were removed in Boogie 2.16.1 (commit 88cd4314, January 2023) together with OrderingAxiomBuilder. Both const c: T extends a, b complete; and x <: y are parse errors today. Top-level declarations transcribes the axioms the tool used to generate and gives three verified hand-written replacements.

• The finite type modifier (paper section 2.0). There is no finite keyword in the grammar. type finite Wicket; now silently declares a unary type constructor named finite, and Wicket is never declared at all; the only diagnostic appears at the use site. There is no cardinality control over user types in either direction. See Types.

• call forall (paper section 9.10) and wildcard actual parameters (call Lemma(*);). Both are parse errors. The desugaring code for wildcards is still in CallCmd.ComputeDesugaring, but no syntax reaches it.

• free modifies. The paper’s Spec production allows it; the grammar attaches free only to pre- and postconditions. Every modifies clause is checked (modifies).

• {:bvIgnore} (paper section 11.1). Never implemented; the string does not occur in the source. Axiom pruning, uses clauses and the hideable modifier cover the use case now.

• Unicode operator forms. The grammar still declares tokens for ⇔ ⇒ ∧ ∨ ≠ ≤ ≥ ¬ ∀ ∃ λ •, and the paper prints them alongside their ASCII spellings, but none can be written in a source file: the parser re-encodes the text to bytes and hands it to a byte-oriented scanner that never sees a character above 255. Lexical structure shows the mechanism.

Two smaller drifts are worth knowing before reading the paper’s appendix. Its reserved-word list has 38 entries and includes bv0, bv1, complete and finite; the scanner’s list has 68 and includes none of those. And its account of identifiers permits non-English Unicode letters; the implementation’s letter class is exactly the 52 ASCII letters.

1.3 What has been added since 2008🔗

• Types. real; the floating-point family floatSeE with the rounding-mode type rmode and its ten constant spellings; string and regex; and algebraic datatype declarations with testers (is), field access (->) and field update. See Types, Bitvectors, floating point and rounding modes, Strings and regular expressions and Algebraic datatypes.

• Expressions. if-then-else expressions, lambda, let (var x := e; body), code expressions |{...}|, real division / and exponentiation **, the postfix type coercion e : T, and the {:nopats} negative trigger. Integer division and modulo are spelled div and mod and map onto SMT-LIB’s Euclidean operators — the paper describes the corresponding operators as meaningless and suggests axiomatising them by hand. See Expressions and operators.

• Extensional maps. Maps satisfy extensionality by default, because the prover’s array theory is used. The paper states that they need not, and gives b[j := b[j]] == b as an example of something that need not hold; it now does. /useArrayAxioms restores the older behaviour.

• Declarations. uses clauses on constants and functions, hideable axioms, revealed functions, and the hide, reveal, push and pop statements that go with them; pure procedure; function bodies together with {:inline} and {:define}. See Top-level declarations.

• Specifications. A fourth kind of specification clause, measure, which checks that recursion terminates; {:always_assume}; free call. See Procedures, implementations and specifications.

• A standard library — /lib:base, /lib:node, /lib:set_size — compiled into the tool as embedded resources: pointwise map combinators, sets, finite maps, Option, vectors, sequences and the datatypes Civl builds on. See The standard library.

• Civl, a concurrency and refinement layer: action, yield procedure and yield invariant declarations, integer {:layer} annotations, mover types, asynchronous and parallel calls, and a linear permission discipline. The paper does not mention concurrency at all. See Civl: concurrency and refinement.

• Machinery around the proof itself, none of which the paper anticipates: automatic monomorphisation and the choice of type encoding, axiom pruning, pool-based quantifier instantiation, verification-condition splitting, result caching, and a large attribute vocabulary that drives all of it. See Advanced topics and tool internals and Attributes.

Section 11 of the paper says that “the Boogie language does not assign any formal meaning to the attributes”. That is the statement in it which has aged worst. The tool now reads more than seventy distinct attribute names, and several of them — {:verify}, {:inline}, {:define}, {:ignore}, {:subsumption}, {:verified_under}, {:checksum} — change what is proved. The paper’s own proposed spellings have drifted too: {:errorMessage} is implemented as {:msg}, and {:bvBuiltin "bvadd 8"} is implemented as {:bvbuiltin "bvadd"} — all lower case, no width. Since an unrecognised attribute name is silently ignored, writing the paper’s spelling produces no diagnostic at all, just a function that stays uninterpreted.

1.4 How this reference is organised🔗

The chapters run roughly bottom-up. Lexical structure through Statements and control flow describe the core language, in the order tokens, types, expressions, declarations, procedures, statements. Bitvectors, floating point and rounding modes, Strings and regular expressions and Algebraic datatypes cover the type families that need more than a paragraph. The standard library describes what /lib: gives you, Attributes is the attribute index, Civl: concurrency and refinement is the concurrency layer, Advanced topics and tool internals is what happens between the program and the solver, and Command-line reference documents every option the tool accepts.

A construct is documented in one place and cross-referenced from the others. Where two chapters could plausibly own a topic, the split is between surface and mechanism: Attributes gives an attribute’s argument shape and where it may be written, while the chapter that owns the feature explains what it does; Command-line reference gives an option’s syntax and default, while the chapter that owns the pass explains its effect.

1.5 Notation🔗

Grammar. Productions are quoted verbatim from Source/Core/BoogiePL.atg, in Coco/R’s EBNF, with the semantic actions elided:

IdsTypeWhere<. bool allowWhereClauses, string context, ... .>

= Idents ":" Type

[ "where" Expression ]

.

Braces { x } mean zero or more repetitions, brackets [ x ] mean optional, | separates alternatives, and quoted strings are terminals. The angle-bracket groups <. ... .> and <...> are Coco/R’s parameter lists, not part of the language. Anything inside a grammar block is what the grammar file says, including its comments and its occasional spelling mistakes. If a construct does not appear in BoogiePL.atg, it does not exist.

Listings. Boogie source appears like this:

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

ensures 0 <= r;

{

if (x < 0) { r := -x; } else { r := x; }

}

Commands and output. A command line, and the output it produced:

boogie cli-small.bpl

Boogie program verifier finished with 1 verified, 0 errors

Nothing in an output block is reconstructed from memory. Where a block is an excerpt — of a prover log, of a /print dump, of a long /trace run — it says so at that point. Timings, solver resource counts, counterexample model values and the numeric suffixes in monomorphised names vary between runs and between builds; those are noted where they appear.

Failing examples are shown with the diagnostics the tool actually produces.

Spelling. British spelling throughout, except in quoted source, quoted output, option names and attribute names, which use whatever the tool uses.

Environment. Boogie 3.5.7.0 with Z3 5.0.0 on Linux. A few results were cross-checked against cvc5 1.3.3, which is stated where it matters — notably in Portability to other solvers, since Boogie writes the regular-expression sort as Z3’s RegEx rather than SMT-LIB 2.6’s RegLan.