Thursday 18 December 2008

Delphi Prism – Class Contracts

One of the new features of Delphi Prism, which you may not have heard about is native support for Class Contracts. Class Contracts are Delphi Prism’s implementation of design by contract.

The whole premise of Design by Contract is that components of a software system interact with each other on the basis of mutual obligations (a contract). Therefore a method of any class may :

  • Insist that any client calling the method must adhere to a certain pre-condition.
  • Guarantee a certain post-condition on exit.
  • or will commit to maintain a certain property (Invariants).

Pre-Conditions

A pre-condition frees the method from having to maintain any checking code as it can be certain that the pre-condition will be met. Delphi Prism implements pre-conditions using the require keyword.

method MyClass.ToString(const aIndex : Integer) : string;
require
aIndex >= 0;
begin
result := fStrings[aIndex];
end;


Pre-Conditions are evaluated before the method is executed.


Post-Conditions

A post-condition ensures that the client knows what to expect from the method after it has executed. Delphi Prism implements post-conditions using the keyword ensure.


method MyClass.ToString(const aIndex : Integer) : string;
require
aIndex >= 0;
begin
result := fStrings[aIndex];
ensure
result.Length > 0;
end;


The old scope prefix can be used in the ensure section for local variables and parameters,  and refers to the values as they were before the method executed.


method MyClass.Add(aValue : string);
require
aValue <> ‘’;
begin
fStrings.Add(aValue);
ensure
Count = old Count+1;
end;

The old construct is only supported for integers and value types of both parameters and local variables. The compiler saves the value before execution of the method.


Class Invariants

Class invariants ensure that certain properties or fields of an object comply with a fixed state. Class invariants may be either private or public. We need to be careful here, as the way these work may initially seem counter intuitive. Public invariants, are checked after every public method only. (Actually, after the ensure clause, if it exists), while private invariants, are checked after both public and private methods. Another point to make is that both public and private invariants have access to all fields of the class. The public and private scope modifiers only indicate on which methods the invariants will apply.



  TestClass = public class
private
fValue : Integer;
private invariants
fValue > 0;
public invariants
fValue > 35;
public
//public methods
end;

Since public fields can be accessed from outside the class, they cannot be used in invariants as there is no way to restrict what goes on outside of the class. Having said that, public fields are never advisable anyway, so it’s not that much of a restriction

If any of the contracts above are not upheld, an assertion is raised. Assertions are by default enabled for the debug configuration, and disabled for the release configuration.


The Future

So what could be added in future to make class contracts even more useful than they already are?


  • Pre and Post conditions for interfaces

ITest = interface
method Test(const aValue : Integer) : string; requires aValue >= 0 ensures result <> '';
end;

With this syntax, we not only specify what the implementation must look like, but we also specify how it must behave.


  • Exceptional Post-Conditions

The ability to specify what exceptions a method can/should raise.


method Test; raises System.OverflowException;

  • Frame Conditions

Frame conditions restricts what a method can modify. Sample syntax could look like

  method Test; modifies fValue; 

Conclusion

Class constructs are not one of those features that you cannot live without. You could happily go on writing code and never use them once. However, by adding class contracts to your code, you make it clearer what the class does, and how it does it. Class contracts remove some of the ambiguity and a lot of the guessing. Up until now, we have used method signatures to indicate how class users can go about using our classes. We have also had to document a lot of other information so the user knows what is expected of him/her, and what he/she can expect from the class. With class contracts, a lot of that documentation is now part of the class, and can be checked at run-time to ensure the application is doing what we intended it to do in the first place.

1 comment:

Anonymous said...

This is extremely interesting stuff. I'm a C# developer and I've been looking for and bloging about support for DbC in .Net, preferably in C#. Learning that there is a language for the CLR that in fact implement this feature is really exciting.

Thanks for a great post.