should postconditions be evaluated even if Exception is thrown?

Steven Schveighoffer schveiguy at yahoo.com
Thu Dec 3 12:13:22 PST 2009


On Thu, 03 Dec 2009 13:47:25 -0500, Andrei Alexandrescu  
<SeeWebsiteForEmail at erdani.org> wrote:

> Don wrote:
>> Andrei Alexandrescu wrote:
>>> Michiel Helvensteijn wrote:
>>>> Andrei Alexandrescu wrote:
>>>>
>>>>> This may sound crazy, but if you just follow the facts that  
>>>>> distinguish
>>>>> regular error handling from program correctness, you must live with  
>>>>> the
>>>>> consequences. And the consequence is - a function's postcondition  
>>>>> must
>>>>> be designed to take into account exceptional paths. Only in case of
>>>>> unrecoverable errors is the function relieved of its duty.
>>>>
>>>> You don't want the regular postcondition to express exceptional  
>>>> outcomes.
>>>>
>>>> However, there *should* be an exception-postcondition clause, which
>>>> describes the conditions which are guaranteed to hold after an  
>>>> exception is
>>>> thrown.
>>>>
>>>> int f() throws (SomeException, SomeOtherException)
>>>> pre { }
>>>> body { }
>>>> post(int result) { }
>>>> epost(SomeException x) { }
>>>> epost(SomeOtherException)x) { }
>>>>
>>>> I believe JML does something like this.
>>>>
>>>
>>> Yah, I was thinking of something along the same lines.
>>>
>>> Andrei
>>  Yup. It's checked exceptions.
>
> The way I was thinking of it is:
>
> int f()
> out(result) { }
> out(Exception e) { }
> body { }
>
> So you have a chance to assert what the world looks like in case you  
> plan on returning a result, and what the world looks like if an  
> exception is emerging from the function.
>
> So checked exceptions - this is not.

That looks fine to me as long as

out(Exception e)

is optional -- it should revert to the original behavior.

-Steve



More information about the Digitalmars-d mailing list