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

Types

TypeDecl ::=
  type Identifier

This declares a nonempty but otherwise uninterpreted type.

There are two built-in types, so the use of type is

Type ::=
  | bool
  | int
  | Identifier

Taggers

Tagger ::=
  tagger Identifier for Type

Functions

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

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

Axioms

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

The explains clause names a set of functions. The axiom is added to the antecedent of a proof obligation if all of the functions have been included in the proof obligation.

Procedures

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

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

Spec ::=
  | requires AExpression
  | ensures AExpression

AExpression ::=
  | Expression
  | BlockStmt

There are restrictions on the BlockStmt version of AExpression as to which statements the block is allowed to contain.

There are three parameter modes: in, inout, and out. The absence of inout and out indicates an in-argument.

In the procedure body, in-parameters are immutable and inout- and out-parameters are mutable.