Top-level declarations

A program consists of a list of top-level declarations. The order of these is irrelevant.

Program ::=
  | TypeDecl
  | Tagger
  | Function
  | Axiom
  | Procedure

A program has three separate namespaces for top-level declarations: one is for types, another is for taggers and functions, and the third is for procedures. In other words, the language allows, for example, a procedure to have the same as a function.

Types

TypeDecl ::=
  type Identifier

A declaration type A declares A to be a nonempty but otherwise uninterpreted type.

There are three built-in types, bool, int, and tag. The use of a type is therefore

Type ::=
  | bool
  | int
  | tag
  | Identifier

Taggers

Tagger ::=
  tagger Identifier for Type

A tagger is a special function from the given type to a tag. The declaration tagger G for A has the effect of declaring a function

function G(subject: A): tag

This function is available for use like any other function in the program.

What makes a tagger special is that it can be mentioned in the tag clause of other function declarations, see Functions with disjoint images.

Functions

Function ::= 
  function Identifier "(" FParameter*, ")" ":" Type [ tag Identifier ]
  [
    ( when Expression )*
    "{" Expression "}"
  ]

FParameter ::=
  [ injective ] Identifier ":" Type

A declaration function F(x: X): Y declares a function from X to Y.

  • The name of the function must not be the same as any other function or tagger.

  • The must not be any duplicate names among the function’s parameters.

  • The identifier in the optional tag clause must denote a tagger.

  • Any when expression must have type bool, and the type of the optional body expression (between curly braces) must be function’s result type.

  • The free variables of the when expressions and body must be some subset of the function’s parameters.

Function definition

A function can be given a definition by providing a body. For example:

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

Such a definition has the effect of declaring an axiom

axiom explains Double
  forall x: int
    pattern Double(x)
    Double(x) == x + x

but better retains the intent behind such an axiom. For example, a B3 back end may give better error diagnostics if the definition is associated with the function.

Underspecified functions

Functions in B3 are total. However, a function may be underspecified. Then when clause is used to give the condition under which the body applies. For example,

function Decrease(x: int): int
  when 0 < x
{
  x - 1
}

defines Decrease for positive integers and leaves it uninterpreted for non-positive integers, as would be stated by the axiom

axiom explains Decrease
  forall x: int
    pattern Decrease(x)
    0 < x ==>
    Decrease(x) == x - 1

Functions that are injective in their arguments

Many functions are injective in one or more of their arguments. This can be indicated in a function declaration by preceding a parameter with injective. For example, if GPSPoint and string are types, then

function MapCoordinate(injective x: int, injective y: int, label: string): GPSPoint

says that MapCoordinate is injective in each of its first two parameters. Consequently, the first check condition in the following program snippet is provable:

var a := MapCoordinate(59, 18, |Stockholm: string|)
var b := MapCoordinate(48, -122, |Seattle: string|)
var c := MapCoordinate(48, -122, |EmeraldCity: string|)

check a != b // yes, follows from injectivity

check b == c // don't know
check b != c // don't know

whereas injectivity alone is not enough to determine which of the second and third conditions holds.

A function F declared to be injective in one of its parameters x automatically introduces the corresponding inverse function, named F..x. That is, the declaration of MapCoordinate above also introduces the functions

function MapCoordinate..x(subject: GPSPoint): int
function MapCoordinate..y(subject: GPSPoint): int

with the associated axioms

axiom explains MapCoordinate
  forall x: int, y: int, label: string
    pattern MapCoordinate(x, y, label)
    MapCoordinate..x(MapCoordinate(x, y, label)) == x

axiom explains MapCoordinate
  forall x: int, y: int, label: string
    pattern MapCoordinate(x, y, label)
    MapCoordinate..y(MapCoordinate(x, y, label)) == y

Note

User-defined identifiers are not allowed to contain the substring .., so the names of these automatically generated inverse functions are unique.

Note

A semantically equivalent way of axiomatizing injectivity for MapCoordinate is

axiom explains MapCoordinate
  forall x0: int, y0: int, label0: string, x1: int, y1: int, label1: string
    pattern MapCoordinate(x0, y0, label0), MapCoordinate(x1, y1, label1)
    MapCoordinate(x0, y0, label0) == MapCoordinate(x1, y1, label1)
    ==>
    x0 == x1 && y0 == y1

However, this axiomatization gives rise to poor SMT performance because the number of matches for its pattern is quadratic is the number of MapCoordinate terms in the proof context. It’s better to mark parameters with injective, whether or not the inverse functions are used elsewhere in the B3 program.

Functions with disjoint images

Sometimes, two functions, say F and G, have the property that their functional images are disjoint. In other words, the values returned by F are never the same as the values returned by G. A group of functions can be declared to pairwise have this behavior. This is done by associating a tagger with each of the functions in the group.

For example, the program snippet

type Drink
tagger Variety for Drink

function Coffee(strength: int): Drink tag Variety
function Tea(organic: bool): Drink tag Variety
function SoftDrink(hasSugar: bool): Drink tag Variety

declares three Drink functions, Coffee, Tea, and SoftDrink. By also declaring the tagger Variety and declaring the functions with tag Variety, these declarations say that functions Coffee, Tea, and SoftDrink return disjoint values. That is, Coffee(x) is not equal to Tea(y) and not equal to SoftDrink(z), regardless of the values of the arguments x, y, and z.

The effect of a tag clause on a function F is to declare an additional function, F..tag. So, for Coffee, the function is

function Coffee..tag(): tag

B3 arranges for all such F..tag functions to return distinct values (across all names of taggers). Hence, the condition

Coffee..tag() != Tea..tag()

holds. The result values of F and “tagged” with the value F..tag(). More precisely, F’s tagger function returns F..tag() when applied to the result values of F. Applied to the Drink example, we have

axiom explains Coffee
  forall strength: int
    pattern Coffee(strength)
    Variety(Coffee(strength)) == Coffee..tag()

Example

The combination of injective and tag are useful in declaring what essentially are the constructors of algebraic datatypes. For example, to represent a type like

datatype List = Nil() | Cons(head: int, tail: List)

from another programming language, one can in B3 declare

type List
tagger ListTagger for List

function Nil(): List tag ListTagger
function Cons(injective head: int, injective tail: List): List tag ListTagger

Inconsistent function definitions

Caution

It is possible to declare a function body that gives rise to a logical inconsistency. For example, the declaration

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

allows one to conclude Bad(100) == 1 + Bad(100), which is false.

Logical inconsistencies can also arise from a combination of a body and the injective or tag. For example,

function G(injective x: int): int { 5 }

would let one conclude

G..x(G(20)) == 20 &&
G..x(G(21)) == 21 &&
G(20) == G(21)

which also implies false.

The B3 language itself does not forbid declarations like the above that cause logical inconsistencies (but third-party tools might try to detect them). The reason for not forbidding them is to allow a source language to encode its proof obligations into B3 without first having to detect the inconsistencies; if the source language is concerned with such inconsistencies, then it would encode additional proof obligations in B3 that detect the source-language inconsistencies. The explains clauses of axioms in B3 allow these two encodings to be done simultaneously.

Axioms

Axiom ::=
  axiom [ explains Identifier+, ]
    Expression

A declaration axiom e introduces a property that can be used at any time while reasoning about the program.

  • The expression must have type bool.

  • Each identifier in the explains clause must denote a function or tagger.

The axiom gets used (is active) in those proof obligations where all of the functions in the explains clause appear. A functions mentioned in the expression of an active axiom may in turn activate further axioms.

Procedures

Procedure ::=
  procedure Identifier "(" PParameter*, ")"
    Spec*
  [ BlockStmt ]

PParameter ::=
  [ inout | out ] Identifier ":" Type [ autoinv Expression ]

Spec ::=
  | requires AExpression
  | ensures AExpression

AExpression ::=
  | Expression
  | BlockStmt

A declaration procedure M(x: X, inout y: Y, out z: Z) introduces a procedure with an in-parameter x, an inout-parameter y, and an out-parameter z. A procedure is a named signature with a pre- and postcondition specification and an optional implementation body.

  • The name of the procedure must not be the same as any other procedure.

  • The must not be any duplicate names among the procedure’s parameters.

  • Each procedure parameter can be pass in (default), out (indicated by out), or both (inout).

  • Any autoinv expression (auto-invariant) must have type bool.

  • Any expression following requires (precondition) or ensures (postcondition) must have type bool.

  • The free variables of the autoinv expression of an in- or inout-parameter or of a requires clause must be some subset of the procedure’s in- and inout-parameters.

  • The free variables of the autoinv expression of an out-parameter or of an ensures clause must be some subset of the procedure’s parameters. In addition, these expressions and clauses are allowed to mention the old form of inout-parameters.

  • The optional body of a procedure can mention any of the procedure’s parameters. In addition, the body is allowed to mention the old form of inout-parameters. In the body, inout- and out-parameters are mutable variables, where in-parameters and the old form of inout-parameters are immutable variables.

The BlockStmt form of an AExpression is a restricted form of statements, described later.

There are three parameter modes, in (denoted by the absence of the keywords inout and out), inout (denoted by inout), and out (denoted by out). In-parameters are passed by value from the caller to the callee, out-parameters are passed by value from the callee to the caller, and inout-parameters combine the two, passing a value from caller to callee and then passing a possibly different value back to the caller.

For a description of auto-invariants, see Auto-invariants.

If the procedure has a body, it is an error if a program trace reaches the end of the block when one of the postconditions does not hold.