Software Contracting:

Preconditions

Conditions that must be true when the statement(s)/method/procedure starts
If they fail, the caller is at fault

Postconditions

Conditions that hold when the statement(s)/method/procedure ends
If they fail, the method writer is at fault

Loop Invariants

A condition that is true at the beginning of a loop
Note: I was incorrect when I said it was true during the whole lifetime of the loop

Loop Variant

An expression (in many cases a variable) that decreases on each iteration of the loop; proves the loop will eventually end
for (i = 1; i < 100; i++) Invariant: 100 - i
for (i = 100; i >= 1; i--) Invariant: i

Often when writing contracts you end up rewriting your code. This is ok.

Ideally you should write your contracts and the code at separate times. Otherwise, any condition you forget in one will be forgotten in the other. Contracts aren't magic. They can be incomplete and/or suffer from errors in logic and syntax as well.

Languages Using Contracting:

(Not required reading.)

Contracting is more than comments:

Assert statements (or defensive programming) is the most basic way to implement contracting:

assert [boolean expression];

A full description of Java's assert is here. A shorter example follows:

// Add an array of numbers, where each number must be between 1 and 100

int AddArrayOfNumbers(int[] inArray) {

int arraySum = 0, oldVariantI = 0;

// Preconditions

assert inArray <> null; // The order of assertions matter

assert inArray.length > 0;

for (int i = 0; i < inArray.length; i++)

{ assert inArray[i] > 0 && inArray[i] < 101; }

// Algorithm

oldVariantI = inArray.length; // Initialize the variant

for (int i = 0; i < inArray.length; i++) {

// Variant decreases

asssert (oldVariantI - 1) < OldVariantI;

// Invariant: inArray.length

arraySum = arraySum + inArray[i];

oldVariantI = oldVariantI - 1;

}

// Postconditions

assert arraySum >= inArray.length;

assert arraySum <= (inArray.length * 100);

// Finally, return the value

return arraySum;

}

In the above code, observe that:

The algorithm takes 8 lines, 2 of which are only a bracket, }
Pre, post, invariant and variant take 12 lines
There are two lines for comments - and neither comment is useful