<?pas
// Design by Contract Demo

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);
?>