Class Contracts

Introduction

Class contracts provide an additional means of testing code before putting it into production and also help to document the code. This RemObjects Oxygene language page and a blog give good explanations of class contracts as used in Oxygene. Necessary preconditions for a method follow the keyword require, and an ensure clause indicates postconditions that the method guarantees. (The old keyword conveniently accesses the value of a variable before it is changed by a method). Class invariants are required conditions that are checked after methods.

Precise error messages result when stated conditions are not met. In the debug version of the program below, this is the informative error message:

Error message

When you select the compilation option 'Release' instead of 'Debug', the contracts do not appear in the executable and the error message therefore does not appear. You can experiment with the Main method to test other error messages.

We tried the code of the class contracts demo for Oxygene for .Net, but could not obtain the array of the generic type T at runtime in Oxygene for Java. We modified the stack code to use an ArrayList instead of an array and wrote several versions of a Main method to test the error messages.

Code of ClassContractDemo.pas

namespace class_contract_demo;

interface

uses
  java.util;

type
  ConsoleApp = class
  public
    class method Main(args: array of String);
  end;

implementation

class method ConsoleApp.Main(args: array of String);
var
  ColourStack : Stack<String>;
  CurrentColour : String;
begin
  ColourStack := new Stack<String>(3);
  writeLn('Creating stack with capacity 3');
  ColourStack.PutItem('Red');
  writeLn('Pushing Red');
  ColourStack.PutItem('Orange');
  writeLn('Pushing Orange');
  ColourStack.PutItem('Yellow');
  writeLn('Pushing Yellow');
  CurrentColour := ColourStack.GetItem; 
  writeLn('Top of stack:');
  writeLn(CurrentColour);
  writeLn('Press any key to attempt to add Green to a full stack.');
  System.in.read;
  ColourStack.PutItem('Green');
  System.in.read;
end;

end.

Code of uStack.pas

namespace class_contract_demo;

interface
uses
  java.util;
type
  // An implementation of a generic stack. Based on the example in 
  // ch. 11 of Bertrand Meyer's "Object Oriented Software Construction" 2nd Ed
  // but using an ArrayList instead of an array.
  Stack<T> = public class 
  private
    fCount: Integer;
    fCapacity: Integer;
    representation: ArrayList<T>;
    
    method GetIsEmpty: Boolean;
    method GetIsFull: Boolean;
    method GetItem: T; 
  public
    constructor(capacity: Integer);    
    method PutItem(newItem: T);
    method RemoveItem;
      
    property Count: Integer read fCount;
    property Item: T read GetItem;
    property IsEmpty: Boolean read GetIsEmpty;
    property IsFull: Boolean read GetIsFull;
    
  public invariants 
    fCount >= 0;
    fCount <= fCapacity;
    IsEmpty = (fCount = 0);
    (fCount > 0) implies (representation[fCount - 1].equals(Item));
  end;

implementation

constructor Stack<T>(capacity: Integer);
require
  capacity >= 0;
begin
  fCount := 0;
  fCapacity := capacity;
  representation := new ArrayList<T>;
ensure
  fCapacity = capacity; 
  assigned(representation);
  IsEmpty;
end;

method Stack<T>.GetIsFull: Boolean;
begin
  result := (fCount = fCapacity); 
ensure
  // The imperative and the applicative 
  result = (fCount = fCapacity);  
end;

method Stack<T>.GetIsEmpty: Boolean;
begin
  result := (fCount = 0);
ensure
  result = (fCount = 0);  
end;

method Stack<T>.GetItem: T;
require
  not IsEmpty;
begin
  result := representation[fCount - 1];
end;

method Stack<T>.PutItem(newItem: T);
require
  not IsFull;
begin
  inc(fCount);
  representation.add(newItem);
ensure
  not IsEmpty;
  Item.equals(newItem);
  fCount = old fCount + 1;
end;

method Stack<T>.RemoveItem;
require
  not IsEmpty;
begin
  representation.remove(Count);
  dec(fCount);
ensure
  fCount = old fCount - 1;   
end;

end.