6 Procedures, implementations and specifications

8.17

6 Procedures, implementations and specifications🔗

A procedure declares a name, a signature and a specification. An implementation supplies a body for a previously declared procedure. The two are separate declarations, and Boogie treats them very differently: a procedure is a contract that is trusted at every call site, while an implementation is the only thing that is ever verified.

Verification is entirely modular. Boogie checks each implementation against the specification of its own procedure, and checks nothing else. A procedure without an implementation is trusted outright. A procedure with several implementations has each of them checked independently against the same specification.

This chapter follows Section 8 of This is Boogie 2 (KRML 178, 2008), which remains an accurate account of the trace semantics. Where the tool has since changed — measure clauses, pure procedures, the disappearance of free modifies, the relaxed type-parameter rule — the difference is called out, and Divergences from This is Boogie 2 collects them.

6.1 Procedure declarations🔗

6.1.1 Grammar🔗

The productions below are quoted from Source/Core/BoogiePL.atg with the embedded C# semantic actions removed and the Coco/R attribute lists abbreviated; everything that affects the concrete syntax is reproduced exactly.

Procedure
= "procedure"
  ProcSignature<allowWhereClausesOnFormals = true>
  ( ";"
    { Spec }
  | { Spec }
    ImplBody
  )
  .

ProcSignature<allowWhereClausesOnFormals>
= { Attribute }
  Ident
  [ TypeParams ]
  ProcFormals<incoming = true,  allowWhereClausesOnFormals>
  [ "returns" ProcFormals<incoming = false, allowWhereClausesOnFormals> ]
  .

ProcFormals<incoming, allowWhereClauses>
= "(" [ AttributesIdsTypeWheres<allowWhereClauses> ] ")"
  .

TypeParams
= "<" Idents ">"
  .

A procedure declaration is introduced by the keyword procedure, optionally preceded by pure (see Pure procedures). At the top level the parser reads

  | Pure
    (
      Procedure
    | ActionDecl
    )

Pure
= [ "pure" ]
  .

so pure is a modifier shared by procedures and Civl atomic actions.

6.1.2 The two forms🔗

The semicolon after the signature is what distinguishes the two forms. With it, the declaration is specification-only; without it, the specification clauses must be followed by a body:

procedure Abs(x: int) returns (r: int);
  ensures 0 <= r;
  ensures r == x || r == -x;

implementation Abs(y: int) returns (res: int)
{
  if (y < 0) {
    res := -y;
  } else {
    res := y;
  }
}

procedure Abs(x: int) returns (r: int)
  ensures 0 <= r;
  ensures r == x || r == -x;
{
  if (x < 0) {
    r := -x;
  } else {
    r := x;
  }
}

Omitting the semicolon in a specification-only declaration produces a confusing parse error, because the parser then expects a body:

procedure P()
requires true;

semicolon.bpl(3,1): error: "{" expected
1 parse errors detected in semicolon.bpl

6.1.3 The combined form is a shorthand🔗

procedure P(ins) returns (outs) spec { body } is exactly equivalent to a procedure declaration plus a separate implementation whose formals are the procedure’s formals with the where clauses stripped. The attributes of the procedure are cloned onto the implementation. This is visible with /print:-:

procedure {:myattr} P(x: int where 0 < x) returns (r: int where 0 < r)
requires x < 10;
{
r := x;
}

boogie /noVerify /print:- shorthand.bpl

procedure {:myattr} P(x: int where 0 < x) returns (r: int where 0 < r);
requires x < 10;

implementation {:myattr} P(x: int) returns (r: int)
{
r := x;
}

6.1.4 Parameters🔗

In- and out-parameters are declared by AttributesIdsTypeWheres: a comma-separated list of ids : Type groups, each optionally preceded by its own attributes and optionally followed by a where clause (where clauses). If returns is omitted it defaults to returns ().

This is not the syntax of a local or global variable declaration. Those use IdsTypeWheres, which has no per-group attribute position: attributes are written once, immediately after the var keyword, and are attached to every variable of the declaration.

procedure P({:a} x: int, {:b} y: int); // fine: attributes per formal group

procedure Q()
{
var u: int, {:b} v: int; // error: no per-variable attributes here
}

paramattr.bpl(5,15): error: invalid Ident
1 parse errors detected in paramattr.bpl

All parameter names of one procedure must be distinct — in-parameters and out-parameters share one namespace — and a local variable of an implementation may not reuse a parameter name:

procedure P(x: int, x: bool);

dupformal.bpl(1,20): Error: more than one declaration of variable name: x
1 name resolution errors detected in dupformal.bpl

A local variable may shadow a global variable, however.

In-parameters are immutable inside the body. Assigning to one, or havocking one, is a type-checking error:

procedure P(x: int)
{
x := 3; // error: in-parameters are immutable
}

inparam.bpl(3,4): Error: command assigns to an immutable variable: x
1 type checking errors detected in inparam.bpl

Out-parameters are mutable and start out arbitrary: an implementation is not required to assign them.

6.1.5 Type parameters🔗

A procedure may be polymorphic. Type parameters are introduced in angle brackets after the name and may be used in the parameter types, the specification and the body.

procedure Id<T>(x: T) returns (r: T);
  ensures r == x;

procedure OutOnly<T>() returns (r: T);   // T occurs only in an out-parameter

implementation Id<U>(y: U) returns (s: U)   // type parameters may be renamed
{
  s := y;
}

procedure Client()
{
  var b: bool;
  var i: int;
  call b := Id(true);
  assert b;
  call i := OutOnly();
}

Boogie program verifier finished with 2 verified, 0 errors

Every type parameter must occur in the type of at least one in- or out-parameter. The paper requires occurrence among the in-parameters; the implementation (Type.CheckBoundVariableOccurrences, called with both parameter lists) accepts occurrence among the out-parameters as well, as OutOnly above shows. A type parameter occurring in neither is rejected:

procedure Unused<T>(x: int); // error: T occurs nowhere

poly.bpl(1,10): Error: type variable must occur in procedure arguments: T
1 name resolution errors detected in poly.bpl

6.1.6 Pure procedures🔗

pure procedure declares a procedure that is resolved in a state-less context: it may not mention any global variable in its specification or body, and may not have a modifies clause.

var g: int;

pure procedure Lemma(x: int) returns (r: int);
  ensures r == x + 1;

pure procedure BadPure();
  modifies g;              // error: pure procedures may not have a modifies clause

pure procedure AlsoBad();
  ensures g == 0;          // error: pure procedures may not mention globals

procedure Client()
{
  var y: int;
  call y := Lemma(1);
  assert y == 2;
}

pure.bpl(6,15): Error: unnecessary modifies clause for pure procedure
pure.bpl(10,10): Error: cannot refer to a global variable in this context: g
2 name resolution errors detected in pure.bpl

A pure procedure may only call other pure procedures. Pure procedures exist mainly to serve as lemmas in Civl developments, but they are ordinary Boogie declarations and work in plain programs. pure does not appear in the 2008 paper.

6.2 Implementation declarations🔗

Implementation
= "implementation"
  ProcSignature<allowWhereClausesOnFormals = false>
  ImplBody
  .

ImplBody
= "{" { LocalVars } StmtList
  .

LocalVars
= "var" { Attribute } IdsTypeWheres<allowWhereClauses = true> ";"
  .

Every implementation must name a procedure declared elsewhere in the program, and must repeat its signature, subject to these relaxations:

Parameter names may differ. Only the order and the types matter. Boogie maintains a substitution from the procedure’s formals to the implementation’s formals and applies it to every specification clause.
Type parameters may be renamed. They are matched positionally after SortTypeParams; the count must agree.
Grouping is insignificant. x, y: int and x: int, y: int declare the same formals.
where clauses must be omitted. They are inherited from the procedure declaration. Writing one is a parse error.

procedure P(x: int where x > 0);

implementation P(x: int where x > 0)
{
}

implwhere.bpl(3,35): error: where clause not allowed on the 'implementation' copies of formals
1 parse errors detected in implwhere.bpl

Attributes on the implementation’s formals are allowed.

Mismatches are reported during type checking:

procedure P(x: int) returns (r: bool);

implementation P(x: int, y: int) returns (r: bool)
{
r := true;
}

implementation P(x: bool) returns (r: bool)
{
r := x;
}

mismatch2.bpl(3,15): Error: mismatched number of in-parameters in procedure implementation: P
mismatch2.bpl(8,15): Error: mismatched type of in-parameter in implementation P: x
2 type checking errors detected in mismatch2.bpl

6.2.1 Multiple implementations🔗

A procedure may have any number of implementations, including zero, and including one supplied by the combined procedure ... { body } form plus further separate ones. Each is verified independently against the same specification; none of them may assume anything about the others.

procedure Max(a: int, b: int) returns (m: int);
  ensures m == a || m == b;
  ensures a <= m && b <= m;

implementation Max(a: int, b: int) returns (m: int)
{
  if (a < b) { m := b; } else { m := a; }
}

implementation Max(a: int, b: int) returns (m: int)
{
  m := a;             // error: this implementation is wrong
}

implementation {:verify false} Max(a: int, b: int) returns (m: int)
{
  m := b;             // not checked at all
}

multiimpl.bpl(13,1): Error: a postcondition could not be proved on this return path
multiimpl.bpl(3,3): Related location: this is the postcondition that could not be proved
Execution trace:
multiimpl.bpl(12,5): anon0

Boogie program verifier finished with 1 verified, 1 error

Note the counts: only implementations are counted as “verified”. A specification-only procedure contributes nothing to either number, and an implementation carrying {:verify false} is skipped entirely.

6.2.2 Local variables🔗

Local variables are declared at the top of the body, before the first statement. Their names must be distinct from each other and from the parameters (they may shadow a global), and they may carry attributes and where clauses. The attributes belong to the var keyword and are attached to every variable of that declaration. Boogie eliminates local variables that are not mentioned in the body (UnusedVarEliminator); see Unused locals lose their where clauses for the observable consequence.

6.3 Specification clauses🔗

Spec
= (
    SpecModifies
  | "free" SpecPrePost<free = true>
  | SpecPrePost<free = false>
  )
  .

SpecModifies
= "modifies" [ Idents ] ";"
  .

SpecPrePost<free>
= ( "requires" { Attribute } Proposition ";"
  | "ensures"  { Attribute } Proposition ";"
  | "measure"  { Attribute } Expressions ";"
  )
  .

Clauses may appear in any order and any number of times. The pretty-printer re-groups them as preconditions, then modifies, then postconditions, but the order within each group is preserved and is semantically significant (see Free specifications).

6.3.1 requires🔗

A precondition constrains the state in which the procedure may be called. It may mention constants, functions, global variables and in-parameters. It may not mention out-parameters, because they are not yet in scope when preconditions are resolved:

procedure P() returns (r: int);
requires r == 0;

reqout.bpl(2,11): Error: undeclared identifier: r
1 name resolution errors detected in reqout.bpl

It may not use old, because a precondition is resolved in a one-state context:

var g: int;

procedure P();
requires old(g) == g;

oldctx.bpl(4,11): Error: old expressions allowed only in two-state contexts
1 name resolution errors detected in oldctx.bpl

Preconditions must have type bool.

6.3.2 ensures🔗

A postcondition relates the entry and exit states. It may mention constants, functions, globals, in-parameters and out-parameters, and it is resolved in a two-state context so old(e) is available.

old applied to anything other than a global variable is the identity: the old-state map is built only from global variables, so old(x) for a parameter or local is just x.

var g: int;

procedure P(x: int) returns (r: int)
  modifies g;
  ensures old(x) == x;        // old of a parameter or local is the identity
  ensures old(r) == r;
  ensures old(g + 1) == old(g) + 1;
{
  g := 17;
  r := 3;
}

Boogie program verifier finished with 1 verified, 0 errors

old(g) is legal even when g is not in the modifies clause. At a call site the old-state substitution is built only from the callee’s modifies set, so old(g) for an unmodified g is just g.

6.3.3 modifies🔗

A modifies clause lists global variables that the procedure is permitted to change. It may only list global variables — constants are rejected — and the list may be empty (modifies ; parses).

const c: int;
procedure P();
modifies c;

modconst.bpl(2,10): Error: modifies list contains constant: c
1 type checking errors detected in modconst.bpl

The clause plays two quite different roles.

Inside the implementation it is enforced syntactically. Any command that assigns a global outside the frame is a type-checking error, and a call counts as assigning every global in the callee’s modifies clause. There is no proof obligation involved and no dependence on reachability:

var g: int;
var h: int;

procedure Callee();
  modifies g;

procedure Caller()
  modifies g;
{
  g := 1;      // fine: g is in the frame
  h := 2;      // error: h is not
  call Callee();
}

procedure Caller2();     // no modifies clause at all
implementation Caller2()
{
  call Callee();         // error: the call assigns g
}

modifies.bpl(11,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h
modifies.bpl(18,2): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g
2 type checking errors detected in modifies.bpl

At a call site it is a havoc list. Every global in the callee’s frame is assigned an arbitrary value, and only the postconditions say anything about the result. This happens whether or not the callee actually changes anything — declaring a modifies clause you do not use costs the caller real information:

var g: int;

procedure P()
  modifies g;
{
}

procedure Client()
  modifies g;
{
  call P();
  assert g == old(g);   // error: the frame is havocked regardless of what P does
}

modnoop.bpl(12,3): Error: this assertion could not be proved
Execution trace:
modnoop.bpl(11,3): anon0

Boogie program verifier finished with 1 verified, 1 error

Globals outside the callee’s frame are known to be unchanged:

var g: int;
var h: int;

procedure P()
  modifies g;
{
  g := g + 1;
}

procedure Client()
  modifies g, h;
{
  h := 0;
  call P();
  assert h == 0;      // h is outside P's frame, so it is unchanged
  assert g == old(g); // error: g may have changed
}

modframe.bpl(16,3): Error: this assertion could not be proved
Execution trace:
modframe.bpl(13,5): anon0

Boogie program verifier finished with 1 verified, 1 error

6.3.3.1 Inferring modifies clauses🔗

/inferModifies computes modifies clauses by a fixpoint over the call graph and, as a side effect, disables modifies checking altogether (TypecheckingContext.CheckModifies). It is switched on automatically for any program containing a Civl attribute.

var g: int;
var h: int;

procedure Callee()
{
  g := 1;
}

procedure Caller()
{
  call Callee();
  assert h == old(h);
  assert g == old(g);   // error: g was inferred into Callee's frame
}

boogie infermod.bpl

infermod.bpl(6,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g
1 type checking errors detected in infermod.bpl

boogie /inferModifies infermod.bpl

infermod.bpl(13,3): Error: this assertion could not be proved
Execution trace:
infermod.bpl(11,3): anon0

Boogie program verifier finished with 1 verified, 1 error

6.3.4 Free specifications🔗

Prefixing requires or ensures with free turns a checked clause into a trusted one. Precisely:

a free precondition is assumed by the implementation but imposes no obligation on callers;
a free postcondition is assumed by callers but imposes no obligation on the implementation.

That is the whole of it, and it is deliberately unsound: free clauses are the mechanism by which a front end relegates a property to a meta-level argument.

procedure P(x: int) returns (r: int)
  free requires 0 < x;
  free ensures r == x;
{
  assert 0 < x;    // holds: the implementation assumes free preconditions
  r := 0;          // the free postcondition is never checked
}

procedure Client()
{
  var y: int;
  call y := P(-1); // no obligation: the precondition is free
  assert y == -1;  // holds: the caller assumes the free postcondition
}

Boogie program verifier finished with 2 verified, 0 errors

Note the asymmetry in the other direction: a checked precondition is also assumed by the implementation (there is no reason for it not to be), and a checked postcondition is also assumed by the caller. So free only ever removes an obligation; it never adds an assumption. In particular a plain free postcondition is invisible to the implementation:

procedure P() returns (r: int)
free ensures r == 3;
{
assert r == 3; // error: a plain free ensures is not visible to the implementation
}

free modifies, which appears in the paper’s grammar, is not accepted:

var g: int;

procedure P();
free modifies g;

freemod.bpl(4,8): error: invalid SpecPrePost
1 parse errors detected in freemod.bpl

6.3.4.1 {:always_assume}🔗

The attribute {:always_assume} on a free clause adds back the assumption on the other side: on a free requires the caller assumes it too, and on a free ensures the implementation assumes it at the exit. It is ignored on non-free clauses.

procedure P() returns (r: int)
  free ensures r == 3;
{
  assert r == 3;    // error: a plain free ensures is not visible to the implementation
}

procedure Q() returns (r: int)
  free ensures {:always_assume} r == 3;
  ensures r == 3;   // holds: the preceding free ensures is assumed at the exit
{
}

procedure R() returns (r: int)
  ensures r == 3;                          // error: the {:always_assume} comes too late
  free ensures {:always_assume} r == 3;
{
}

alwaysassume.bpl(4,3): Error: this assertion could not be proved
Execution trace:
alwaysassume.bpl(4,3): anon0
alwaysassume.bpl(17,1): Error: a postcondition could not be proved on this return path
alwaysassume.bpl(14,3): Related location: this is the postcondition that could not be proved
Execution trace:
alwaysassume.bpl(17,1): anon0

Boogie program verifier finished with 1 verified, 2 errors

Q and R differ only in clause order. Postconditions are emitted into the unified exit block in declaration order, so an assumption introduced by a later clause cannot help an assertion emitted by an earlier one. The same ordering rule applies to preconditions at a call site:

procedure P();
  free requires 1 == 2;

procedure Q();
  free requires {:always_assume} 1 == 2;

procedure ClientP()
{
  call P();
  assert false;   // error: a plain free requires is skipped at the call site
}

procedure ClientQ()
{
  call Q();
  assert false;   // holds: {:always_assume} makes the caller assume it too
}

alwaysassume2.bpl(10,3): Error: this assertion could not be proved
Execution trace:
alwaysassume2.bpl(9,3): anon0

Boogie program verifier finished with 1 verified, 1 error

Because a failed assert is followed by an assumption of the asserted condition (default /subsumption:2), a checked precondition that is false at a call site masks every later precondition of the same call: only the first failure is reported.

procedure P(x: int);
  requires 0 < x;
  requires x < 0;

procedure Client()
{
  call P(0);   // only the first precondition is reported
}

preorder.bpl(7,3): Error: a precondition for this call could not be proved
preorder.bpl(2,3): Related location: this is the precondition that could not be proved
Execution trace:
preorder.bpl(7,3): anon0

Boogie program verifier finished with 0 verified, 1 error

6.3.5 measure clauses🔗

measure is a specification clause not described in the 2008 paper. It asks Boogie to prove termination of recursion. A sequential procedure may carry at most one measure clause, listing one or more expressions of type int or bool, compared lexicographically.

The transformation (Source/Core/MeasureChecker.cs) is:

each int-typed measure expression m adds a checked requires 0 <= m to the procedure;
before every recursive call (a call that closes a cycle in the transitive call graph), an assertion is inserted saying that the callee’s measure tuple, instantiated with the actual arguments, is lexicographically smaller than old of the caller’s measure tuple. For int components “smaller” is <; for bool components it is !m’ && m.

procedure Countdown(n: int)
  measure n;
{
  if (0 < n) {
    call Countdown(n - 1);
  }
}

procedure Bad(n: int)
  measure n;
{
  call Bad(n + 1);   // error: the measure does not decrease
}

measure1.bpl(12,3): Error: measure could not be proved to decrease
Execution trace:
measure1.bpl(12,3): anon0

Boogie program verifier finished with 1 verified, 1 error

The implicit non-negativity precondition is a real obligation at every call site, with its own error description:

procedure Countdown(n: int)
  measure n;
{
  if (0 < n) {
    call Countdown(n - 1);
  }
}

procedure Client()
{
  call Countdown(-1);   // error: an int measure gets an implicit "requires 0 <= n"
}

measure2.bpl(11,3): Error: a precondition for this call could not be proved
measure2.bpl(2,11): Related location: this measure could not be proved to be non-negative
Execution trace:
measure2.bpl(11,3): anon0

Boogie program verifier finished with 1 verified, 1 error

A lexicographic measure with mutual recursion:

procedure A(m: int, n: int)
  measure m, n;
{
  if (0 < n) { call A(m, n - 1); }
  else if (0 < m) { call A(m - 1, 100); }
}

Boogie program verifier finished with 1 verified, 0 errors

Mutually recursive procedures must agree on the number of measure expressions (“Expected number of measure expressions on callee and caller to be same”). More than one measure clause on a sequential procedure is an error:

procedure P(n: int)
measure n;
measure n;
{
}

measure3.bpl(3,2): Error: Sequential procedure may contain at most one measure command
1 type checking errors detected in measure3.bpl

Yielding procedures use per-layer measures and may carry several clauses; a measure command may also appear at a loop head; see measure for the loop form and Civl: concurrency and refinement for the per-layer form.

6.4 The caller/callee obligation split🔗

A procedure defines two sets of traces: the caller traces, which govern what a call does, and the callee traces, which govern what an implementation must satisfy. If a program uses no free clauses and no where clauses, the two coincide. Otherwise they differ, and the differences are exactly the trusted parts of the specification.

6.4.1 What the callee sees🔗

Boogie prepends a synthetic entry block to every implementation containing, in this order:

assume of the where clause of every global variable in the program (not merely those the procedure mentions);
assume of the where clauses of the procedure’s in-parameters, rewritten in the implementation’s parameter names;
assume of the where clauses of the procedure’s out-parameters, likewise — so an out-parameter’s where clause constrains its arbitrary initial value;
assume of the where clauses of the implementation’s local variables;
assume of every precondition, free and checked alike, in declaration order.

At the unified exit block it appends an assert for every checked postcondition, in declaration order, and an assume for every free postcondition carrying {:always_assume}. Plain free postconditions contribute nothing.

/traceverify shows the result:

var g: int where 0 <= g;

procedure P(x: int where 0 < x) returns (r: int where r == x)
  requires x < 10;
  free requires 0 < x;
  modifies g;
  ensures g == x;
  free ensures 0 <= r;
{
  var y: int where y == g;
  assert 0 <= y;
  g := x;
}

boogie /traceverify whereorder2.bpl

after inserting pre- and post-conditions
implementation P(x: int) returns (r: int where r == x)
{
  var y: int where y == g;

  PreconditionGeneratedEntry:
    assume 0 <= g;
    assume 0 < x;
    assume r == x;
    assume {:where y} y == g && true;
    assume x < 10;
    assume 0 < x;
    goto 0;

  0:
    goto anon0;

  anon0:
    assert 0 <= y;
    g := x;
    assert g == x;
    return;
}

6.4.2 What the caller sees🔗

A call is sugar for a block of primitive commands. /printDesugared prints it:

var g: int;

procedure P(x: int) returns (r: int where 0 < r);
  requires 0 < x;
  free requires x < 10;
  modifies g;
  ensures r == x + g;

procedure Client()
  modifies g;
{
  var y: int;
  call y := P(3);
}

boogie /noVerify /printDesugared /print:- desugar.bpl

implementation Client()
{
  var y: int;

    call y := P(3);
    /*** desugaring:
    {
      var call0formal#AT#x: int;
      var call1old#AT#g: int;
      var call2formal#AT#r: int where 0 < call2formal#AT#r;
      call0formal#AT#x := 3;
      assert 0 < call0formal#AT#x;
      call1old#AT#g := g;
      havoc g, call2formal#AT#r /* where 0 < call2formal#AT#r */;
      assume call2formal#AT#r == call0formal#AT#x + g;
      y := call2formal#AT#r;
    }
    **** end desugaring */
}

Reading it off: the actual arguments are copied into fresh temporaries; every checked precondition is asserted (free ones vanish unless they carry {:always_assume}); the pre-call values of the frame are saved for old; the frame and the out-parameter temporaries are havocked, which re-establishes any where clauses attached to them; every postcondition, free and checked alike, is assumed; and the out-parameter temporaries are copied to the actual out variables.

free call suppresses the precondition assertions for one call site while still assuming the postconditions. It is not in the 2008 paper.

procedure P(x: int) returns (r: int);
  requires 0 < x;
  ensures r == x;

procedure Client()
{
  var y: int;
  free call y := P(-1);   // preconditions are not checked
  assert y == -1;         // postconditions are still assumed
}

Boogie program verifier finished with 1 verified, 0 errors

6.4.3 Summary🔗

Clause	At a call site	In an implementation
requires P	assert P	assume P
free requires P	nothing	assume P
free requires {:always_assume} P	assume P	assume P
ensures Q	assume Q	assert Q at exit
free ensures Q	assume Q	nothing
free ensures {:always_assume} Q	assume Q	assume Q at exit
modifies g	havoc g	permission to assign g
measure m	assert 0 <= m as a precondition, plus a decrease check on recursive calls	assume 0 <= m
where	assumed for out-parameters and havocked globals, after the havoc	assumed on entry, and after every havoc

6.5 where clauses🔗

A where clause attaches a constraint to a variable rather than to a program point. It is best understood as a free assumption that Boogie re-inserts every time the variable acquires an unconstrained value.

/* AttributesIdsTypeWheres is used with the declarations of formals and bound variables */
AttributesIdsTypeWheres<allowWhereClauses>
= AttributesIdsTypeWhere<allowWhereClauses>
  { "," AttributesIdsTypeWhere<allowWhereClauses> }
  .

/* IdsTypeWheres is used with global and local variable declarations */
IdsTypeWheres<allowWhereClauses>
= IdsTypeWhere<allowWhereClauses>
  { "," IdsTypeWhere<allowWhereClauses> }
  .

AttributesIdsTypeWhere<allowWhereClauses>
= { Attribute } IdsTypeWhere<allowWhereClauses>
  .

IdsTypeWhere<allowWhereClauses>
= Idents ":" Type [ "where" Expression ]
  .

6.5.1 Where they may appear🔗

where is permitted on global variable declarations, on procedure formals (both in and out) and on local variables of an implementation. It is rejected everywhere else:

Position		Allowed?
global var declaration		yes
procedure formals (in and out)		yes
implementation formals		no — inherited from the procedure
local variables		yes
bound variables of a quantifier		no
constants		no
function parameters		no

The implementation and bound-variable cases produce a dedicated message. For implementation formals it is the one shown in Implementation declarations; for bound variables:

function f(x: int): bool;

axiom (forall y: int where 0 < y :: f(y)); // error: not allowed on bound variables

wherebound.bpl(3,32): error: where clause not allowed on bound variables
1 parse errors detected in wherebound.bpl

For constants and function parameters the grammar simply has no place for the keyword, so the diagnostic is a plain parse error (invalid Consts, ")" expected).

The Type and where clause of an IdsTypeWhere apply to each identifier declared, as if each had been written separately — the same expression is attached to every one of them, with no renaming. So x, y: int where 0 <= x gives y a clause that constrains x:

procedure P()
{
  var x, y: int where 0 <= x;
  x := -1;
  havoc y;          // y's clause is "0 <= x", so this re-constrains x
  assert 0 <= x;
}

boogie /noVerify /print:- sharedwhere.bpl

procedure P();

implementation P()
{
  var x: int where 0 <= x;
  var y: int where 0 <= x;

    x := -1;
    havoc y;
    assert 0 <= x;
}

boogie sharedwhere.bpl

Boogie program verifier finished with 1 verified, 0 errors

6.5.2 Scope and typing🔗

A where expression must have type bool. It is resolved in a one-state context, so it may not use old:

var g: int;

procedure P() returns (r: int where r == old(g));

oldwhere.bpl(3,41): Error: old expressions allowed only in two-state contexts
1 name resolution errors detected in oldwhere.bpl

The visible names depend on the position:

a global’s clause sees constants, functions and all global variables;
an in-parameter’s clause sees the above plus all in-parameters — not the out-parameters, which are registered later;
an out-parameter’s clause sees in- and out-parameters both;
a local’s clause sees globals, parameters and all locals.

Within each group, forward references are fine: all names of the group are registered before any where clause of the group is resolved.

procedure P(a: int where a < b, b: int) returns (r: int where r == a, s: int where s == r);

procedure Q()
{
  var u: int where u == v;
  var v: int where 0 <= v;
  assert u == v && 0 <= v;
}

Boogie program verifier finished with 1 verified, 0 errors

An in-parameter’s clause referring to an out-parameter is not:

procedure P(x: int where x < r) returns (r: int);

wherescope.bpl(1,29): Error: undeclared identifier: r
1 name resolution errors detected in wherescope.bpl

6.5.3 When a where clause is assumed🔗

This is the part that surprises people. A where clause is turned into an assume at exactly these points, and nowhere else.

On entry to an implementation. All four groups, in the order given in The caller/callee obligation split. Note in particular that the where clause of an out-parameter is assumed about its arbitrary initial value.

After a havoc. All the new incarnations are created first, and only then are the where clauses assumed. This makes a single multi-variable havoc order-insensitive, but a sequence of single-variable havocs order-sensitive:

procedure P()
{
  var x: int where 0 <= x;
  var y: int where x <= y;

  havoc y;
  havoc x;
  assert x <= y;    // error: y was re-constrained before x got its new value
}

procedure Q()
{
  var x: int where 0 <= x;
  var y: int where x <= y;

  havoc x;
  havoc y;
  assert x <= y;    // holds
}

procedure R()
{
  var x: int where 0 <= x;
  var y: int where x <= y;

  havoc y, x;       // one havoc: all incarnations first, then all where clauses
  assert x <= y;    // holds
}

wherehavoc.bpl(8,3): Error: this assertion could not be proved
Execution trace:
wherehavoc.bpl(6,3): anon0

Boogie program verifier finished with 2 verified, 1 error

At loop heads, for loop targets, because those are havocked there:

procedure P()
{
  var x: int where 0 <= x;
  var y: int;

  x := 5;
  y := 0;
  while (*)
  {
    x := x - 1;   // makes x a loop target
  }
  assert 0 <= x;  // holds: the where clause is re-assumed at the loop head
  assert y == 0;
}

Boogie program verifier finished with 1 verified, 0 errors

At a call site, for the temporaries holding the callee’s out-parameters and for the globals in the callee’s frame — both are havocked, so both pick up their clauses. The out-parameter clause is instantiated with the actual arguments, and any global it mentions is read in the post-state:

procedure P(x: int) returns (r: int where x < r);

procedure Client()
{
  var y: int;
  call y := P(5);
  assert 5 < y;      // holds: the where clause is instantiated with the actual argument
}

Boogie program verifier finished with 1 verified, 0 errors

var g: int;

procedure P() returns (r: int where r == g);
  modifies g;

procedure Client()
  modifies g;
{
  var y: int;
  call y := P();
  assert y == g;        // holds: g is read in the post-state
  assert y == old(g);   // error
}

whereglobalout.bpl(12,3): Error: this assertion could not be proved
Execution trace:
whereglobalout.bpl(10,3): anon0

Boogie program verifier finished with 0 verified, 1 error

A plain assignment does not re-impose a where clause. A global’s clause is therefore assumed at entry, re-assumed after any havoc and after any call whose frame contains it, and ignored in between:

var g: int where 0 < g;

procedure Q();
  modifies g;

procedure P()
  modifies g;
{
  assert 0 < g;    // assumed on entry to every implementation
  g := -1;
  assert g < 0;    // the where clause is not re-imposed by an assignment
  call Q();
  assert 0 < g;    // but it is re-assumed after the havoc of g caused by the call
  havoc g;
  assert 0 < g;    // and after an explicit havoc
}

Boogie program verifier finished with 1 verified, 0 errors

6.5.4 A where clause is never a proof obligation🔗

Nothing ever checks a where clause. In the paper’s terms, a where on an in-parameter behaves like a free precondition; a where on an out-parameter or on a modified global behaves like a free precondition and a free postcondition. Three consequences follow.

Callers need not establish an in-parameter’s clause, and the implementation gets to assume it anyway:

procedure P(x: int where 0 < x)
{
assert 0 < x; // assumed on entry
}

procedure Client()
{
call P(-1); // no proof obligation: where clauses are not checked at call sites
}

Boogie program verifier finished with 2 verified, 0 errors

Implementations need not establish an out-parameter’s clause, and callers assume it regardless. This program verifies completely, even though the caller’s conclusion is the exact negation of what the implementation returns:

procedure P() returns (r: int where 0 < r);

implementation P() returns (r: int)
{
  assert 0 < r;   // holds: the out-parameter's where clause is assumed on entry
  r := -1;        // and nothing requires it to hold on exit
}

procedure Client()
{
  var y: int;
  call y := P();
  assert 0 < y;   // holds anyway: the caller assumes the where clause after the call
}

Boogie program verifier finished with 2 verified, 0 errors

Globals’ clauses are simply believed, in every implementation, even one that never mentions the variable. A where clause on a global is the cheapest way to state a program-wide invariant, and also the cheapest way to make a whole program vacuous:

var unrelated: int where false; // never mentioned by P

procedure P()
{
assert false; // holds: every global's where clause is assumed on entry
}

Boogie program verifier finished with 1 verified, 0 errors

The clauses are inherited by the implementation under the parameter renaming, so none of this depends on using the same names:

procedure P(x: int where 0 < x) returns (r: int where r == x);

implementation P(a: int) returns (b: int)
{
assert 0 < a; // the procedure's where clauses are re-expressed in the
assert b == a; // implementation's parameter names
}

Boogie program verifier finished with 1 verified, 0 errors

Inside the implementation the clause also survives assignment-and-havoc of the out-parameter, because VC generation installs it on the implementation’s own copy of the formal:

procedure P() returns (r: int where 0 < r);

implementation P() returns (r: int)
{
  r := -1;
  havoc r;
  assert 0 < r;    // holds: the where clause is carried over to the implementation's copy
}

Boogie program verifier finished with 1 verified, 0 errors

6.5.5 Unused locals lose their where clauses🔗

Local variables not mentioned in the body are deleted before VC generation, and their where clauses go with them. A variable’s own where clause does not count as a mention. The effect is observable:

procedure Unused()
{
  var y: int where false;   // y is never mentioned
  assert false;             // error: the where clause of an unused local is dropped
}

procedure Used()
{
  var y: int where false;
  assert y == y;
  assert false;             // holds: the where clause is assumed
}

deadwhere.bpl(4,3): Error: this assertion could not be proved
Execution trace:
deadwhere.bpl(4,3): anon0

Boogie program verifier finished with 1 verified, 1 error

6.6 Inlining🔗

The attribute {:inline N} on a procedure or an implementation asks Boogie to replace calls to it by a copy of its body, up to depth N. N should be a non-negative integer literal. This section covers what inlining does to a procedure’s specification; the pass itself, the call-site form and the /inline option are in Inlining and Inlining and loops.

procedure {:inline 1} Inc(x: int) returns (r: int)
{
  r := x + 1;
}

procedure Client()
{
  var a: int;
  call a := Inc(41);
  assert a == 42;    // provable only because Inc's body was inlined
}

boogie inline1.bpl

Boogie program verifier finished with 1 verified, 0 errors

boogie /inline:none inline1.bpl

inline1.bpl(10,3): Error: this assertion could not be proved
Execution trace:
inline1.bpl(9,3): anon0

Boogie program verifier finished with 1 verified, 1 error

Two things are worth noticing in the first run. Inlining is on by default: the default strategy is /inline:assume. And the count says 1 verified, not 2: under /inline:assume and /inline:assert a procedure carrying {:inline N} is not verified at all (Implementation.IsSkipVerification).

{:inline N} may also be written on an implementation, which is how you inline one particular implementation of a procedure:

procedure Inc(x: int) returns (r: int);   // no postcondition at all

implementation {:inline 1} Inc(x: int) returns (r: int)
{
  r := x + 1;
}

procedure Client()
{
  var a: int;
  call a := Inc(41);
  assert a == 42;   // provable only because the implementation was inlined
}

Boogie program verifier finished with 1 verified, 0 errors

6.6.1 What happens at the cut-off🔗

/inline:i chooses what to do with a call once the depth is exhausted:

Option	Effect at the cut-off	Callee verified?
/inline:assume	replace the call by assume false	no
/inline:assert	replace the call by assert false	no
/inline:spec	leave the call as a call	yes
/inline:none	ignore {:inline} entirely	yes

The default is assume, which makes bounded inlining unsound for recursion — everything beyond the bound is silently assumed unreachable:

procedure {:inline 2} Down(n: int) returns (r: int)
{
  if (n <= 0) { r := 0; } else { call r := Down(n - 1); r := r + 1; }
}

procedure Client()
{
  var a: int;
  call a := Down(1);
  assert a == 1;      // reachable within the inlining depth
}

procedure Client2()
{
  var a: int;
  call a := Down(5);
  assert false;       // holds vacuously: /inline:assume cuts the recursion with assume false
}

boogie inlinerec.bpl

Boogie program verifier finished with 2 verified, 0 errors

boogie /inline:assert inlinerec.bpl

inlinerec.bpl(3,34): Error: this assertion could not be proved
Execution trace:
    inlinerec.bpl(16,3): anon0
    inlinerec.bpl(3,34): inline$Down$0$anon3_Else
    inlinerec.bpl(1,23): inline$Down$1$Entry
    inlinerec.bpl(3,34): inline$Down$1$anon3_Else

Boogie program verifier finished with 1 verified, 1 error

boogie /inline:spec inlinerec.bpl

inlinerec.bpl(17,3): Error: this assertion could not be proved
Execution trace:
    inlinerec.bpl(16,3): anon0
    inlinerec.bpl(3,34): inline$Down$0$anon3_Else
    inlinerec.bpl(1,23): inline$Down$1$Entry
    inlinerec.bpl(3,34): inline$Down$1$anon3_Else
    inlinerec.bpl(3,34): inline$Down$0$anon3_Else$1
    inlinerec.bpl(16,3): anon0$1

Boogie program verifier finished with 2 verified, 1 error

6.6.2 What inlining does to the specification🔗

Inlining does not discard the callee’s specification — it moves it into the caller. Inliner.CreateInlinedBlocks emits, around the copied body:

assignments of the actual arguments to the copied in-parameters;
an assert for each checked precondition (free preconditions become assert true);
a havoc of the copied locals and out-parameters;
saved copies of the modifies frame for old;
the copied body;
an assert for each checked postcondition (free postconditions become assume true; an ensures carrying {:InlineAssume} becomes an assume, whether it is free or not — the attribute is tested first);
assignments of the copied out-parameters to the call’s actual out variables.

So a postcondition of an inlined procedure becomes a proof obligation in the caller:

procedure {:inline 1} Inc(x: int) returns (r: int)
  requires 0 <= x;
  ensures r == x + 2;
{
  r := x + 1;
}

procedure Client()
{
  var a: int;
  call a := Inc(1);   // the ensures is asserted here, against the inlined body
  assert a == 2;
}

(0,0): Error: a postcondition could not be proved on this return path
inlinespec2.bpl(3,3): Related location: this is the postcondition that could not be proved
Execution trace:
    inlinespec2.bpl(11,3): anon0
    inlinespec2.bpl(1,23): inline$Inc$0$Entry
    inlinespec2.bpl(5,5): inline$Inc$0$anon0
    inlinespec2.bpl(1,23): inline$Inc$0$Return

Boogie program verifier finished with 0 verified, 1 error

/printInlined shows the expansion:

procedure {:inline 1} Inc(x: int) returns (r: int)
{
  r := x + 1;
}

procedure Client()
{
  var a: int;
  call a := Inc(41);
  assert a == 42;
}

boogie /printInlined printinlined.bpl

after inlining procedure calls
procedure Client();

implementation Client()
{
  var a: int;
  var inline$Inc$0$x: int;
  var inline$Inc$0$r: int;

  anon0:
    goto inline$Inc$0$Entry;

  inline$Inc$0$Entry:
    inline$Inc$0$x := 41;
    havoc inline$Inc$0$r;
    goto inline$Inc$0$anon0;

  inline$Inc$0$anon0:
    inline$Inc$0$r := inline$Inc$0$x + 1;
    goto inline$Inc$0$Return;

  inline$Inc$0$Return:
    a := inline$Inc$0$r;
    goto anon0$1;

  anon0$1:
    assert a == 42;
    return;
}

6.7 Recursion and termination🔗

Boogie proves partial correctness. Recursion is allowed and needs no annotation: a call to a procedure is checked against that procedure’s specification, including a self-call. Consequently a non-terminating procedure can “prove” anything about its exit state:

procedure Loop(n: int)
ensures false; // "proved" because Loop is verified against its own specification
{
call Loop(n);
}

Boogie program verifier finished with 1 verified, 0 errors

Use a measure clause (measure clauses) when termination matters, or {:inline N} with /inline:assert when you want the bound itself to be checked.

6.8 Attributes and options that affect procedures🔗

Name		Effect
{:verify false}		Skip verification of the implementation. Written on the procedure it applies to all of its implementations. The specification is still trusted by callers.
{:inline N}		Inline calls up to depth N; see Inlining.
{:msg "..."}		Replace the diagnostic for a requires or ensures. The replacement text is printed instead of the location prefix, so the source position is lost.
{:priority N}		Order in which implementations are verified.
{:timeLimit N}, {:vcs_max_cost N}, ...		Per-implementation versions of the corresponding options.
/proc:P		Verify only implementations whose name matches P.
/noProc:P		Skip implementations whose name matches P.
/inferModifies		Infer modifies clauses; disables modifies checking.
/printDesugared		Print the desugaring of call commands.
/printInlined		Print implementations after inlining.

procedure {:verify false} P() returns (r: int)
  ensures r == 1;
{
  r := 2;
}

procedure Q() returns (r: int)
  ensures r == 1;
{
  r := 2;
}

procedure Client()
{
  var a: int;
  call a := P();
  assert a == 1;   // the (unchecked) postcondition is still assumed by callers
}

verifyfalse.bpl(11,1): Error: a postcondition could not be proved on this return path
verifyfalse.bpl(8,3): Related location: this is the postcondition that could not be proved
Execution trace:
verifyfalse.bpl(10,5): anon0

Boogie program verifier finished with 1 verified, 1 error

boogie /proc:Client verifyfalse.bpl

Boogie program verifier finished with 1 verified, 0 errors

6.9 Divergences from This is Boogie 2🔗

Section 8 of the paper is still an accurate description of the trace semantics. The syntax and the specification vocabulary have moved on.

free modifies is gone. The paper’s Spec production has free? modifies; the grammar attaches free only to SpecPrePost, so free modifies g; is a parse error. Correspondingly the paper’s clause “free modifies clauses are ignored; that is, B8 considers only checked modifies clauses” has no counterpart in the tool: all modifies clauses are checked.
measure is new. A fourth kind of specification clause, checking that recursion terminates. See measure clauses.
pure procedure is new. See Pure procedures.
{:always_assume} is new. It gives back, per clause, the assumption that free removed on the other side of the split.
free call is new, as are async call and parallel call a() | b(). Both of the latter are Civl constructs: async call is rejected outside a yield procedure or an action (“async call allowed only from a yield procedure or an action”), and a parallel call requires both the caller and every target to be yielding.
call forall and wildcard actuals are gone. The paper’s Stmt grammar has call forall Id ( WildcardExpr ,*) and WildcardExpr ::= Expr | *. Neither survives in BoogiePL.atg; both are parse errors today. (The CallCmd desugaring still contains the code for wildcard actuals, but nothing produces them.)
The type-parameter rule is weaker. The paper requires every type parameter to occur among the in-parameter types; Boogie accepts occurrence among the out-parameter types as well.
Attributes on formals. The paper’s IdsTypeWhere has no attribute position; the grammar allows {:attr} x: int on every procedure and implementation formal and on bound variables. In the other direction, the paper’s Spec production allows attributes on a modifies clause (free? modifies Attribute* Id,* ;) and SpecModifies does not: modifies {:attr} g; is a parse error.
where clauses on in-parameters see less. The paper says the expression of a where clause among the parameters “can refer to any constant, function, global variable, and in- and out-parameter”. Boogie resolves the in-parameters’ clauses before registering the out-parameters, so an in-parameter’s clause that mentions an out-parameter is an undeclared-identifier error (where clauses).
New declaration forms share this grammar. yield procedure, action, yield invariant and their preserves / refines clauses are Civl extensions and are described in Civl: concurrency and refinement. preserves is not accepted on a plain procedure.

contents ← prev up next →

1	Introduction
2	Lexical structure
3	Types
4	Expressions and operators
5	Top-level declarations
6	Procedures, implementations and specifications
7	Statements and control flow
8	Bitvectors, floating point and rounding modes
9	Strings and regular expressions
10	Algebraic datatypes
11	The standard library
12	Attributes
13	Civl: concurrency and refinement
14	Advanced topics and tool internals
15	Command-line reference

6.1	Procedure declarations
6.2	Implementation declarations
6.3	Specification clauses
6.4	The caller/ callee obligation split
6.5	where clauses
6.6	Inlining
6.7	Recursion and termination
6.8	Attributes and options that affect procedures
6.9	Divergences from This is Boogie 2