6.15 Annotated Iteration Statements

Larch/C++ allows one to add annotations to iteration statements for loop invariants and termination functions. The syntax, borrowed from RESOLVE [Edwards-etal94], is that one can write a sequence of loop invariants with the keyword maintaing and a sequence of termination functions with the keyword decreasing; these go before the iteration-statement.

annotated-iteration-statement ::= [ maintaining-seq ] [ decreasing-seq ] iteration-statement
maintaining-seq ::= maintaining-clause [ maintaining-clause ] ...
maintaining-clause ::= maintaining [ redundantly ] predicate
decreasing-seq ::= decreasing-clause [ decreasing-clause ] ...
decreasing-clause ::= decreasing [ redundantly ] predicate
iteration-statement ::= a C++ while, do, or for statement

The following (adapted from chapter 7 of [Dijkstra76]), shows an example that uses annotations to state an invariant and termination function for Euclid's algorithm. Note that this code also makes use of assertions as statements (see section 6.14 Behavior Programs). Also, in the assertions, note that the values of the formal parameters X and Y are refered to using the ^ notation; this is because in code, these formal parameters are objects, and could be assigned to.

// @(#)$Id: Euclid.C,v 1.2 1999/04/12 17:06:23 leavens Exp $
#include <stdlib.h>

//@ uses gcd(int for Int);

int Euclid(int X, int Y) throw()
{
  //@ requires X^ \neq 0 \/ Y^ \neq 0;
  int x = abs(X);
  int y = abs(Y);
  //@ assert x' == abs(X^) /\ y' == abs(Y^);
  //@ assert redundantly x' \neq 0 \/ x' \neq 0;

  //@ maintaining gcd(x', y') == gcd(X^, Y^)
  //@ decreasing abs(y' - x')
  while (x != y) {
    if (x > y) {
      x = x - y;
    } else {
      //@ assert y' > x';
      y = y - x;
    }
  }
  //@ assert x' == y';

  //@ ensures x' == gcd(X^,Y^);
  return x;
}

Go to the first, previous, next, last section, table of contents.