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-statementmaintaining-seq::=maintaining-clause[maintaining-clause] ...maintaining-clause::=`maintaining`

[`redundantly`

]predicatedecreasing-seq::=decreasing-clause[decreasing-clause] ...decreasing-clause::=`decreasing`

[`redundantly`

]predicateiteration-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.