should postconditions be evaluated even if Exception is thrown?

[Michel Fortin]

On 2009-12-03 01:06:07 -0500, Walter Bright <newshound1 at digitalmars.com> said:

> Brad Roberts wrote:
>> Walter Bright wrote:
>>> Andrei Alexandrescu wrote:
>>>> An exception (not an Error) is an expected and documented outcome of a
>>>> function. After having listened to those endless Boeing stories,
>>>> please listen to this one :o). Contract Programming covers the
>>>> correctness of a program, and exceptions are correct behavior. By your
>>>> very Boeing stories that I stoically endured, it seems like the
>>>> logical conclusion is that postconditions must be evaluated upon
>>>> exceptional return.
>>> Consider a constructor. It's postcondition is the class invariant is
>>> satisfied. If it throws, the object is not successfully constructed and
>>> the invariant does not hold.
>> 
>> If the constructor fails, the object never existed.  Nothing to 
>> validate is valid.
> 
> Right. And I can't see how you can validate the output of a function 
> that failed. Let's say your function sorts an array, and the post 
> condition is the array is sorted. So, what would the postcondition be 
> if it failed?
> 
>    out (result)
>    {
>      assert(failed || isSorted(result));
>    }
> 
> ? What's the point?

That's silly indeed. But this is not:

	char[] array;

	void func()
	out {
		// array is guarantied to be left intact upon failure.
		if (failed)
			assert(array == in.array);
		else
			assert(isSorted(array));
	}
	body {...}

-- 
Michel Fortin
michel.fortin at michelf.com
http://michelf.com/