2 Lexical structure🔗

This chapter describes how Boogie turns the bytes of a source file into a stream of tokens. Everything here is fixed by three pieces of the implementation:

• Source/Core/BoogiePL.atg — the Coco/R attributed grammar. Its CHARACTERS, TOKENS, COMMENTS and IGNORE sections define the token language, and the generated Source/Core/Scanner.cs implements it.

• Source/Core/ParserHelper.cs — a line-oriented conditional-compilation pass that runs before the scanner.

• Source/Core/Scanner.frame, from which Scanner.cs is generated — a customised Coco/R frame that additionally implements the #line pragma and rejects any other # line that starts in column 1.

The processing pipeline for one file is:

1. The file is opened and decoded as UTF-8 by a StreamReader. If the file name is exactly stdin.bpl, the program text is read from standard input instead.

2. ParserHelper.Fill walks the text line by line and resolves #if/#elsif/#else/#endif, replacing every directive line and every excluded line with an empty line.

3. The resulting string is re-encoded to UTF-8 bytes and handed to the scanner as a byte stream.

4. The scanner skips whitespace and comments, handles # pragmas in column 1, and produces tokens by longest match.

5. The Coco/R LL(1) parser consumes the tokens.

Throughout this chapter, /print:- output is shown with its two-line version and command-line banner removed.

2.1 Source text and encoding🔗

Boogie source is, for practical purposes, ASCII. The grammar’s letter class is exactly the 52 unaccented English letters:

letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".

digit = "0123456789".

hexdigit = "0123456789ABCDEFabcdef".

special = "'~#$^_.?`".

glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".

cr        = '\r'.

lf        = '\n'.

tab       = '\t'.

space = ' '.

quote = '"'.

newLine = cr + lf.

regularStringChar = ANY - quote - newLine.

nondigit = letter + special.

nonquote = letter + digit + space + glyph.

(glyph and nonquote are defined but are not referenced by any token production; they are dead declarations.)

2.1.1 Non-ASCII bytes🔗

The scanner reads bytes, not characters: the UTF-8-aware buffer in the generated scanner is only installed when the byte stream begins with a UTF-8 byte-order mark, and by that point the mark has already been consumed and discarded by the StreamReader that fed the preprocessor. The consequences are worth spelling out.

A non-ASCII character is legal in a comment (the scanner is just discarding bytes) and inside a string literal (every byte other than ", LF and CR is accepted), but a string literal keeps the individual UTF-8 bytes as separate characters. Printing the program back out re-encodes each of those bytes, producing mojibake:

procedure {:tag "café"} P()

{

assert true;

}

boogie /noVerify /print:- mojibake.bpl

procedure {:tag "café"} P();

implementation {:tag "café"} P()

{

assert true;

}

Boogie program verifier finished with 0 verified, 0 errors

A non-ASCII character anywhere else is a parse error, since none of its bytes belong to any token class.

If the file is not valid UTF-8, the StreamReader substitutes U+FFFD for each bad byte, which is re-encoded as the three bytes EF BF BD.

2.1.2 The Unicode operator tokens are unreachable🔗

The grammar declares Unicode spellings for thirteen operators and binders:

None of them can actually be written in a source file, because the scanner never sees a character above 255. Twelve of the thirteen have code points above 255 and are therefore unreachable in principle; ¬ (U+00AC) would be reachable from a raw 0xAC byte, but such a byte is not valid UTF-8 and is replaced by U+FFFD before the scanner runs. A file using the Unicode forms fails to parse:

axiom (∀ x: int :: x == x);

boogie /noVerify unicode.bpl

unicode.bpl(1,8): error: invalid AtomExpression

1 parse errors detected in unicode.bpl

There are no Unicode characters in Boogie’s own 764-file test suite except one curly apostrophe inside a comment.

2.1.3 Positions🔗

Tokens carry a 1-based line number and a 1-based column number, and diagnostics are reported as file(line,col). Diagnostics produced while handling a # pragma report column 0. The file name in a diagnostic is the file name as given on the command line, unless a #line pragma has changed it.

2.2 Whitespace🔗

The scanner skips space (32), tab (9), line feed (10) and carriage return (13) between tokens. The grammar’s IGNORE clause lists only cr, lf and tab; the space character is always ignored by Coco/R and does not appear there.

IGNORE cr + lf + tab

An isolated carriage return (one not followed by a line feed) is normalised to a line feed, so Unix, Windows and classic-Mac line endings all work and all count as one line.

No other character is whitespace. In particular form feed (12) and vertical tab (11) are not skipped and terminate the parse:

const a: int;

<FF>const b: int;

Here <FF> stands for a single form-feed byte (0x0C) at the start of line 2; it cannot be shown literally.

boogie /noVerify formfeed.bpl

formfeed.bpl(2,1): error: EOF expected

1 parse errors detected in formfeed.bpl

Whitespace is never required between tokens except where it is needed to separate two tokens that would otherwise merge under longest match. Two cases where this bites are described later: 300bv8 is one token but 300 bv8 is two, and x-0x1.0e0f24e8 lexes the minus sign as part of the float literal.

2.3 Comments🔗

COMMENTS FROM "/*" TO "*/" NESTED

COMMENTS FROM "//" TO lf

A line comment runs from // to the next line feed. A block comment runs from /* to the matching */ and nests: /* inside a block comment increments the nesting level and a matching */ is required for each. This differs from C, C++, Java and C#.

The two comment forms do not interact. /* inside a line comment does not open a block comment, and // inside a block comment does not hide a following */.

// a line comment; /* here does not open a block comment

/* a block comment, in which // is not special */

/* outer

/* inner */

still commented out

*/

procedure P()      // trailing comment

{

assert /* inline */ true;

}

boogie comments.bpl

Boogie program verifier finished with 1 verified, 0 errors

2.3.1 Unterminated block comments are silently accepted🔗

If a block comment is never closed, the scanner reaches end of file inside it and simply reports end of file. There is no diagnostic. The following program has no declarations at all, and Boogie says nothing about it:

/* /* */

procedure P() { assert false; }

boogie /noVerify /print:- comments-eat.bpl

Boogie program verifier finished with 0 verified, 0 errors

The /* */ on line 1 opens two nesting levels and closes one, so the rest of the file is comment. A C programmer would expect line 2 to be code. This is the single most likely way to lose a chunk of a Boogie program without being told.

Source comments are not retained in the AST, so /print never reproduces them.

2.4 The conditional preprocessor🔗

Before the scanner runs, ParserHelper.Fill processes the text one line at a time and resolves conditional compilation. It is not a macro processor: there is no substitution, no #define in the language, and no #include.

2.4.1 Directives🔗

Four directives are recognised, after the line has been trimmed of leading and trailing whitespace:

Note the spelling #elsif, not #elif and not #elseif. #if blocks nest to any depth.

The condition of #if and #elsif is everything after the directive name, with leading whitespace stripped. Any number of leading ! characters (each optionally followed by whitespace) flips the sense of the test; what remains is compared, as an exact string, against the list of defined symbols. So #if !!X means “X is defined”.

Directive lines and excluded lines are replaced by empty lines rather than being deleted, so line numbers in diagnostics always refer to the original file.

2.4.2 What is defined🔗

There is no command-line option to define a symbol — Boogie has no /D flag. The only symbols ever defined are supplied by the execution engine, which passes exactly one per file: FILE_n, where n is the 0-based index of that file on the command line. So FILE_0 is defined while parsing the first file, FILE_1 while parsing the second, and so on. Nothing else is ever defined; every other condition is false. (Standard-library files pulled in by /lib: are parsed with an empty list, so inside them no condition at all is true. None of them uses a directive.)

#if FILE_0

const first: int;

#endif

#if FILE_1

const second: int;

#endif

#if FILE_0

const third: int;

#endif

#if FILE_1

const fourth: int;

#endif

boogie /noVerify /print:- pp-a.bpl pp-b.bpl

const first: int;

const fourth: int;

Boogie program verifier finished with 0 verified, 0 errors

Because FILE_0 is always defined for the first file, #if FILE_0 is the idiomatic way to write “include this unconditionally” and #if !FILE_0 the way to write “never include this”. A general #if/#else works as expected:

procedure P()

{

#if FILE_0

assert true;

#elsif SOMETHING_ELSE

assert false;

#else

assert false;

#endif

}

boogie /print:- pp.bpl

procedure P();

implementation P()

{

assert true;

}

Boogie program verifier finished with 1 verified, 0 errors

2.4.3 Surprises🔗

Directives may be indented, but #line may not. Fill trims the line before testing it, so   #if FILE_0 is a directive. The #line pragma, handled later by the scanner, requires the # in column 1.

A trailing comment silently changes the condition. The condition is the rest of the line verbatim, so #if FILE_0 // always true tests for a symbol literally named FILE_0 // always true, which is not defined, and the block is dropped without any diagnostic.

#if FILE_0 // always true

const a: int;

#endif

boogie /noVerify /print:- pp-comment.bpl

Boogie program verifier finished with 0 verified, 0 errors

By contrast #else and #endif are matched by exact equality, so #endif // done is not recognised as a directive at all, and later fails as an unrecognised pragma.

No space is needed after #if. The condition is Substring(3), so #ifFILE_0 is a well-formed directive testing FILE_0.

Directives are recognised inside comments and strings. Fill has no idea what a comment is. A block comment that happens to contain a line reading #endif breaks the file:

/* a block comment that mentions

#endif

in passing */

procedure P() { assert true; }

boogie /noVerify pp-in-comment.bpl

pp-in-comment.bpl(2,0): error: Unrecognized pragma: #MalformedInput: misplaced #endif

1 parse errors detected in pp-in-comment.bpl

2.4.4 Preprocessor errors🔗

Fill does not report errors itself. When it detects malformed input it stops and appends a line of the form #MalformedInput: reason, which the scanner then rejects as an unrecognised pragma. The four reasons are missing #endif, misplaced #elsif, misplaced #else and misplaced #endif.

#if FILE_0

const a: int;

boogie /noVerify pp-noend.bpl

pp-noend.bpl(3,0): error: Unrecognized pragma: #MalformedInput: missing #endif

1 parse errors detected in pp-noend.bpl

An #elsif after an #else at the same level is misplaced:

#if FILE_0

const a: int;

#else

const b: int;

#elsif FILE_0

const c: int;

#endif

boogie /noVerify pp-misplaced.bpl

pp-misplaced.bpl(5,0): error: Unrecognized pragma: #MalformedInput: misplaced #elsif

1 parse errors detected in pp-misplaced.bpl

An #else with no open #if is the fourth reason:

#else

const x: int;

boogie /noVerify pp-else.bpl

pp-else.bpl(1,0): error: Unrecognized pragma: #MalformedInput: misplaced #else

1 parse errors detected in pp-else.bpl

A C-style #elif is not a directive, so it survives into the token stream and is rejected by the scanner:

#if FILE_0

const a: int;

#elif FILE_0

const b: int;

#endif

boogie /noVerify pp-elif.bpl

pp-elif.bpl(3,0): error: Unrecognized pragma: #elif FILE_0

1 parse errors detected in pp-elif.bpl

2.5 The #line pragma🔗

The scanner treats any # that appears in column 1 as introducing a pragma, and consumes the rest of the line. Exactly one pragma is understood:

#line num [ filename ]

It sets the line number of the following line to num, and, if a filename is present, changes the file name reported in all subsequent diagnostics. This makes Boogie usable as a back end for a front-end compiler that wants errors reported against its own source. The feature is implemented in Scanner.frame and appears nowhere in the grammar.

procedure P()

{

#line 100 original.c

assert false;

}

boogie linepragma.bpl

original.c(100,3): Error: this assertion could not be proved

Execution trace:

original.c(100,3): anon0

Boogie program verifier finished with 0 verified, 1 error

A line that starts #line (or is exactly #line) but whose argument is not an integer is reported specifically:

procedure P()

{

#line

assert false;

}

boogie /noVerify line-alone.bpl

line-alone.bpl(3,0): error: Malformed (#line num [filename]) pragma: #line

1 parse errors detected in line-alone.bpl

2.5.1 Any other # in column 1 is an error🔗

Because # is a legal identifier character (see below), an identifier may begin with #. Such an identifier is fine anywhere except at the very start of a line, where the scanner takes it for a pragma:

const c: int;

#name: int;

boogie /noVerify hashident.bpl

hashident.bpl(2,0): error: Unrecognized pragma: #name: int;

1 parse errors detected in hashident.bpl

Only the first character of the line matters. Breaking the line so that the # is no longer in column 1 makes the same declaration legal:

const c: int;

const

#name: int;

boogie /noVerify /print:- hashident2.bpl

const c: int;

const #name: int;

Boogie program verifier finished with 0 verified, 0 errors

Names beginning with # are common in machine-generated Boogie, and they work provided they never start a line:

procedure P()

{

var #tmp: int;

#tmp := 1;

assert #tmp == 1;

}

boogie hashok.bpl

Boogie program verifier finished with 1 verified, 0 errors

2.6 Identifiers🔗

nondigit = letter + special.

special  = "'~#$^_.?`".

ident =  [ '\\' ] nondigit {nondigit | digit}.

An identifier is an optional backslash, then one character that is a letter or one of the nine special characters, then any number of letters, special characters and digits. Identifiers are case sensitive and have no length limit.

The characters legal in an identifier are therefore:

Every character in the table may appear after the first one. Everything else — including @, %, &, - and non-ASCII letters — is not part of an identifier.

All of these are ordinary global names:

const x': int;

const x~: int;

const x#y: int;

const x$y: int;

const x^y: int;

const _x: int;

const a.b: int;

const p?: int;

const `q: int;

const ?huh: int;

const .dot: int;

const 'tick: int;

procedure P()

requires x' == 1 && .dot == 2;

{

assert x' + .dot == 3;

}

boogie idchars.bpl

Boogie program verifier finished with 1 verified, 0 errors

Because . is a legal first character, some things that look like numbers are identifiers. .5 is not a real literal, it is an identifier:

const a: real;

axiom a == .5;

boogie /noVerify dotfive.bpl

dotfive.bpl(2,11): Error: undeclared identifier: .5

1 name resolution errors detected in dotfive.bpl

2.6.1 The backslash escape🔗

A leading backslash is not part of the name: the parser strips it. Its only purpose is to let a reserved word be used as an identifier, since the keyword test is applied to the raw token text and \forall does not equal forall.

const \forall: int;

const \int: bool;

procedure P()

requires \int;

{

assert \forall == \forall;

}

boogie escaped.bpl

Boogie program verifier finished with 1 verified, 0 errors

Every one of the 68 reserved words listed below can be escaped this way. \foo and foo denote the same entity. The backslash is only allowed in the first position: a\b is a followed by the identifier b; \\foo and \1 are rejected (invalid Ident).

The printer round-trips escaped identifiers, re-inserting a backslash when it prints a name that it believes needs one:

boogie /noVerify /print:- escaped.bpl

const \forall: int;

const \int: bool;

procedure P();

requires \int;

implementation P()

{

assert \forall == \forall;

}

Boogie program verifier finished with 0 verified, 0 errors

2.6.2 Names with special meaning that are not keywords🔗

Several names that behave like built-in types are lexically ordinary identifiers, given meaning only during name resolution:

• bvK for a decimal K — a bitvector type;

• floatNeM — a floating-point type;

• rmode — the rounding-mode type;

• string and regex — the string and regular-expression types.

Only int, real and bool are reserved type names. The names above are ordinary identifiers, and can be used as such wherever no type is expected — a constant called rmode or a variable called string is perfectly legal.

They cannot, however, be shadowed. UnresolvedTypeIdentifier.ResolveType (Source/Core/AST/AbsyType.cs) tests for these five shapes before it looks up type variables and before it looks up user-declared type constructors and synonyms, so a user declaration of the same name never wins. Declaring type rmode;, type string;, type regex; or type floatNeM; is accepted without a diagnostic and then has no effect whatsoever:

type string;

const s: string;

axiom s == "abc";

const rmode: int;

axiom rmode == 0;

boogie /noVerify noshadow.bpl

Boogie program verifier finished with 0 verified, 0 errors

bvK is the exception: a type declaration whose name matches bvdigits is rejected outright by ResolutionContext.CheckBvNameClashes, even though the same name is fine for a constant or a variable.

type bv8;

boogie /noVerify bvclash.bpl

bvclash.bpl(1,5): Error: type name: bv8 is registered for bitvectors

1 name resolution errors detected in bvclash.bpl

2.6.3 Identifiers downstream: what needs quoting🔗

The set of characters Boogie allows in an identifier is larger than the set SMT-LIB allows in a symbol, so names are rewritten on the way to the prover (Source/Provers/SMTLib/SmtLibNameUtils.cs). Two rewrites apply:

• A name that is an SMT-LIB reserved word, or that starts with a digit or a dot, is prefixed with q@.

• A name containing any character outside ~!@$%^&*_-+=<>.?/ plus letters and digits is wrapped in vertical bars. Of Boogie’s identifier characters, that means `, ' and # force quoting. (| and \ are illegal even inside bars, and are replaced by _; neither can occur in a Boogie name anyway.)

const x#1: int;

const y': int;

const `z: int;

const .w: int;

const \div: int;

procedure P()

{

assert x#1 + y' + `z + .w + \div == \div + .w + `z + y' + x#1;

}

boogie /proverLog:smtnames.smt2 smtnames.bpl

Boogie program verifier finished with 1 verified, 0 errors

The corresponding declarations in the prover log:

(declare-fun |x#1| () Int)

(declare-fun |y'| () Int)

(declare-fun |`z| () Int)

(declare-fun q@.w () Int)

(declare-fun q@div () Int)

This is transparent — verification is unaffected — but it explains the names that show up in prover logs and counterexample models.

2.7 Reserved words🔗

Sixty-eight words are reserved. They are recognised in Scanner.CheckLiteral, which runs on every identifier token.

Using one bare where an identifier is expected fails:

const real: int;

boogie /noVerify bare-keyword.bpl

bare-keyword.bpl(1,7): error: invalid Ident

1 parse errors detected in bare-keyword.bpl

2.7.1 Soft keywords🔗

Eight of the reserved words are explicitly converted back into identifiers by the Ident production, which is also where the leading backslash is dropped (the production’s Contract.Ensures line is elided here):

Ident<out IToken x>

= ( ident

| "atomic"   (. t.kind = _ident; .) // convert to ident

| "both"     (. t.kind = _ident; .) // convert to ident

| "left"     (. t.kind = _ident; .) // convert to ident

| "right"    (. t.kind = _ident; .) // convert to ident

| "reveal"     (. t.kind = _ident; .) // convert to ident

| "hide"     (. t.kind = _ident; .) // convert to ident

| "push"     (. t.kind = _ident; .) // convert to ident

| "pop"     (. t.kind = _ident; .) // convert to ident

)

(.

x = t;

if (x.val.StartsWith("\\"))

x.val = x.val.Substring(1);

.)

.

So atomic, both, left, right, reveal, hide, push and pop can be declared and used without a backslash. There is a catch for the last four: reveal, hide, push and pop also start statements, and the parser commits to the statement form before it can see the :=. A local named pop can be declared but not assigned to:

procedure P()

{

var pop: int;

pop := 1;

}

boogie /noVerify softkw.bpl

softkw.bpl(4,7): error: ";" expected

1 parse errors detected in softkw.bpl

atomic, both, left and right have no statement form and work everywhere:

procedure P()

{

var pop: int;

var left: int;

left := 1;

assert left == 1;

}

boogie softkw2.bpl

Boogie program verifier finished with 1 verified, 0 errors

2.8 Literals🔗

2.8.1 Boolean literals🔗

true and false, both of type bool. They are reserved words rather than a token class.

2.8.2 Integer literals🔗

digits = digit {digit}.

A non-empty run of decimal digits, and nothing else. There is no sign (a leading - is the unary minus operator), no radix prefix, no digit separator and no width suffix. Integers are arbitrary precision. Leading zeros are permitted and discarded.

const i: int;

const j: int;

axiom i == 007;

axiom j == 123456789012345678901234567890;

boogie /noVerify /print:- numbers.bpl

const i: int;

const j: int;

axiom i == 7;

axiom j == 123456789012345678901234567890;

Boogie program verifier finished with 0 verified, 0 errors

There are no hexadecimal integer literals. 0x10 is the integer 0 followed by the identifier x10:

const a: int;

axiom a == 0x10;

boogie /noVerify hexint.bpl

hexint.bpl(2,13): error: ";" expected

1 parse errors detected in hexint.bpl

2.8.3 Real literals🔗

Two token classes produce a value of type real:

decimal   = digit {digit} 'e' [ '-' ] digit {digit} .

dec_float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .

(The token named dec_float has nothing to do with the float types; both classes denote exact arbitrary-precision decimals, held as a BigDec.)

Note what is not allowed:

• no + in the exponent — 1e+3 does not parse;

• no capital E — 1E3 does not parse;

• digits are required on both sides of the point — 1. and .5 do not parse as reals;

• no sign; -1.5 is unary minus applied to 1.5.

The printer normalises every real to the decimal form with a minimal mantissa:

const r: real;

const s: real;

const t: real;

axiom r == 3.14;

axiom s == 1e3;

axiom t == 2.5e-2;

boogie /noVerify /print:- reals.bpl

const r: real;

const s: real;

const t: real;

axiom r == 314e-2;

axiom s == 1e3;

axiom t == 25e-3;

Boogie program verifier finished with 0 verified, 0 errors

2.8.4 Bitvector literals🔗

bvlit = digit {digit} 'b' 'v' digit {digit}.

A bitvector literal is a decimal value, the two letters bv, and a decimal width, all one token — no whitespace is allowed anywhere inside it. The literal carries its own type: 255bv8 has type bv8. What can be done with such a value — extraction, concatenation and the :bvbuiltin catalogue — is in Bitvectors, floating point and rounding modes.

The value is not range-checked. A literal too large for its width is accepted silently and truncated modulo two to the power of the declared width when it reaches the prover:

procedure P()

{

assert 300bv8 == 44bv8;

}

boogie bvwrap.bpl

Boogie program verifier finished with 1 verified, 0 errors

procedure P()

{

assert 300bv8 == 45bv8;

}

boogie bvwrap2.bpl

bvwrap2.bpl(3,3): Error: this assertion could not be proved

Execution trace:

bvwrap2.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

The paper states that Xbv K is legal only when X is 0 or fits in K bits; the tool does not enforce this and wraps instead.

2.8.5 Floating-point literals🔗

This is the least documented corner of Boogie’s lexis, so the grammar is worth quoting in full. (The float types and operations are in Floating-point types; this subsection is only about the token.)

float = [ '-' ] '0' 'x' hexdigit {hexdigit} '.' hexdigit {hexdigit}

'e' [ '-' ] digit {digit} 'f' digit {digit} 'e' digit {digit}

| '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit}

| '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit}

| '0' '+' 'o' 'o' digit {digit} 'e' digit {digit}

| '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} .

The finite form. Reading 0x1.0e0f24e8 left to right:

so the type of 0x1.0e0f24e8 is float24e8 (IEEE single precision) and the type of 0x1.8e1f53e11 is float53e11 (double).

The exponent is a power of sixteen, not two. This is the fact most likely to mislead. BigFloat.TryParseHexFormat computes the biased exponent using decExp * 4, so 0x1.0e1f24e8 is 1.0 hexadecimal times 16, that is 16, not 2:

procedure P()

{

assert 0x1.0e1f24e8 == 0x10.0e0f24e8;

assert 0x3.2e1f53e11 == 0x32.0e0f53e11;

}

boogie floatbase.bpl

Boogie program verifier finished with 1 verified, 0 errors

(Boogie’s own test suite annotates 0x3.2e1f53e11 as 50.0, which is 3.125 times 16.)

Both size fields must be greater than 1, and the value must be exactly representable in the stated format. The parser used for source literals is the strict one (BigFloat.TryParseExact), which rejects, with incorrectly formatted floating point:

• any literal that would lose precision — so the fraction may have more hex digits than the format has fraction bits only if the surplus low bits are zero (0x1.000002e0f24e8 is fine for float24e8, 0x1.0000001e0f24e8 is not);

• overflow to infinity — for float24e8 the largest legal exponent on a 0x1.0 significand is 31, since 31 times 4 plus the bias 127 is still below the reserved exponent 255;

• underflow all the way to zero. Subnormals that are still representable are accepted; values below the smallest subnormal are rejected rather than rounded.

procedure P()

{

var x: float24e8;

x := 0x1.0000001e0f24e8;

x := 0x1.0e32f24e8;

x := 0x0.8e-126f24e8;

x := 0x1.0e0f1e8;

}

boogie /noVerify floatbad.bpl

floatbad.bpl(4,8): error: incorrectly formatted floating point

floatbad.bpl(5,8): error: incorrectly formatted floating point

floatbad.bpl(6,8): error: incorrectly formatted floating point

floatbad.bpl(7,8): error: incorrectly formatted floating point

4 parse errors detected in floatbad.bpl

Hex digit e versus the exponent marker. The exponent marker is lowercase e, and e is also a hex digit, so the scanner and the value parser both resolve the ambiguity by taking the last e before the f as the marker. Uppercase E is unambiguous. 0x1.0ee0f24e8 is therefore significand 1.0E with exponent 0, and the printer says so:

const a: float24e8;

const b: float24e8;

const c: float24e8;

const d: float24e8;

axiom a == 0xA.Be0f24e8;

axiom b == 0x1.0ee0f24e8;

axiom c == 0nan24e8;

axiom d == -0x0.0e0f24e8;

boogie /noVerify /print:- floatnorm.bpl

const a: float24e8;

const b: float24e8;

const c: float24e8;

const d: float24e8;

axiom a == 0x0.ABe1f24e8;

axiom b == 0x1.0Ee0f24e8;

axiom c == 0NaN24e8;

axiom d == -0x0.0e0f24e8;

Boogie program verifier finished with 0 verified, 0 errors

The printer always emits exactly one hex digit before the point, upper-cases the hex digits, drops trailing zeros from the fraction and rewrites 0nan as 0NaN. It is not a canonical form: which digit lands before the point is an artifact of BigInteger.ToString("X"), which prepends a 0 whenever the top nibble is 8–F. So 0xA.Be0f24e8 comes back as 0x0.ABe1f24e8 and 0xF.0e0f24e8 as 0x0.Fe1f24e8, while 0x7.0e0f24e8, 0x3.0e0f24e8, 0x2.0e0f24e8 and 0x1.0e0f24e8 are reproduced verbatim. The printed value is always equal to the original.

Special values. 0NaNNeM, 0nanNeM, 0+ooNeM and 0-ooNeM. Only these exact spellings work; 0NAN24e8 does not lex as a float literal. The optional sign belongs only to the hexadecimal alternative, so there is no negative-infinity-by-sign spelling and no negative NaN: -0NaN24e8 parses as unary minus applied to a NaN literal, which then fails type checking with invalid argument type (float24e8) to unary operator -. Signed zeros are written with the finite form, 0x0.0e0f24e8 and -0x0.0e0f24e8.

BigFloat.TryCreateSpecialFromString still accepts +zero and -zero, but that code is unreachable from source text: the token grammar has no such alternative, and the special-value dispatcher only ever looks at a three-character slice. 0+zero53e11 lexes as 0, +, zero53e11 — Boogie’s own regression test Test/floats/RemovedZeroSpecialValue.bpl pins this down by expecting undeclared identifier: zero53e11.

The sign is part of the token. Because [ '-' ] is inside the token, a minus sign immediately followed by 0x is absorbed into the literal. Subtraction therefore needs a space:

procedure P()

{

var x: float24e8;

x := 0x3.0e0f24e8;

assert x -0x1.0e0f24e8 == 0x2.0e0f24e8;

}

boogie /noVerify floatminus.bpl

floatminus.bpl(5,12): error: ";" expected

1 parse errors detected in floatminus.bpl

Writing x - 0x1.0e0f24e8 verifies. Only -0x is affected; x-0 and x-1.5 are fine, because the scanner only enters the float branch after seeing -, 0, x in sequence.

2.8.6 Rounding-mode literals🔗

Five values of type rmode, each with a long and a short spelling. All ten spellings are reserved words.

const r: rmode;

axiom r == roundNearestTiesToEven;

procedure P()

{

assert r == RNE;

assert RTZ != RTP;

}

boogie /print:- roundingmodes.bpl

const r: \rmode;

axiom r == RNE;

procedure P();

implementation P()

{

assert r == RNE;

assert RTZ != RTP;

}

Boogie program verifier finished with 1 verified, 0 errors

The printer normalises the long spellings to the short ones. It also emits \rmode for the type name, because rmode is in the printer’s keyword array even though it is not a reserved word; that output does reparse, since the backslash is simply stripped.

2.8.7 String literals🔗

regularStringChar = ANY - quote - newLine.

string = quote { regularStringChar | "\\\"" } quote.

A string literal is a double-quoted run of characters. Any character is allowed except a double quote, a line feed and a carriage return; a string literal therefore cannot span lines. The only escape is \", and it is the only role the backslash plays: \\ is not an escape for a backslash, \n is a backslash followed by an n, and there is no way to write a control character.

function {:builtin "str.len"} len(string): int;

procedure P()

{

assert len("abc") == 3;

assert len("") == 0;

assert len("a b/c*d") == 7;

}

boogie strings.bpl

Boogie program verifier finished with 1 verified, 0 errors

String literals appear in two places, and they are decoded differently:

• As an attribute argument, the token text is taken apart with Substring(1, len-2) — exactly one character is removed from each end. The \" escape survives into the value as a backslash and a quote.

• As an expression of type string, the token text is taken apart with Trim('"'), which removes all leading and trailing quote characters.

Neither one actually decodes the escape. In an attribute the escaped quote round trips:

procedure {:tag "\""} P()

{

}

boogie /noVerify /print:- attrescape.bpl

procedure {:tag "\""} P();

implementation {:tag "\""} P()

{

}

Boogie program verifier finished with 0 verified, 0 errors

2.9 Operators and punctuation🔗

The remaining tokens are fixed character sequences. They are listed here for completeness; their meaning, arity and precedence are given in Expressions and operators.

A few notes. < and > double as the delimiters of a type-parameter list. * is both multiplication and the nondeterministic guard of if and while; ** is exponentiation. A lone | separates the arms of a Civl parallel call (call A() | B();); the two-character |{ and }| open and close a code expression. :: separates a quantifier’s binders from its body. div and mod are reserved words, not symbols; so are is and old. The alternatives of a datatype declaration are separated by commas, not by |.

2.10 Divergences from This is Boogie 2🔗

The 2008 paper describes the lexis only in passing, and several of its statements no longer hold.

• Identifier characters. The paper says identifiers consist of “letters (including non-English letters from the Unicode alphabet), digits ... and” a list of symbols. The implementation’s letter class is ASCII only, and non-ASCII bytes do not survive the scanner at all.

• Backslash. The paper lists \ among the characters an identifier may contain. In the implementation it may only appear as the first character of an identifier token, and it is stripped: it is an escape, not part of the name.

• The reserved word list. The paper’s list is assert, assume, axiom, bool, break, bv0, bv1, bv2, ..., call, complete, const, else, ensures, exists, false, finite, forall, free, function, goto, havoc, if, implementation, int, invariant, modifies, old, procedure, requires, return, returns, true, type, unique, var, where, while. Today bvK is an ordinary identifier, and finite and complete have been removed from the language entirely — type finite T; now simply declares a type constructor named finite with one parameter. Thirty-six words have been added since (real, datatype, div, mod, is, lambda, then, uses, hideable, revealed, reveal, hide, the ten rounding modes, and the Civl vocabulary action, asserts, async, atomic, both, left, measure, preserves, pure, refines, right, yield, push, pop).

• String literals. The paper says “string literals are not used anywhere else in Boogie” than attributes. Boogie now has a string type and string-literal expressions.

• Bitvector literals. The paper says Xbv K is legal only when X fits in K bits. Nothing checks this; oversized literals wrap.

• Not in the paper at all. Comments (the paper uses // in its examples but never defines it, and block comments and their nesting are never mentioned), the conditional preprocessor, the #line pragma, real literals, floating-point literals, rounding-mode literals, and the float/rmode/string/regex type names.