The language has two halves that meet in the middle. The mathematical
half — types, constants, functions, axioms, expressions — describes an
uninterpreted logical vocabulary. The imperative half — global
variables, procedures, implementations and statements — describes sets of
execution traces over states built from that vocabulary. Nothing in Boogie is
executable, there are no side effects in expressions, and there is no runtime.
A Boogie program either verifies or it does not.
1 Introduction |
1.1 This reference and This is Boogie 2 |
1.2 What the paper describes that no longer exists |
1.3 What has been added since 2008 |
1.4 How this reference is organised |
1.5 Notation |
|
2 Lexical structure |
2.1 Source text and encoding |
2.1.1 Non-ASCII bytes |
2.1.2 The Unicode operator tokens are unreachable |
2.1.3 Positions |
2.2 Whitespace |
2.3 Comments |
2.3.1 Unterminated block comments are silently accepted |
2.4 The conditional preprocessor |
2.4.1 Directives |
2.4.2 What is defined |
2.4.3 Surprises |
2.4.4 Preprocessor errors |
2.5 The #line pragma |
2.5.1 Any other # in column 1 is an error |
2.6 Identifiers |
2.6.1 The backslash escape |
2.6.2 Names with special meaning that are not keywords |
2.6.3 Identifiers downstream: what needs quoting |
2.7 Reserved words |
2.7.1 Soft keywords |
2.8 Literals |
2.8.1 Boolean literals |
2.8.2 Integer literals |
2.8.3 Real literals |
2.8.4 Bitvector literals |
2.8.5 Floating-point literals |
2.8.6 Rounding-mode literals |
2.8.7 String literals |
2.9 Operators and punctuation |
2.10 Divergences from This is Boogie 2 |
|
3 Types |
3.1 The shape of a type |
3.2 Primitive types |
3.2.1 bool, int and real |
3.2.2 Bitvector types |
3.2.3 Floating-point types |
3.2.4 rmode |
3.2.5 string and regex |
3.2.6 None of these take arguments |
3.2.7 These names are not keywords |
3.2.8 Types are disjoint |
3.3 Type constructors |
3.3.1 Applying a type constructor |
3.3.2 The paper’s finite modifier does not exist |
3.3.3 Built-in type constructors |
3.3.4 Datatypes are type constructors |
3.4 Type synonyms |
3.5 Map types |
3.5.1 Arity |
3.5.2 Nullary map types |
3.5.3 Polymorphic map types |
3.5.4 Where a bound type variable must occur |
3.5.5 Canonical ordering of map type parameters |
3.5.6 Higher-rank map types |
3.5.7 Map values |
3.6 Type variables |
3.6.1 Scope and shadowing |
3.7 Type checking |
3.7.1 The mechanism: matching by unification |
3.7.2 Map selection |
3.7.3 Map update |
3.7.4 Function and procedure application |
3.7.5 Equality |
3.7.6 Type inference and type proxies |
3.7.7 Type ascription |
3.8 Monomorphism and the type encoding |
3.8.1 Monomorphic programs |
3.8.2 Monomorphisable programs |
3.8.3 When monomorphisation fails |
3.8.4 Datatypes and :define require the monomorphic encoding |
3.9 Divergences from This is Boogie 2 |
|
4 Expressions and operators |
4.1 The expression grammar |
4.2 Precedence and associativity |
4.2.1 Operators that cannot be chained |
4.2.2 Two parsing traps |
4.3 Boolean operators |
4.4 Relational operators |
4.5 Arithmetic |
4.5.1 Integer division and modulo: div and mod |
4.5.2 Real division: / |
4.5.3 Exponentiation: ** |
4.5.4 Coercions between int and real |
4.6 Type coercion: e : T |
4.7 Map selection and update |
4.7.1 Extensionality |
4.8 Bitvector concatenation and extraction |
4.9 old expressions |
4.10 If-then-else expressions |
4.11 Quantifiers |
4.11.1 Scoping of bound variables |
4.11.2 Adjacent quantifiers are merged |
4.11.3 Triggers |
4.11.4 Negative triggers: {:nopats E} |
4.12 Lambda expressions |
4.12.1 Lambda lifting |
4.13 let expressions |
4.14 Code expressions |
4.14.1 Meaning |
4.14.2 Errors |
4.15 Datatype expressions |
4.16 Type checking of expressions |
4.17 Divergences from This is Boogie 2 |
|
5 Top-level declarations |
5.1 The shape of a program |
5.1.1 Namespaces |
5.1.2 Declaration order does not matter |
5.1.3 Duplicate declarations: :extern and :ignore |
5.2 Type declarations |
5.3 Constant declarations |
5.3.1 unique |
5.3.2 uses clauses on constants |
5.4 Orders: extends, complete and <: |
5.4.1 What used to exist |
5.4.2 The axioms the feature generated |
5.4.3 Worked example: extends |
5.4.4 Worked example: complete |
5.4.5 Worked example: unique parent edges |
5.4.6 Migration advice |
5.5 Function declarations |
5.5.1 Signatures |
5.5.2 Polymorphism |
5.5.3 Functions without bodies |
5.5.4 Function bodies and the axiom they generate |
5.5.5 Recursion |
5.5.6 :inline |
5.5.7 :define |
5.5.8 Attribute restrictions and the call-cycle check |
5.5.9 :builtin and :bvbuiltin |
5.5.10 uses clauses and pruning |
5.5.11 revealed |
5.6 Axiom declarations |
5.6.1 hideable |
5.6.2 Attributes on axioms |
5.6.3 :ctor no longer exists |
5.7 Global variable declarations |
5.7.1 What a where clause means |
5.7.2 The where-clause hazard |
5.7.3 Other notes on globals |
5.8 Summary: ordering and recursion rules |
5.9 Divergences from This is Boogie 2 |
|
6 Procedures, implementations and specifications |
6.1 Procedure declarations |
6.1.1 Grammar |
6.1.2 The two forms |
6.1.3 The combined form is a shorthand |
6.1.4 Parameters |
6.1.5 Type parameters |
6.1.6 Pure procedures |
6.2 Implementation declarations |
6.2.1 Multiple implementations |
6.2.2 Local variables |
6.3 Specification clauses |
6.3.1 requires |
6.3.2 ensures |
6.3.3 modifies |
6.3.3.1 Inferring modifies clauses |
6.3.4 Free specifications |
6.3.4.1 {:always_assume} |
6.3.5 measure clauses |
6.4 The caller/callee obligation split |
6.4.1 What the callee sees |
6.4.2 What the caller sees |
6.4.3 Summary |
6.5 where clauses |
6.5.1 Where they may appear |
6.5.2 Scope and typing |
6.5.3 When a where clause is assumed |
6.5.4 A where clause is never a proof obligation |
6.5.5 Unused locals lose their where clauses |
6.6 Inlining |
6.6.1 What happens at the cut-off |
6.6.2 What inlining does to the specification |
6.7 Recursion and termination |
6.8 Attributes and options that affect procedures |
6.9 Divergences from This is Boogie 2 |
|
7 Statements and control flow |
7.1 The shape of an implementation body |
7.2 assert and assume |
7.3 Assignment |
7.3.1 Map and field targets are sugar for whole-variable assignment |
7.3.2 Restrictions |
7.3.3 where clauses do not apply to assignment |
7.3.4 Attributes on assignments are parsed and dropped |
7.4 havoc |
7.5 Unpacking a datatype value |
7.6 Procedure calls |
7.6.1 What a call means |
7.6.2 free call |
7.6.3 Asynchronous and parallel calls |
7.7 if |
7.8 while |
7.8.1 invariant and free invariant |
7.8.2 measure |
7.9 break |
7.10 Labels, goto and return |
7.10.1 Label scoping |
7.11 From structured statements to basic blocks |
7.12 Loop semantics |
7.12.1 What exactly gets havoc’d |
7.12.2 Loops written with goto |
7.12.3 Irreducible control flow |
7.12.4 Free invariants: the tool differs from the paper |
7.12.5 Unrolling |
7.13 hide, reveal, push and pop |
7.14 Statement attributes |
7.14.1 The print attribute |
7.14.2 The captureState attribute |
7.14.3 Other statement attributes |
7.15 Divergences from This is Boogie 2 |
|
8 Bitvectors, floating point and rounding modes |
8.1 Bitvector types |
8.1.1 Bitvector literals |
8.2 Extraction and concatenation |
8.2.1 Extraction |
8.2.2 Concatenation |
8.2.3 Typing rules |
8.3 What bitvectors do not have |
8.4 :bvbuiltin and the SMT-LIB bitvector operations |
8.4.1 The catalogue |
8.4.2 Indexed operations |
8.4.3 Axioms about builtin functions |
8.5 Integers and bitvectors |
8.6 Floating-point types |
8.7 Floating-point literals |
8.7.1 Literals must be exact |
8.7.2 NaN and infinity |
8.7.3 The sign is part of the token |
8.8 The built-in float operators |
8.8.1 Arithmetic rounds to nearest, ties to even |
8.8.2 Comparison is IEEE; equality is not |
8.9 Rounding modes |
8.10 Float operations via :builtin |
8.10.1 Fixing the rounding mode in the attribute |
8.10.2 Conversions |
8.11 Interaction with the rest of the language |
8.11.1 Counterexamples |
8.11.2 Solver dependence |
8.12 Divergences from This is Boogie 2 |
|
9 Strings and regular expressions |
9.1 The string and regex types |
9.1.1 Syntax and resolution |
9.1.2 What the language gives you |
9.1.3 How the types reach the solver |
9.2 String literals |
9.2.1 The token |
9.2.2 There are no escape sequences |
9.3 Reaching the string theory: :builtin |
9.3.1 Mechanics |
9.3.2 Nothing about the name is validated |
9.3.3 Where :builtin applies |
9.4 String operations |
9.5 Regular-expression operations |
9.5.1 Indexed operators |
9.6 Legacy and standard spellings |
9.7 Corner cases of the SMT semantics |
9.8 Reasoning about strings |
9.8.1 Incompleteness is normal |
9.8.2 Counterexample models |
9.8.3 Quantifiers and triggers |
9.9 Portability to other solvers |
9.10 Divergences from This is Boogie 2 |
|
10 Algebraic datatypes |
10.1 Declaring a datatype |
10.1.1 Syntactic rules |
10.1.2 Names and name spaces |
10.1.3 Attributes |
10.1.4 Type parameters |
10.1.5 Fields shared between constructors |
10.1.6 Well-foundedness |
10.2 Constructors |
10.3 Testers: e is Ctor |
10.4 Field access: e->f |
10.4.1 Selectors are total, but underspecified off their own constructor |
10.4.2 Shared field names produce a conditional |
10.5 Field update: e->(f := v) |
10.5.1 Trap: updating a field the value does not have |
10.6 Statements over datatypes |
10.6.1 Field assignment |
10.6.2 Unpack |
10.7 What the prover is told |
10.7.1 The properties you get |
10.7.2 Counterexample models |
10.8 Polymorphic datatypes and the type encoding |
10.8.1 Interaction with /typeEncoding |
10.9 Datatypes, maps and quantifiers |
10.9.1 Triggers |
10.9.2 Recursive definitions |
10.10 Pattern-style specifications |
10.11 Standard library datatypes |
10.12 Divergences from This is Boogie 2 |
|
11 The standard library |
11.1 Loading a library |
11.1.1 Automatic loading for Civl programs |
11.1.2 Monomorphisation |
11.2 Map combinators |
11.2.1 Implementation note: the emitted SMT |
11.2.2 Integer ranges |
11.3 Default |
11.4 Option, Unit and UnitMap |
11.5 Sets |
11.5.1 Set cardinality: /lib:set_size |
11.6 Vectors |
11.6.1 Representation |
11.6.2 The canonicalisation axioms |
11.6.3 Vector operations |
11.6.4 Concat and Slice |
11.6.5 Extensionality: Vec_Ext |
11.7 Sequences |
11.8 Finite maps |
11.8.1 Operations |
11.8.2 Permission collectors |
11.9 Civl-oriented types and primitives |
11.9.1 One, Cell, Tag, Loc |
11.9.2 The linear primitives |
11.9.3 Surprise: Map_Put assumes freshness of a linear key |
11.9.4 Allocation: Loc_New, Tag_New, Tags_New |
11.9.5 Move, Copy, Assume, Assert |
11.9.6 Map well-formedness is free in Civl |
11.10 The node library |
11.10.1 Node, Between and Avoiding |
11.10.2 InDomain |
11.10.3 Stack, set and queue abstractions |
11.10.4 The lemmas are trusted unless you discharge them |
11.11 Divergences from This is Boogie 2 |
11.12 Where to find real usage |
|
12 Attributes |
12.1 Syntax |
12.1.1 Attributes chain |
12.1.2 Arguments are resolved and type checked |
12.1.3 Unknown attributes are silently accepted |
12.2 How Boogie reads an attribute |
12.3 Where attributes may be written |
12.3.1 A procedure with a body has two attribute lists |
12.3.2 Quantifiers: before the bound variables means something else |
12.4 Top-level declarations |
12.4.1 {:ignore} |
12.4.2 {:extern} |
12.4.3 {:name "s"} |
12.4.4 {:verboseName "s"} |
12.4.5 {:keep} and {:include_dep} |
12.5 Functions |
12.5.1 {:inline} and {:define} |
12.5.2 {:builtin "s"} and {:bvbuiltin "s"} |
12.5.3 {:never_pattern} |
12.5.4 {:identity} |
12.6 Procedures and implementations |
12.6.1 {:verify false} |
12.6.2 {:inline N} |
12.6.3 {:priority N} |
12.6.4 {:timeLimit N}, {:rlimit N},
{:random_seed N}, {:smt_option "k", "v"} |
12.6.5 {:selective_checking} and
{:start_checking_here} |
12.6.6 {:kInductionDepth N} |
12.6.7 {:msg_if_verifies "s"} |
12.6.8 Other implementation attributes |
12.7 Specifications |
12.7.1 {:msg "s"} |
12.7.2 {:always_assume} |
12.8 Statements |
12.8.1 {:subsumption n} |
12.8.2 {:expand} |
12.8.3 {:verified_under e} |
12.8.4 {:minimize e} and {:maximize e} |
12.8.5 {:soft} and {:try} |
12.8.6 {:print e0, e1, ...} |
12.8.7 {:captureState "s"} |
12.8.8 {:PossiblyUnreachable} |
12.8.9 {:id "s"} on statements |
12.8.10 {:assumption} on local variables |
12.9 Splitting the verification condition |
12.9.1 {:split_here} |
12.9.2 {:isolate} and {:isolate "paths"} |
12.9.3 {:allow_path_isolation} |
12.9.4 {:focus} |
12.9.5 {:vcs_*} |
12.10 Quantifiers, triggers and lambdas |
12.10.1 Triggers |
12.10.2 {:nopats e} |
12.10.3 {:qid "s"} and {:weight N} |
12.10.4 {:pool "name"} and {:add_to_pool "name", e, ...} |
12.11 Verification result caching |
12.12 Houdini and abstract interpretation |
12.12.1 {:existential true} |
12.12.2 Staged Houdini |
12.12.3 Stratified inlining |
12.12.4 {:inferred} and {:where e} |
12.13 Civl |
12.14 Attributes Boogie generates |
12.15 Attributes Boogie does not read |
12.16 Divergences from This is Boogie 2 |
12.17 Summary: everything Boogie reads |
|
13 Civl: concurrency and refinement |
13.1 The model |
13.2 Layers |
13.2.1 Where a layer annotation may appear |
13.2.2 Global variables |
13.2.3 Layers on assertions and specifications |
13.3 Atomic actions |
13.3.1 Declaring an action |
13.3.2 The gate |
13.3.3 modifies |
13.3.4 Calls between actions |
13.3.5 An action refining an action |
13.3.6 pure actions and procedures |
13.4 Yield procedures |
13.4.1 Declaring a yield procedure |
13.4.2 refines |
13.4.3 {:hide} and visible formals |
13.4.4 Mover procedures |
13.4.5 What a yield procedure body may do |
13.4.6 Introducing state |
13.5 Yield invariants |
13.5.1 Declaration |
13.5.2 What a yield invariant obliges |
13.5.3 requires call, ensures call, preserves call |
13.5.4 Yielding loops |
13.6 Calls |
13.6.1 Synchronous calls |
13.6.2 Asynchronous calls |
13.6.3 Parallel calls |
13.7 Mover types and their obligations |
13.7.1 The four mover checks |
13.7.2 Yield sufficiency (the atomicity check) |
13.8 Linear variables |
13.8.1 Linear types and permissions |
13.8.2 The three annotations |
13.8.3 The availability discipline |
13.8.4 Linear globals and the primitives |
13.9 The checks Civl generates |
13.9.1 The shape of a desugared yield procedure |
13.9.2 Trusting parts of the proof |
13.10 Worked example: a spin lock |
13.11 Divergences from This is Boogie 2 |
|
14 Advanced topics and tool internals |
14.1 The verification pipeline |
14.1.1 Whole-program phases |
14.1.2 Per-implementation phases |
14.1.3 Watching a program go through the pipeline |
14.1.4 Which flag prints which intermediate form |
14.2 Type encodings and monomorphisation |
14.2.1 How the encoding is actually chosen |
14.2.2 Monomorphisation |
14.2.3 When monomorphisation fails |
14.2.4 What the three encodings look like at the solver |
14.2.5 Maps: theory of arrays versus axioms |
14.3 Pruning |
14.3.1 /prune defaults to off |
14.3.2 What pruning keeps |
14.3.3 uses clauses |
14.3.4 Escape hatches: {:include_dep} and {:keep} |
14.3.5 Inspecting the result |
14.4 Hiding and revealing function definitions |
14.4.1 Syntax |
14.4.2 Semantics |
14.4.3 The granularity is one verification condition, not one statement |
14.4.4 There is no {:opaque} attribute |
14.5 Pool-based quantifier instantiation |
14.5.1 {:pool} and {:add_to_pool} |
14.5.2 What the engine does |
14.5.3 /keepQuantifier |
14.5.4 Limits and traps |
14.6 Splitting the verification condition |
14.6.1 {:split_here} |
14.6.2 {:isolate} |
14.6.3 {:isolate "paths"} and {:allow_path_isolation} |
14.6.4 {:focus} |
14.6.5 /vcsSplitOnEveryAssert |
14.6.6 Automatic, cost-based splitting |
14.7 Loop unrolling |
14.7.1 /soundLoopUnrolling |
14.7.2 Related loop options |
14.8 Inlining |
14.8.1 What happens to the specification at an inline site |
14.8.2 Inlining at the call site |
14.8.3 Function inlining is a different mechanism |
14.9 Abstract interpretation |
14.10 Houdini |
14.11 The SMT-LIB interface |
14.11.1 Reading the query |
14.11.2 Batch versus interactive |
14.11.3 Passing options to the solver |
14.11.4 Reproducibility |
14.12 Divergences from This is Boogie 2 |
14.13 Gotchas, collected |
|
15 Command-line reference |
15.1 Invoking Boogie |
15.1.1 Usage |
15.1.2 Option syntax |
15.1.3 Unknown options behave differently on Unix |
15.1.4 Input files |
15.1.5 Exit codes |
15.2 Informational options |
15.3 Selecting what to verify |
15.3.1 /proc and /noProc |
15.3.2 /verifySeparately |
15.3.3 /noResolve, /noTypecheck, /noVerify |
15.3.4 /overlookTypeErrors |
15.4 Libraries |
15.5 Printing the program |
15.5.1 /print and the print modifiers |
15.5.2 /printPassive |
15.5.3 /printSplit, /printPruned and /printSplitDeclarations |
15.5.4 /printInstrumented and /printInlined |
15.5.5 /printCFG |
15.5.6 /printLean |
15.5.7 /xml |
15.5.8 File-name macros and /logPrefix |
15.5.9 /useBaseNameForFileName and /printVerifiedProceduresCount |
15.6 Verification-condition generation |
15.6.1 Program transformations before VC generation |
15.6.2 /subsumption |
15.6.3 /alwaysAssumeFreeLoopInvariants |
15.6.4 /prune |
15.6.5 Type and array encoding |
15.6.6 Prover-input stability |
15.6.7 /keepQuantifier and pool instantiation |
15.7 Error reporting |
15.7.1 /errorLimit |
15.7.2 /errorTrace |
15.7.3 /printModel, /printModelToFile and /mv |
15.7.4 /enhancedErrorMessages |
15.7.5 /forceBplErrors |
15.7.6 /trackVerificationCoverage and /warnVacuousProofs |
15.7.7 /smoke and /smokeTimeout |
15.8 Resource limits |
15.8.1 How a timeout is reported |
15.8.2 /runDiagnosticsOnTimeout and /traceDiagnosticsOnTimeout |
15.9 Prover selection and options |
15.9.1 /proverDll |
15.9.2 /proverOpt (/p) |
15.9.3 /proverLog, /proverLogAppend and /proverPreamble |
15.9.4 Other prover-facing options |
15.10 Splitting and parallelism |
15.10.1 /vcsMaxCost |
15.10.2 The splitting cost model |
15.10.3 /vcsSplitOnEveryAssert and /vcsDumpSplits |
15.10.4 /vcsCores and /vcsLoad |
15.10.5 /relaxFocus |
15.11 Inference |
15.11.1 Abstract interpretation: /infer |
15.11.2 Houdini: /contractInfer |
15.11.3 Staged and concurrent Houdini |
15.12 Inlining and loops |
15.12.1 /inline and /printInlined |
15.12.2 Loop options |
15.12.3 Stratified inlining |
15.12.4 Lambda-lifting options |
15.12.5 /printMeasureDesugaring |
15.13 Caching and snapshots |
15.13.1 /verifySnapshots |
15.13.2 /traceCaching |
15.14 Civl |
15.15 Verbosity, tracing and debugging |
15.15.1 Verbosity levels |
15.15.2 /trace and friends |
15.16 Options with no effect, and undocumented options |
15.16.1 Options with no effect |
15.16.2 Undocumented options |
15.17 Complete option index |