What is a post-condition exception?

Question

I'm doing some homework which has the question:

How would you a pre-condition exception?
How would you use a post-condition exception?

So for the first question, I assume a precondition is something that must be met in order for the function to run. E.g, an argument must not be null, we could throw an exception:

if (myArg == null)
    throw new ArgumentNullException("myArg");
//do work here

However, I can't figure out what a use for a post-condition exception would be, and indeed why we would want to throw an exception in this case (e.g. instead of returning false if a condition is not met).

Can anyone please provide an example for this?

Answer 1

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.

Answer 2

The other answer is correct and the comments are all useful in answering your question. I felt there is a little bit that could be added, so here is my contribution.

I had never heard it called "post-condition exceptions" either, but as to your question, "when are they used," they are used a lot in Unit Testing (See https://stackoverflow.com/tags/unit-testing/info or other resource like wikipedia for how-to). In the Unit Test, a testing programmer calls a function that she wants to test, and she also knows what value she expects from the function (that is, an answer known to be correct from other sources of knowledge). The post-condition test is: "do the expected value and the actual value returned from the function or method agree?"

Then the Assert Method throws an exception if they do not agree. The testing framework software catches the exception, then reports the given test as failed, and moves on to run other tests without halting on the failed test. Here is a toy example to illustrate.

[TestMethod]
public void Integers_7Add1_equals8()
{
   int expected = 8;
   int actual = MyClass.AddOne(7);
   Assert.AreEqual(expected, actual);
}

So the exception is thrown in the Assert.AreEqual method call, after calling the method being tested, thus it is a post-condition exception.