10 Algebraic datatypes🔗

A datatype declaration introduces a type together with a fixed set of constructors, each of which has a list of named, typed fields. Datatype values are built by applying a constructor, taken apart with the field selector ->, discriminated with the tester is, and rebuilt with the field-update expression ->(f := e).

Datatypes are entirely absent from This is Boogie 2 (2008): there is no datatype production in the paper’s grammar, no is, no ->, and the paper’s type section (§2) recognises only type constructors, built-in types and type synonyms. Everything in this chapter postdates the paper.

Two facts shape the rest of this chapter.

• Boogie generates no axioms for datatypes. Instead, each datatype is emitted to the prover as an SMT-LIB declare-datatypes command, and all the reasoning power — distinctness, injectivity, exhaustiveness, acyclicity — comes from the solver’s datatype theory. What the prover is told describes exactly what this buys you.

• Because declare-datatypes declares monomorphic sorts, polymorphic datatypes have to be eliminated before the VC is built. Boogie does this by monomorphising the whole program, which is only done under the default /typeEncoding:m. Under /typeEncoding:p or /typeEncoding:a a program that needs monomorphisation and contains datatypes is rejected outright. See Polymorphic datatypes and the type encoding.

10.1 Declaring a datatype🔗

Datatype<out DatatypeTypeCtorDecl datatypeTypeCtorDecl>

= "datatype"

{ Attribute }

Ident

[ TypeParams ]

"{"

Constructors

"}"

.

Constructors = Constructor { "," Constructor } .

Constructor  = Ident "(" [ AttributesIdsTypeWheres ] ")" .

(Source/Core/BoogiePL.atg, productions Datatype, Constructors and Constructor, with the semantic actions elided.)

A datatype declaration is a top-level declaration, on a par with type, const, function, axiom, var, procedure and implementation. It is not terminated by a semicolon — unlike type — and there is no ordering requirement: a datatype may mention a datatype declared later in the file.

Because the field list uses the same AttributesIdsTypeWheres production as procedure formals, consecutive fields of the same type may share one type annotation: Point3(x, y, z: int) declares three int fields, and /print expands it back to Point3(x: int, y: int, z: int).

datatype Shape {

Circle(r: int),

Rect(w: int, h: int)

}

procedure Area(s: Shape) returns (a: int)

requires s is Rect ==> s->w >= 0 && s->h >= 0;

ensures  s is Rect ==> a == s->w * s->h;

{

if (s is Circle) {

a := 3 * s->r * s->r;

} else {

a := s->w * s->h;

}

}

boogie shapes.bpl

Boogie program verifier finished with 1 verified, 0 errors

10.1.1 Syntactic rules🔗

The grammar is stricter than it looks; the following are all rejected.

• At least one constructor is required. Constructors is Constructor { "," Constructor }, with no empty alternative, so there is no empty datatype.

  datatype Empty { }

  e2.bpl(1,18): error: invalid Ident

  1 parse errors detected in e2.bpl

• The parentheses after a constructor name are mandatory, even for a nullary constructor.

  datatype D { C }

  noparens.bpl(1,16): error: "(" expected

  1 parse errors detected in noparens.bpl

• No trailing comma after the last constructor, and no trailing semicolon after the closing brace.

  datatype D { C(), }

  trailing.bpl(1,19): error: invalid Ident

  1 parse errors detected in trailing.bpl

  datatype D { C() };

  semi.bpl(1,19): error: EOF expected

  1 parse errors detected in semi.bpl

• Fields may not carry where clauses. The field list is parsed by the same production that parses procedure formals, but with where-clauses disabled and the context string "datatype constructor".

  datatype D { C(f: int where f > 0) }

  wherefield.bpl(1,33): error: where clause not allowed on datatype constructor

  1 parse errors detected in wherefield.bpl

• datatype and is are reserved words. They are literal tokens in the grammar, so neither can be used as an identifier or as an attribute name. This is why the older attribute-based encoding type {:datatype} Tree; with function {:constructor} ... no longer parses. That encoding was replaced by the datatype declaration in Boogie 2.16.1, which also deleted the Program.ProcessDatatypes pass that used to read the two attributes. Note that this predates Boogie 3.0: no 3.x release has ever accepted the attribute form.

  type {:datatype} Tree;

  function {:constructor} leaf(): Tree;

  legacy.bpl(1,8): error: invalid Ident

  1 parse errors detected in legacy.bpl

10.1.2 Names and name spaces🔗

A datatype declaration creates one TypeCtorDecl (a subclass, DatatypeTypeCtorDecl) and one Function per constructor (a subclass, DatatypeConstructor). Consequently:

• The datatype name lives in the type name space and must not collide with another type or type synonym:

  datatype A { A1(f: int) }

  type A;

  ns.bpl(3,5): Error: more than one declaration of type name: A

  1 name resolution errors detected in ns.bpl

• Constructor names live in the function name space and must not collide with a function or another constructor of any datatype:

  datatype D { C(f: int) }

  function C(x: int): int;

  ctorclash.bpl(2,9): Error: more than one declaration of function name: C

  1 name resolution errors detected in ctorclash.bpl

  Duplicate constructor names inside one datatype are caught by the parser, not the resolver:

  datatype Split<T> {

  Left(i: T),

  Left(i: T)

  }

  dupctor.bpl(3,12): error: constructor name Left used more than once in datatype

  1 parse errors detected in dupctor.bpl

• Because a datatype and its constructor are in different name spaces, the common idiom of naming a single-constructor datatype after itself (datatype Point { Point(x: int, y: int) }) is legal, and is what the standard library does.

• Field names are scoped to their datatype, so two datatypes may use the same field name for different types without interference. Within one constructor, field names must be distinct:

  datatype D { C(f: int, f: bool) }

  dupfield.bpl(1,23): Error: more than one declaration of variable name: f

  1 name resolution errors detected in dupfield.bpl

10.1.3 Attributes🔗

Attributes are accepted on the datatype (before the name) and on each field (before the field name); there is no place to attach an attribute to a constructor.

datatype {:mydt} D { C1({:myfield} f: int), C2() }

procedure P(d: D) { assert d is C1 || d is C2; }

They parse and are stored on the declaration, but no core Boogie feature reads them. In particular, Civl does not: its linear type collector decides whether a datatype carries permissions by looking at the types of the constructor fields, never at attributes attached to them. Treat datatype and field attributes as inert.

10.1.4 Type parameters🔗

Type parameters are written in angle brackets and separated by commas. This is not the syntax used by ordinary type constructors, which take whitespace-separated parameters and no brackets (type Barrel _;). Applying the datatype to arguments, on the other hand, uses the ordinary juxtaposition syntax: Split int bool, Map (One Loc) (Node int).

datatype Split<X, Y> {

Left(i: X, j: Y),

Right(i: X, k: Y)

}

procedure P(s: Split int bool) returns (t: Split int bool)

{

t := s->(i := 5);

assert t->i == 5;

}

Boogie program verifier finished with 1 verified, 0 errors

Every constructor of a datatype is typed with all of the datatype’s type parameters, regardless of which of them it actually uses, and its result type is the datatype applied to those parameters. So Left above has signature Left<X, Y>(i: X, j: Y): Split X Y.

10.1.5 Fields shared between constructors🔗

The same field name may appear in more than one constructor of a datatype. When it does, all occurrences must have the same type, after normalising through each constructor’s result type:

datatype Split<X, Y> {

Left(i: X, j: Y),

Right(i: Y, k: X)

}

shared4.bpl(3,8): Error: type mismatch between field i and identically-named field in constructor Left

1 type checking errors detected in shared4.bpl

The message does not print the expected type; the constructor it names is always the first constructor that declares the field, in declaration order, and it is that constructor’s field type every later one is compared against (DatatypeTypeCtorDecl.Typecheck). Sharing a field name changes the meaning of -> and of field update; see Field access: e->f and Field update: e->(f := v).

10.1.6 Well-foundedness🔗

After resolution, Program.CheckDatatypesWellFounded computes the least set of datatypes that have at least one constructible constructor, where a constructor is constructible if every field type is constructible, a map type is constructible if its index and result types are, a datatype is constructible if it is already in the set, and every other type is constructible. Any datatype not in the fixpoint is an error.

In practice this means: every datatype needs a reachable base case, and a recursive occurrence hidden under a map type does not count as a base case.

Note that the error is reported with the pseudo-position (0,-1) and lists all offending datatypes at once, so a mutual cycle produces one message naming the whole group. The shipped test Test/datatypes/cycle.bpl reports List1, List2, Foo, List3, List4 in a single error.

Mutual recursion is fine as long as the group has a base case, and a map-typed recursive field is fine as long as the datatype has some other constructible constructor:

10.2 Constructors🔗

A constructor is an ordinary Boogie function, so it is applied with the ordinary call syntax and obeys the ordinary type-inference and arity rules. Nullary constructors still need the empty argument list, both at declaration and at use; Red on its own is an undeclared identifier.

Type parameters are inferred from the arguments as for any polymorphic function. If a constructor mentions a type parameter in none of its fields, the parameter is unconstrained at that call site and Boogie warns and picks int:

In a context that fixes the type, inference succeeds silently:

Arity and argument-type errors are reported by the generic function machinery (these two lines come from the errs.bpl program shown in full in Field access: e->f):

errs.bpl(8,9): Error: wrong number of arguments to function: A1 (0 instead of 1)

errs.bpl(9,12): Error: invalid type for argument 0 in application of A1: bool (expected: int)

Because constructors are functions, they may appear anywhere a function application may: in axioms, in triggers, in {:define} function bodies, in lambdas, and as procedure arguments.

10.3 Testers: e is Ctor🔗

Power = IsConstructor [ "**" Power ] .

IsConstructor

= UnaryExpression

[ "is" Ident ]

.

e is C has type bool and holds when e was built by constructor C. Its left operand must have a datatype type and C must be a constructor of that datatype. The next three lines, and every other field_access_type_error.bpl excerpt in this chapter, come from the shipped test Test/datatypes/field_access_type_error.bpl, which collects the datatype-related type errors in one file:

field_access_type_error.bpl(8,14): Error: is-constructor must be applied to a datatype, int is not a datatype

field_access_type_error.bpl(13,14): Error: is-constructor must be applied to a datatype, T is not a datatype

field_access_type_error.bpl(22,14): Error: datatype Perm does not have a constructor with name Middle

Precedence. is sits between UnaryExpression and Power in the expression grammar. It therefore binds tighter than **, than the multiplicative and additive operators, than the relational operators, than ==, and than the boolean connectives, and looser than ->, [] and prefix !/-. So

d is C1 && d->f == 0

parses as (d is C1) && ((d->f) == 0) — which is what you want — and

d->f is C2

parses as (d->f) is C2. But because prefix ! is part of UnaryExpression, negation binds tighter than is, and the natural-looking form is a type error:

Write !(d is C1). Binding tighter than arithmetic is equally surprising in the other direction — 1 + d is C1 groups as 1 + (d is C1):

There is no chaining: the is suffix is optional but not repeatable.

10.4 Field access: e->f🔗

ArrayExpression

= AtomExpression

{ "[" ... "]"

|

"->"

(

Ident

|

"(" Ident ":=" Expression ")"

)

}

.

e->f selects the field named f. The -> and [] suffixes are in the same repetition of the same production, so selection, subscripting and update compose freely and associate to the left, and any AtomExpression — including a function application, an old, a parenthesised expression — can be the receiver.

Resolution of ->f is deferred to type checking, because the field’s meaning depends on the datatype of the receiver, which is only known then. Type checking requires the receiver’s type to expand to a datatype and the datatype to declare the field:

The two remaining diagnostics come from applying -> to a non-datatype:

field_access_type_error.bpl(7,12): Error: field-access must be applied to a datatype, int is not a datatype

field_access_type_error.bpl(12,12): Error: field-access must be applied to a datatype, T is not a datatype

10.4.1 Selectors are total, but underspecified off their own constructor🔗

A selector is a total function. s->w is well-defined even when s is a Circle; it just denotes an unspecified value. It is the same unspecified value for the same s — selectors are functions, not nondeterministic reads — but nothing else is known about it.

This is a real source of vacuous-looking specifications: a postcondition like ensures r->hd == 0; on a value that turns out to be Nil constrains nothing useful. Guard field accesses with is in specifications where the constructor is not otherwise determined.

10.4.2 Shared field names produce a conditional🔗

When a field name occurs in several constructors, e->f expands to a conditional over the testers. Concretely, Boogie2VCExpr starts from the accessor of the first constructor that declares f and wraps each later one in an if:

datatype D { C1(f: int, g: int), C2(f: int, h: bool) }

procedure P(d: D) returns (e: D)

{

e := d->(f := 7);

assert e->f == 7;

assert (d is C1) == (e is C1);

assert (d is C2) == (e is C2);

}

The verification condition (from /proverLog:) shows the shape exactly — e->f became (ite (is-C2 e) (f#C2 e) (f#C1 e)):

(assert (not

(=> (= (ControlFlow 0 0) 5) (let ((anon0_correct  (=> (= e@0 (ite (is-C2 d) (C2 7 (|h#C2| d)) (C1 7 (|g#C1| d)))) (and (=> (= (ControlFlow 0 2) (- 0 4)) (= (ite (is-C2 e@0) (|f#C2| e@0) (|f#C1| e@0)) 7)) (=> (= (ite (is-C2 e@0) (|f#C2| e@0) (|f#C1| e@0)) 7) (and (=> (= (ControlFlow 0 2) (- 0 3)) (= (is-C1 d) (is-C1 e@0))) (=> (= (is-C1 d) (is-C1 e@0)) (=> (= (ControlFlow 0 2) (- 0 1)) (= (is-C2 d) (is-C2 e@0))))))))))

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

PreconditionGeneratedEntry_correct)))

))

The first constructor that declares f is the fall-through branch, so for a value of a constructor that does not declare f at all, e->f silently reads that constructor’s selector — again a total but unconstrained value.

10.5 Field update: e->(f := v)🔗

e->(f := v) is an expression of the same type as e, denoting e with field f replaced by v. It is pure syntactic sugar: FieldUpdate is expanded by FieldAccess.Update into a constructor application whose other arguments are field selections of the original value. The type checker requires the right-hand side to match the field’s type:

field_access_type_error.bpl(61,11): Error: right-hand side in field update with wrong type: bool (expected: int)

For a field declared in exactly one constructor C(f1, ..., fn), the expansion is C(e->f1, ..., v, ..., e->fn). For a shared field the expansion is a conditional, as shown in Field access: e->f: d->(f := 7) became (ite (is-C2 d) (C2 7 (h#C2 d)) (C1 7 (g#C1 d))).

10.5.1 Trap: updating a field the value does not have🔗

Because the expansion always produces a constructor application, and because the fall-through case is the first constructor that declares the field, updating a field on a value of a constructor that does not declare that field silently changes the constructor. There is no error, no warning, and no proof obligation.

The verification condition confirms that e is literally (C1 7 (g#C1 d)), built out of an unconstrained g#C1 read of a C2 value:

(assert (not

(=> (= (ControlFlow 0 0) 3) (let ((anon0_correct  (=> (and (= e@0 (C1 7 (|g#C1| d))) (= (ControlFlow 0 2) (- 0 1))) (is-C1 e@0))))

(let ((PreconditionGeneratedEntry_correct  (=> (and (is-C2 d) (= (ControlFlow 0 3) 2)) anon0_correct)))

PreconditionGeneratedEntry_correct)))

))

If you rely on a field update preserving the constructor, assert or assume the tester explicitly.

10.6 Statements over datatypes🔗

10.6.1 Field assignment🔗

LabelOrAssign

= Ident

( ...

| { MapAssignIndex | FieldAccess }

{ "," Ident { MapAssignIndex | FieldAccess } }

":=" { Attribute } Expression { "," Expression } ";"

)

.

FieldAccess = "->" Ident .

An assignment left-hand side is an identifier followed by any sequence of map indexings and field selections. Note that the left-hand side form is ->Ident only; the parenthesised update form ->(f := e) is an expression and cannot appear on the left.

x->f := e; is shorthand for x := x->(f := e);, and the desugaring composes down an arbitrary path.

Maps and fields interleave in either order:

Since the ultimate target of the assignment is the root variable (FieldAssignLhs.DeepAssignedVariable delegates to the receiver), a field assignment to a global requires that global in the modifies clause:

A field left-hand side may be one of several targets of a simultaneous assignment:

but it may not be an output of a call (invalid CallParams) nor an operand of havoc, which both take bare identifiers.

10.6.2 Unpack🔗

LabelOrAssign

= Ident

( ...

| "(" Idents ")" ":=" { Attribute } Expression ";"

| ...

)

.

C(x1, ..., xn) := e; is the unpack command: it asserts that e was built with C and then assigns each field of e to the corresponding variable. UnpackCmd.ComputeDesugaring produces exactly

assert e is C;

x1, ..., xn := e->f1, ..., e->fn;

where the assertion carries the description "the precondition for unpack could not be proved".

Restrictions, all checked:

• The left-hand side must be a constructor application. An ordinary function of the right signature is not enough:

  datatype Point { Point(x: int, y: int) }

  function F(a: int, b: int): Point;

  procedure P(p: Point) returns (a: int, b: int) { F(a, b) := p; }

  unp5.bpl(3,57): Error: left side of unpack command must be a constructor application

  1 type checking errors detected in unp5.bpl

• Its arguments are parsed as Idents, so they must be plain identifiers — a field path or map index is a parse error:

  datatype Point { Point(x: int, y: int) }

  datatype Line { Line(from: Point, to: Point) }

  procedure P(p: Point) returns (l: Line, b: int) { Point(l->from->x, b) := p; }

  unppath.bpl(3,58): error: ")" expected

  1 parse errors detected in unppath.bpl

  and a nullary constructor cannot be unpacked at all, because Idents requires at least one identifier:

  datatype D { C() }

  procedure P(d: D) { C() := d; }

  unp0.bpl(2,23): error: invalid Ident

  1 parse errors detected in unp0.bpl

• The number of identifiers must match the constructor’s arity:

  datatype Point { Point(x: int, y: int) }

  procedure P(p: Point) returns (a: int) { Point(a) := p; }

  unp4.bpl(2,41): Error: wrong number of arguments to function: Point (1 instead of 2)

  1 type checking errors detected in unp4.bpl

• No identifier may be repeated:

  field_access_type_error.bpl(45,13): Error: variable a is assigned more than once in unpack command

• Each identifier must be assignable — not an in-parameter, and, if global, in the modifies clause:

  field_access_type_error.bpl(50,13): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g

  field_access_type_error.bpl(56,13): Error: command assigns to an immutable variable: a

Putting unpack and field assignment together, this procedure

datatype Shape { Circle(r: int), Rect(w: int, h: int) }

procedure P(s: Shape) returns (t: Shape)

requires s is Rect;

ensures t->w == s->w + 1;

{

var w, h: int;

Rect(w, h) := s;

t := s;

t->w := w + 1;

}

produces this verification condition, in which every datatype operation has become an SMT-LIB constructor, selector or tester application:

(assert (not

(=> (= (ControlFlow 0 0) 4) (let ((anon0_correct  (and (=> (= (ControlFlow 0 2) (- 0 3)) (is-Rect s)) (=> (is-Rect s) (=> (and (and (= w@0 (|w#Rect| s)) (= h@0 (|h#Rect| s))) (and (= t@0 (Rect (+ w@0 1) (|h#Rect| s))) (= (ControlFlow 0 2) (- 0 1)))) (= (|w#Rect| t@0) (+ (|w#Rect| s) 1)))))))

(let ((PreconditionGeneratedEntry_correct  (=> (and (is-Rect s) (= (ControlFlow 0 4) 2)) anon0_correct)))

PreconditionGeneratedEntry_correct)))

))

10.7 What the prover is told🔗

Boogie emits no axioms for datatypes. TypeDeclCollector deliberately skips DatatypeConstructors when declaring functions and returns early for datatype sorts; instead SMTLibProcessTheoremProver.PrepareDataTypes groups the datatypes into strongly connected components of the "field type mentions" graph and emits one declare-datatypes per component. For the Shape example above:

(declare-datatypes ((T@Shape 0)) (((Circle (|r#Circle| Int) ) (Rect (|w#Rect| Int) (|h#Rect| Int) ) ) ))

The naming scheme, useful when reading a /proverLog: file:

• the sort is T@Name;

• constructors keep their Boogie name;

• a selector is field#Ctor;

• a tester is is-Ctor.

Name collisions with user declarations are handled by the prover namer, which appends @@n; a user function genuinely called f#C (# is a legal identifier character in Boogie) coexists with the selector f#C without trouble.

All datatypes in the program are declared, whether or not the implementation being verified mentions them, and /prune does not change this:

10.7.1 The properties you get🔗

Everything below follows from the SMT datatype theory, so it holds without any user axioms:

Only the last procedure fails, as it should. Recursive datatypes additionally get acyclicity for free:

What you do not get is an induction principle. Any property that needs induction over a recursive datatype has to be proved by other means — a recursive pure procedure whose postcondition is the inductive hypothesis is the idiom used by the standard library and the shipped tests.

10.7.2 Counterexample models🔗

Datatype values appear in /mv: output as constructor applications:

datatype Shape { Circle(r: int), Rect(w: int, h: int) }

procedure P(s: Shape) { assert s is Circle; }

boogie /mv:- model.bpl

model.bpl(2,25): Error: this assertion could not be proved

Execution trace:

model.bpl(2,25): anon0

*** MODEL

s -> (Rect 4 5)

ControlFlow -> {

0 0 -> 3

0 2 -> (- 1)

0 3 -> 2

else -> (- 1)

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

s -> (Rect 4 5)

*** END_STATE

*** END_MODEL

Boogie program verifier finished with 0 verified, 1 error

10.8 Polymorphic datatypes and the type encoding🔗

declare-datatypes declares sorts of arity 0, so a polymorphic datatype cannot be sent to the prover as such. SMTLibProverContext.DeclareType throws "Polymorphic datatypes are not supported" if one ever reaches it. Boogie avoids that by monomorphising: for each type instantiation actually used, the monomorphiser creates a fresh, ground DatatypeTypeCtorDecl with fresh constructor names.

The prover sees a monomorphic instance whose name carries a disambiguating suffix:

(declare-sort T@A_46 0)

(declare-datatypes ((T@Box_68 0)) (((Box_68 (|v#Box_68| T@A_46) ) ) ))

10.8.1 Interaction with /typeEncoding🔗

ExecutionEngine decides as follows, immediately after type checking:

• If the program is already monomorphic, TypeEncodingMethod is forced to Monomorphic regardless of what /typeEncoding said, and no monomorphisation pass runs.

• Otherwise, if the encoding is Monomorphic (the default), the monomorphiser runs. It can fail with "Unable to monomorphize input program: unhandled polymorphic features detected" or "... expanding type cycle detected".

• Otherwise — a polymorphic program under /typeEncoding:p or /typeEncoding:a — the presence of any datatype declaration is a fatal error.

So a monomorphic datatype program is happily verified under /typeEncoding:p, because the option is overridden before the datatype check is reached — this is the Shape program from Declaring a datatype:

while a polymorphic one is not:

The same message appears for /typeEncoding:a. Note that the message is printed as a fatal error with no source location, and that the actual trigger is "the program needed monomorphisation and has datatypes", not "the program has polymorphic datatypes".

10.9 Datatypes, maps and quantifiers🔗

Datatypes compose with maps in both directions. A datatype may be a map’s domain or range, and a map may be the type of a datatype field.

A map-typed field becomes an SMT Array inside the datatype under the default array theory, and an uninterpreted sort under /useArrayAxioms; both work.

The two encodings differ only in the sort used for the field:

(declare-datatypes ((T@Env 0)) (((Env (|vars#Env| (Array Int Int)) (|n#Env| Int) ) ) ))

(declare-sort |T@[Int]Int| 0)

(declare-datatypes ((T@Env 0)) (((Env (|vars#Env| |T@[Int]Int|) (|n#Env| Int) ) ) ))

10.9.1 Triggers🔗

Constructor applications, selector applications and tester applications are all legal trigger terms; each is a genuine SMT function application, so each becomes a :pattern.

which emits

(assert (forall ((b T@Box) ) (! (= (g (|v#Box| b)) 0)

:qid |trig2bpl.3:15|

:skolemid |0|

:pattern ( (|v#Box| b))

)))

and testers work too:

Beware that a selector used as a trigger fires on every value of the datatype, since selectors are total; a tester used as a trigger fires on every term the solver has produced a tester for. Both are much more permissive than they look.

10.9.2 Recursive definitions🔗

There is no match construct and no built-in recursion. The idiom for a recursive function over a datatype is an uninterpreted function plus one axiom per constructor, triggered on the constructor application:

A {:define} function can pattern-match with is and -> but cannot recurse — definitions are expanded, and cycles are rejected:

10.10 Pattern-style specifications🔗

Boogie has no pattern matching, so specifications are written with testers as guards and selectors as projections. The two rules of thumb are: guard every selector whose constructor is not already determined, and state the constructor of a result explicitly when it matters.

The unpack command is the specification-side counterpart of a single-case match: it makes the constructor a proof obligation rather than a silently underspecified read. Prefer

Rect(w, h) := s;

over

w, h := s->w, s->h;

when s is expected to be a Rect: the first form fails loudly if it is not.

10.11 Standard library datatypes🔗

The libraries loaded with /lib: declare several datatypes that most datatype code ends up using. From base.bpl:

datatype Option<T> { None(), Some(t: T) }

datatype Vec<T> { Vec(contents: [int]T, len: int) }

datatype Map<T,U> { Map(dom: [T]bool, val: [T]U) }

datatype One<T> { One(val: T) }

datatype Cell<T,U> { Cell(key: One T, val: U) }

datatype Unit { Unit() }

datatype Tag<V> { Tag(loc: Loc, val: V) }

and from node.bpl:

datatype Node<T> { Node(next: Option Loc, val: T) }

They behave like any other datatype; the operations over them are described in The standard library.

// Option, Vec, Map, One, Cell and Unit come from the base library.

procedure P(o: Option int) returns (n: int)

ensures o is Some ==> n == o->t;

ensures o is None ==> n == 0;

{

if (o is None) { n := 0; } else { n := o->t; }

}

Civl uses datatypes heavily for linear permissions: One is the primitive permission carrier, and a user datatype is treated as carrying permissions when one of its constructor fields has a permission-carrying type. The shipped tests Test/datatypes/list-reversal-iterative.bpl, list-reversal-recursive.bpl and node-client.bpl are worked examples; see Civl: concurrency and refinement.

10.12 Divergences from This is Boogie 2🔗

This is Boogie 2 does not describe datatypes in any form. In particular:

• The paper’s grammar summary (Appendix A) has no datatype declaration; TypeDecl is only TypeConstructor or TypeSynonym (§2.0, §2.2).

• The paper’s expression grammar (§4) has neither -> nor is; the only postfix forms are map selection and map update (§4.1).

• The paper’s assignment statement (§9.3, and Lhs ::= Id MapSelect* in Appendix A) has no unpack command and no field-assignment left-hand side; assignment targets are identifiers followed by map selections only.

• The paper describes a type constructor as denoting a nonempty, normally infinite set of individuals, with finite available to allow a finite one (§2.0). Datatypes are the opposite: their inhabitants, and their equalities, are completely determined by the constructors, and there is no cardinality knob.

The paper’s idiom for a closed enumeration (§2.0, example (0)) is an uninterpreted type, unique constants and an explicit closure axiom. That idiom is also where the difference bites hardest. With today’s default prover options the closure axiom has no trigger and smt.mbqi is off, so it never fires, while the datatype’s exhaustiveness is a native property of the sort:

Only the first assertion — the one about the paper’s encoding — fails, because the axiom is emitted without a :pattern:

(assert (forall ((ce T@RGBColor) ) (!  (or (or (= ce red) (= ce green)) (= ce blue))

:qid |enumbpl.7:15|

:skolemid |0|

)))

(Triggering is a general Boogie topic, not a datatype one; the point here is only that the datatype assertions need no help.) Note also that the paper’s finite keyword no longer exists in the grammar: type finite RGBColor; now parses as the declaration of a unary type constructor named finite.

Everything in this chapter should therefore be read as an addition to the paper rather than a refinement of it.