Design by Contract (DbC)

Showcases formal verification and defensive programming using built-in contract keywords. This example illustrates the 'require' (pre-conditions) and 'ensure' (post-conditions) syntax to define strict API boundaries, showcasing how to validate input parameters and output results at runtime to catch logic errors early and improve software reliability.

Source Code

<?pas
function Divide(a, b: Integer): Float;
require
  b <> 0 : 'Divisor cannot be zero';
  a >= 0 : 'Dividend must be non-negative';
begin
  Result := a / b;
ensure
  Result >= 0 : 'Result must be non-negative';
end;

// Valid call
PrintLn('10 / 2 = ' + Divide(10, 2).ToString);

// Contract violation examples
try
  Divide(10, 0); // Fails 'require b <> 0'
except
  on E: Exception do
    PrintLn('Contract violation: ' + E.Message);
end;

// Class invariant example
type
  TBankAccount = class
    FBalance: Float;
    
    procedure Withdraw(amount: Float);
    require
      amount > 0 : 'Amount must be positive';
      amount <= FBalance : 'Insufficient funds';
    begin
      FBalance := FBalance - amount;
    ensure
      FBalance >= 0 : 'Balance cannot go negative';
    end;
    
    constructor Create(initial: Float);
    require
      initial >= 0 : 'Initial balance cannot be negative';
    begin
      FBalance := initial;
    end;
  end;

var account := TBankAccount.Create(100);
account.Withdraw(30);
PrintLn('Balance after withdrawal: ' + account.FBalance.ToString);
?>

Result

10 / 2 = 5
Contract violation: Pre-condition failed in Divide [line: 6, column: 3], Divisor cannot be zero
Balance after withdrawal: 70

← Class Operators Enums & Sets →