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