Prism - Invariants, and pre/post conditions

I’ve been looking at Prism some more recently. I’m a bit annoyed with myself really because someone has been telling me to look at it for years but I wanted to concentrate on C#. Now that I am looking at

it I see things in there which I really like.

Recently I am looking at invariants, pre-conditions, and post-conditions. First let me show you the invariant support. An invariant is like a class constraint, it specifies a condition which must be true

but when must it be true?

type
  BankAccount = public class
  public
    property Balance : Decimal read write;
  public invariants
    Balance >= 0;
  end;

The invariant is enforced each time a public method exits. Actually it is enforced after the post-conditions of a public method exits but we don’t have any post conditions yet.

class method ConsoleApp.Main;
begin
  var account : BankAccount := new BankAccount();

  //The next line throws an assertion error
  account.Balance := -1;
end;

Property getters and setters are considered methods, so as long as you aren’t publically exposing a field (which you should never do) then you are protected. In the following example the setter for Balance is Private but it is set via a public constructor, so the assertion is checked when the public constructor exits.

type
  BankAccount = public class
  public
    constructor (OpeningBalance : Decimal);
    property Balance : Decimal read private write;
  public invariants
    Balance >= 0;
  end;
  
implementation


constructor BankAccount(OpeningBalance : Decimal);
begin
  Balance := OpeningBalance;
end;


class method ConsoleApp.Main;
begin
  var account : BankAccount := new BankAccount(-1);
end;

Obviously we can’t set a balance for an account directly because its setter is private, so let’s add another feature we could use instead. Next I will add a Withdraw method with overdraft facility.

type
  BankAccount = public class
  public
    constructor (OpeningBalance : Decimal);
    property Balance : Decimal read private write;

    method Withdraw(Amount : Decimal);
    property Overdraft : Decimal read write;
  public invariants
    Balance + Overdraft >= 0;
    Overdraft >= 0;
  end;
  
implementation


constructor BankAccount(OpeningBalance : Decimal);
begin
  Balance := OpeningBalance;
end;

method BankAccount.Withdraw(Amount : Decimal);
begin
  Balance := Balance - Amount;
end;

As you can see the invariants of this class are that the Overdraft must be >= 0 and the Balance plus the Overdraft must be >= 0. The following program illustrates use of this.

class method ConsoleApp.Main;
begin
  var account : BankAccount := new BankAccount(10);
  account.Overdraft := 10;
  account.Withdraw(20);

  //Outputs -10
  Console.WriteLine("Balance : " + account.Balance.ToString);

  //The next line throws an assertion error
  account.Withdraw(1);
end;

So that’s an invariant now let’s look at pre-conditions. The Withdraw method would currently accept an Amount of zero which obviously makes no sense, what’s worse though is that it could accept a negative number and actually increment the balance so let’s add a pre-condition to prevent this.

constructor BankAccount(OpeningBalance : Decimal);
require
  OpeningBalance >= 0;
begin
  Balance := OpeningBalance;
end;

method BankAccount.Withdraw(Amount : Decimal);
require
  Amount > 0;
begin
  Balance := Balance - Amount;
end;

Now if I try to create the bank account with a negative opening balance, or if I try to withdraw an amount of money that is not greater than zero I will experience an assertion. It’s possible also to add post-conditions by using the "ensure" keyword.

method BankAccount.Withdraw(Amount : Decimal);
require
  Amount > 0;
begin
  Balance := Balance - Amount;
ensure
  Balance = old Balance - Amount;
end;

Note here that I use "old Balance", which is the value that Balance was when the method was called. The combination of pre/post conditions say that "If you pass me a positive amount of money I will decrement the Balance by that exact amount".

I haven’t finished yet! The default behaviour is to use Debug.Assert whenever an invariant is broken, a pre-condition is not met, or a post-condition is not satisfied. It is possible to change this behaviour for a Release build so that your invariants are not only checked during debugging. This is particularly useful when you are persisting and retrieving objects’ state in a database, if another application bypasses your business classes and writes directly to the database your invariants ensure that your application fails immediately rather than working with an invalid state and possibly causing more invalid state elsewhere. To do this create a static class like so

type
  ClassContractChecker = public static class
  private
  protected
  public
    class method Check(IsValid : Boolean; ErrorMessage : String);
  end;
  
implementation

class method ClassContractChecker.Check(IsValid : Boolean; ErrorMessage : String);
begin
  if not IsValid then
    raise new Exception(’Unexpected class contract violation ’ + ErrorMessage);
end;

Then in the project’s properties look on the DEBUG tab and enter

  Assertion class name : MyNameSpace.ClassContractChecker
  Assertion method : Check

NOTE: This is a separate setting for each build configuration, so set it to RELEASE

Now instead of using Debug.Assert any time something goes wrong the Prism compiler will execute this static method so that we can throw an exception instead (currently this doesn’t work for RELEASE builds, I have reported it as a bug so hopefully it will be fixed).

This kind of programming allows us to identify errors in our objects’ states early on. Using this approach will cause an app to "fail hard" at the first sign of something unexpected happening. This may sound harsh at first but the app failing immediately and prominently is better than it being wrong for a long period of time and causing weird side effects in your logic which could end up with nonesense data - that would be a much worse situation.