A post-condition is a guarantee that a piece of code (e.g. a method or function) gives about the state when the function is exited, such as the correctness of the return value, or the correctness of a wider state, such as the state of the class instance or even the whole program.
I would interpret a Post-Condition Exception
as the action of throwing an exception (either directly with throw
, or use of a guard Assert
), rather than just softly returning a failed return code, or a default value, which might not be checked by the caller.
A hard failure is critical in the checking of pre-conditions, post conditions and invariants, as a soft return (such as a magic value like false or 0 or -1) would need to be checked (and could be missed) by the caller and mask the real problem that the code is operating in an out-of-design state.
The following example hopefully illustrates a post condition using an exception. In my simplistic design of Square(x)
, provided that the contract on the input is valid (viz that the input number squared won't overflow), the function SHOULD guarantee that the result is a positive number. If the post condition check fails it means a flaw in my design / implementation which could have dire consequences (e.g. a scenario which wasn't thought of, or failure of a dependency, such as in the Math
library itself).
Example with exceptions:
public static double Square(double number)
{
// Pre condition
if (Math.Abs(number) > Math.Sqrt(double.MaxValue))
throw new InvalidArgumentException("Number too big - will overflow");
var result = number * number;
// Post condition
if (result < 0)
throw new Exception("Square(x) should always be positive!");
return result;
}
As per the comments, Code Contracts also allow post conditions to be specified via Contract.Ensures
. This has the benefit that pre, and post conditions are documented at the top of the method, and also avoids the need for the extra local variable, since the result can be 'checked' directly:
public static double Square(double number)
{
Contract.Requires(Math.Abs(number) < Math.Sqrt(double.MaxValue),
"Oops number will result in overflow");
Contract.Ensures(Contract.Result<double>() >= 0,
"Square should always be positive!");
return number * number;
}
Another advantage Code Contracts have over exception-based assertions is static checking- contracts can be verified just after compile-time.