www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - should postconditions be evaluated even if Exception is thrown?

reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
If a function throws a class inheriting Error but not Exception (i.e. an 
unrecoverable error), then the postcondition doesn't need to be satisfied.

I just realized that postconditions, however, must be satisfied if the 
function throws an Exception-derived object. There is no more return 
value, but the function must leave everything in a consistent state. For 
example, a function reading text from a file may have the postcondition 
that it closes the file, even though it may throw a malformed file 
exception.

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.


Andrei
Dec 02 2009
next sibling parent reply Walter Bright <newshound1 digitalmars.com> writes:
Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. an 
 unrecoverable error), then the postcondition doesn't need to be satisfied.
 
 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. For 
 example, a function reading text from a file may have the postcondition 
 that it closes the file, even though it may throw a malformed file 
 exception.
 
 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.

I have a hard time accepting this as a requirement. An exception means it failed, not succeeded.
Dec 02 2009
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Walter Bright wrote:
 Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. 
 an unrecoverable error), then the postcondition doesn't need to be 
 satisfied.

 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. 
 For example, a function reading text from a file may have the 
 postcondition that it closes the file, even though it may throw a 
 malformed file exception.

 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.

I have a hard time accepting this as a requirement. An exception means it failed, not succeeded.

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. Andrei
Dec 02 2009
parent reply Walter Bright <newshound1 digitalmars.com> writes:
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.
Dec 02 2009
next sibling parent reply Walter Bright <newshound1 digitalmars.com> writes:
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.

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?
Dec 02 2009
next sibling parent Michel Fortin <michel.fortin michelf.com> writes:
On 2009-12-03 01:06:07 -0500, Walter Bright <newshound1 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.

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 michelf.com http://michelf.com/
Dec 03 2009
prev sibling next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Walter Bright wrote:
 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.

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?

Very, very interesting example that actually makes my point very nicely. If the function doesn't throw, the postcondition is that the array is sorted. If the function does throw, the postcondition is that the array has not lost any element. So at least you know that information wasn't lost. I can't believe this is working so well in my argument :o). Andrei
Dec 03 2009
parent reply Don <nospam nospam.com> writes:
Andrei Alexandrescu wrote:
 Walter Bright wrote:
 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.

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?

Very, very interesting example that actually makes my point very nicely. If the function doesn't throw, the postcondition is that the array is sorted. If the function does throw, the postcondition is that the array has not lost any element. So at least you know that information wasn't lost. I can't believe this is working so well in my argument :o).

I don't understand why you think that. I can't believe it adds any value whatsoever. It's just like checked exceptions, but with a much, much higher burden.
Dec 03 2009
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Don wrote:
 Andrei Alexandrescu wrote:
 Walter Bright wrote:
 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.

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?

Very, very interesting example that actually makes my point very nicely. If the function doesn't throw, the postcondition is that the array is sorted. If the function does throw, the postcondition is that the array has not lost any element. So at least you know that information wasn't lost. I can't believe this is working so well in my argument :o).

I don't understand why you think that. I can't believe it adds any value whatsoever. It's just like checked exceptions, but with a much, much higher burden.

Checked exceptions are a very different beast. With a checked exception you must repeat statically all of the possible exceptions emerging from the function. But that information is next to useless. All that code is interested in is the throws-or-not bit. Postconditions are different. They are checks on the outcome of functions. The bane of exceptions-based languages is that once an exception is thrown, there's no real guarantee of the state of the system. This is because functions are too often written only having the success case in mind and neglecting to think and document how the world remains in case an exception is thrown. In the particular case of array sorting, if you use swap() throughout against elements of the array, the postcondition is always respected. But if you temporarily alter the array (e.g. by moving some of its elements off to temporary storage), then the postcondition is weaker - you're not guaranteed to even have the data in place if your comparison operator throws. I think this is information that a client of sort would be interested in. Andrei
Dec 03 2009
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Walter Bright wrote:
 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.

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?

I found one more example. A function that transfers money from one account to another must provide a postcondition even in the case of failure: no matter what, upon exit, the sum of the monies in the accounts is preserved. The transfer itself may fail for any number of complex reasons (overdraft, limit of transfers per month reached, account has limited access etc.) but the transfer function must in all cases preserve the total sum of funds in the two involved accounts. Andrei
Dec 03 2009
parent reply Michel Fortin <michel.fortin michelf.com> writes:
On 2009-12-03 17:16:11 -0500, Andrei Alexandrescu 
<SeeWebsiteForEmail erdani.org> said:

 I found one more example.
 
 A function that transfers money from one account to another must 
 provide a postcondition even in the case of failure: no matter what, 
 upon exit, the sum of the monies in the accounts is preserved. The 
 transfer itself may fail for any number of complex reasons (overdraft, 
 limit of transfers per month reached, account has limited access etc.) 
 but the transfer function must in all cases preserve the total sum of 
 funds in the two involved accounts.

That's a good example. But make this multithreaded and you have to hold the lock or transaction across the function and its pre- and post-conditions. Where should we stop? -- Michel Fortin michel.fortin michelf.com http://michelf.com/
Dec 03 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Michel Fortin wrote:
 On 2009-12-03 17:16:11 -0500, Andrei Alexandrescu 
 <SeeWebsiteForEmail erdani.org> said:
 
 I found one more example.

 A function that transfers money from one account to another must 
 provide a postcondition even in the case of failure: no matter what, 
 upon exit, the sum of the monies in the accounts is preserved. The 
 transfer itself may fail for any number of complex reasons (overdraft, 
 limit of transfers per month reached, account has limited access etc.) 
 but the transfer function must in all cases preserve the total sum of 
 funds in the two involved accounts.

That's a good example. But make this multithreaded and you have to hold the lock or transaction across the function and its pre- and post-conditions. Where should we stop?

I'd think the pre- and postconditions msut be under the lock anyhow. Andrei
Dec 03 2009
parent Michel Fortin <michel.fortin michelf.com> writes:
On 2009-12-03 19:31:37 -0500, Andrei Alexandrescu 
<SeeWebsiteForEmail erdani.org> said:

 Michel Fortin wrote:
 On 2009-12-03 17:16:11 -0500, Andrei Alexandrescu 
 <SeeWebsiteForEmail erdani.org> said:
 
 I found one more example.
 
 A function that transfers money from one account to another must 
 provide a postcondition even in the case of failure: no matter what, 
 upon exit, the sum of the monies in the accounts is preserved. The 
 transfer itself may fail for any number of complex reasons (overdraft, 
 limit of transfers per month reached, account has limited access etc.) 
 but the transfer function must in all cases preserve the total sum of 
 funds in the two involved accounts.

That's a good example. But make this multithreaded and you have to hold the lock or transaction across the function and its pre- and post-conditions. Where should we stop?

I'd think the pre- and postconditions msut be under the lock anyhow.

That'll only work if the lock is acquired outside of the function call. If the lock is acquired inside the function, pre- and post-conditions cannot be under the lock, and thus cannot check that. I think this just show that you probably ought to have two functions: one acquiring the lock which calls the other one to do the actual processing, the later one can have the pre-/post-conditions. But you can't put a contract on the one acquiring the lock since the contract would be outside it. Well, you could avoid it if labeling the function with synchronized was sufficient, but for the case above you probably want two locks, or some sort of database transaction, which won't work with synchronized. -- Michel Fortin michel.fortin michelf.com http://michelf.com/
Dec 04 2009
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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.

I agree. But constructors and destructors are already special, so that doesn't count. A regular function's postcondition should specify how it leaves the world in case an exception is passing through it. string readAllText(File input) out { assert(!input.isOpen()); } body { .... } Andrei
Dec 03 2009
prev sibling next sibling parent Brad Roberts <braddr puremagic.com> writes:
Walter Bright wrote:
 Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e.
 an unrecoverable error), then the postcondition doesn't need to be
 satisfied.

 I just realized that postconditions, however, must be satisfied if the
 function throws an Exception-derived object. There is no more return
 value, but the function must leave everything in a consistent state.
 For example, a function reading text from a file may have the
 postcondition that it closes the file, even though it may throw a
 malformed file exception.

 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.

I have a hard time accepting this as a requirement. An exception means it failed, not succeeded.

I agree with Andrei on this one. If there's some part of the object that's allowed to be in a 'bad' state, then it shouldn't be part of the invariant nor checked in the out contract. But it _should_ be possible for someone to construct an object that is strongly consistent including in the face of exceptions and have the DbC aspects of D help enforce that. Later, Brad
Dec 02 2009
prev sibling parent reply Rory McGuire <rjmcguire gmail.com> writes:
Walter Bright <newshound1 digitalmars.com> wrote:
 
 Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. an 
 unrecoverable error), then the postcondition doesn't need to be satisfied.
 
 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. For 
 example, a function reading text from a file may have the postcondition 
 that it closes the file, even though it may throw a malformed file 
 exception.
 
 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.

I have a hard time accepting this as a requirement. An exception means it failed, not succeeded.

I would think that if a method in a class throws then at least the class' invariant should be run? does it?
Dec 02 2009
parent reply Walter Bright <newshound1 digitalmars.com> writes:
Rory McGuire wrote:
 I would think that if a method in a class throws then at least the class' 
 invariant should be run? does it?

No.
Dec 02 2009
next sibling parent reply Walter Bright <newshound1 digitalmars.com> writes:
Brad Roberts wrote:
 Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?


Do you consider that broken or correct?

Not sure.
Dec 03 2009
next sibling parent reply Don <nospam nospam.com> writes:
Walter Bright wrote:
 Brad Roberts wrote:
 Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?


Do you consider that broken or correct?

Not sure.

I think it has to. Otherwise, how can the caller restore the invariant? Note that once the invariant is invalid, it can't call any member functions! The only thing it could do is delete the object.
Dec 03 2009
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Don wrote:
 Walter Bright wrote:
 Brad Roberts wrote:
 Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?


Do you consider that broken or correct?

Not sure.

I think it has to. Otherwise, how can the caller restore the invariant? Note that once the invariant is invalid, it can't call any member functions! The only thing it could do is delete the object.

s/delete the object/terminate the program ASAP/ Andrei
Dec 03 2009
prev sibling next sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Walter Bright wrote:
 Brad Roberts wrote:
 Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?


Do you consider that broken or correct?

Not sure.

Think Boeing: an exception is a possible and expected error of a subsystem. For example, failure to connect with the tower on radio or failure of the radar or failure to connect to the GPS satellite. Would you expect that such failures make no guarantee about the integrity of the plane's controls? Andrei
Dec 03 2009
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Walter Bright wrote:
 Brad Roberts wrote:
 Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?


Do you consider that broken or correct?

Not sure.

TDPL says that in non-release mode, public methods have code instrumented like this: class C { void m() { __check_invariant(); scope(exit) __check_invariant(); ... body ... } } My understanding after a recent discussion to Walter focused on the topic is that in case a non-Exception Error is thrown, scope(exit) statements are not guaranteed to be executed, as aren't destructors of local objects and finally clauses. Andrei
Dec 03 2009
parent reply Don <nospam nospam.com> writes:
Andrei Alexandrescu wrote:
 Walter Bright wrote:
 Brad Roberts wrote:
 Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?


Do you consider that broken or correct?

Not sure.

TDPL says that in non-release mode, public methods have code instrumented like this: class C { void m() { __check_invariant(); scope(exit) __check_invariant(); ... body ... } } My understanding after a recent discussion to Walter focused on the topic is that in case a non-Exception Error is thrown, scope(exit) statements are not guaranteed to be executed, as aren't destructors of local objects and finally clauses. Andrei

There are worse problems than that... At present, scope(exit) isn't executed if it's preceded by a label (!). And if the scope consists of a single declaration, the compiler will ICE if there is a destructor. Deterministic destruction is still horribly broken.
Dec 03 2009
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Don wrote:
 Andrei Alexandrescu wrote:
 Walter Bright wrote:
 Brad Roberts wrote:
 Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?


Do you consider that broken or correct?

Not sure.

TDPL says that in non-release mode, public methods have code instrumented like this: class C { void m() { __check_invariant(); scope(exit) __check_invariant(); ... body ... } } My understanding after a recent discussion to Walter focused on the topic is that in case a non-Exception Error is thrown, scope(exit) statements are not guaranteed to be executed, as aren't destructors of local objects and finally clauses. Andrei

There are worse problems than that... At present, scope(exit) isn't executed if it's preceded by a label (!). And if the scope consists of a single declaration, the compiler will ICE if there is a destructor. Deterministic destruction is still horribly broken.

Ouch. Well, at least these are problems we all agree what the fix should be. Andrei
Dec 03 2009
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the 
 class' invariant should be run? does it?

No.

Well you must do as you preach. Throwing a non-Error exception does not absolve a method from preserving the class invariant. Again: throwing a subclass of Exception is part of the specification and can happen during the working of a system. Andrei
Dec 03 2009
prev sibling next sibling parent Brad Roberts <braddr puremagic.com> writes:
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.
Dec 02 2009
prev sibling next sibling parent reply Michiel Helvensteijn <m.helvensteijn.remove gmail.com> writes:
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. -- Michiel Helvensteijn
Dec 03 2009
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
Dec 03 2009
parent reply Don <nospam nospam.com> writes:
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.
Dec 03 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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. Andrei
Dec 03 2009
next sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Steven Schveighoffer wrote:
 On Thu, 03 Dec 2009 13:47:25 -0500, Andrei Alexandrescu 
 <SeeWebsiteForEmail 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


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

I agree. To entirely accommodate existing behavior, out without an argument should only be evaluated if an exception is not thrown. Andrei
Dec 03 2009
prev sibling parent reply Michal Minich <michal.minich gmail.com> writes:
Hello Andrei,

 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.
 
 Andrei
 

if the function which throws exception is pure, then there is no world invariant to hold on after function exits (only return value is to be checked on success). Is there reason to have out(Exception ex) {} postcondition for pure function, or it should be compile time error to specify one? Similarly, when function is nothrow or when is not marked pure but does not make any side effect either.
Dec 04 2009
next sibling parent reply Michel Fortin <michel.fortin michelf.com> writes:
On 2009-12-04 04:11:22 -0500, Michal Minich <michal.minich gmail.com> said:

 Hello Andrei,
 
 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.
 
 Andrei
 

if the function which throws exception is pure, then there is no world invariant to hold on after function exits (only return value is to be checked on success). Is there reason to have out(Exception ex) {} postcondition for pure function, or it should be compile time error to specify one?

Well you could still assert something about the exception: out (LoginException ex) { assert(ex.errorDescription != ""); } So, although I can't really find an example that looks useful, someone might and I don't think it should be disallowed.
 Similarly, when function is nothrow or when is not marked pure but does 
 not make any side effect either.

In a nothrow function it certainly does not make sense have contracts for exceptions since none can be thrown. The only reasonable thing you could do in one is this: out (Exception e) { assert(false); } But since the compiler can statically check that no exception can be thrown it's dead code anyway... unless someone cast a function that throws as nothrow. -- Michel Fortin michel.fortin michelf.com http://michelf.com/
Dec 04 2009
next sibling parent Michal Minich <michal.minich gmail.com> writes:
Hello Michel,

 if the function which throws exception is pure, then there is no
 world invariant to hold on after function exits (only return value is
 to be checked on success). Is there reason to have out(Exception ex)
 {} postcondition for pure function, or it should be compile time
 error to specify one?
 

out (LoginException ex) { assert(ex.errorDescription != ""); } So, although I can't really find an example that looks useful, someone might and I don't think it should be disallowed.

Yes, you could provide more specific error message (or maybe throw more specific exception), but I'm not sure how useful is this. I'm also not sure about how some specifics should work: currently, it is not allowed to throw Exception from postcondition, it is only possible to throw Error (assert). Should it be possible to throw Exception from error handling postcondition or not? If exception handling postcondition is empty (or does not throw any Error or Exception), should the exception throw in body be suppressed or not? If you throw in postcondition, what to do with Exception throw in body ?
 Similarly, when function is nothrow or when is not marked pure but
 does not make any side effect either.
 

for exceptions since none can be thrown. The only reasonable thing you could do in one is this: out (Exception e) { assert(false); } But since the compiler can statically check that no exception can be thrown it's dead code anyway... unless someone cast a function that throws as nothrow.

but function and it contracts are defined at compile time anyway. (Such nothrow cast could only badly affect callers of this function.)
Dec 04 2009
prev sibling next sibling parent reply Leandro Lucarella <llucax gmail.com> writes:
Michal Minich, el  4 de diciembre a las 13:13 me escribiste:
 Hello Michel,
 
if the function which throws exception is pure, then there is no
world invariant to hold on after function exits (only return value is
to be checked on success). Is there reason to have out(Exception ex)
{} postcondition for pure function, or it should be compile time
error to specify one?

out (LoginException ex) { assert(ex.errorDescription != ""); } So, although I can't really find an example that looks useful, someone might and I don't think it should be disallowed.

Yes, you could provide more specific error message (or maybe throw more specific exception), but I'm not sure how useful is this. I'm also not sure about how some specifics should work: currently, it is not allowed to throw Exception from postcondition, it is only possible to throw Error (assert). Should it be possible to throw Exception from error handling postcondition or not?

I don't think so, postconditions should not change the programs behavior, it's like asserts or any other DbC feature. You can compile the program without it, and it should work the same. I think postconditions should only be able to inspect (in a read-only manner) the exception; once the postcondition finished executing, the exception should be propagated as is.
 If exception handling postcondition is empty (or does not throw any
 Error or Exception), should the exception throw in body be
 suppressed or not?

No.
 If you throw in postcondition, what to do with Exception throw in body ?

You can't throw in postconditions. -- Leandro Lucarella (AKA luca) http://llucax.com.ar/ ---------------------------------------------------------------------- GPG Key: 5F5A8D05 (F8CD F9A7 BF00 5431 4145 104C 949E BFB6 5F5A 8D05) ---------------------------------------------------------------------- G: I don't want hope. Hope is killing me. My dream is to become hopeless. When you're hopeless you don't care. And when you care, that indifference makes you attractive. J: So, hopelessness is the key? G: It's my only hope. -- George Constanza & Jerry Seinfeld
Dec 04 2009
next sibling parent Michal Minich <michal.minich gmail.com> writes:
Hello Leandro,

 I think postconditions should only be able to inspect (in a read-only
 manner) the exception; once the postcondition finished executing, the
 exception should be propagated as is.
 

heating up the processor for no effect whatsoever?! Note also that it is possible, and desired, to use assert statement in conditions; this statement can throw Error (it is corner case of changing behavior of program, but we can consider that it is not changing anything, because it should end the program very fast anyway).
Dec 04 2009
prev sibling parent Leandro Lucarella <llucax gmail.com> writes:
Michal Minich, el  4 de diciembre a las 14:13 me escribiste:
 Hello Leandro,
 
I think postconditions should only be able to inspect (in a read-only
manner) the exception; once the postcondition finished executing, the
exception should be propagated as is.

heating up the processor for no effect whatsoever?! Note also that it is possible, and desired, to use assert statement in conditions; this statement can throw Error (it is corner case of changing behavior of program, but we can consider that it is not changing anything, because it should end the program very fast anyway).

Well, yes, failing a postcondition should be a non-recoverable Error, and that's an exception, you're right. But I don't think being able to throw any non-Error should be allowed. I think only asserts should be allowed (not throwing using throw), and assert should in post/pre-conditions should dump a core, no more, no less. -- Leandro Lucarella (AKA luca) http://llucax.com.ar/ ---------------------------------------------------------------------- GPG Key: 5F5A8D05 (F8CD F9A7 BF00 5431 4145 104C 949E BFB6 5F5A 8D05) ---------------------------------------------------------------------- Agitamos toda la zona de la paleta al horno, vemos que una luz nos atraviesa toda la zona intestinal... -- Sidharta Kiwi
Dec 04 2009
prev sibling next sibling parent "Denis Koroskin" <2korden gmail.com> writes:
On Fri, 04 Dec 2009 16:35:57 +0300, Leandro Lucarella <llucax gmail.com>  
wrote:

 Michal Minich, el  4 de diciembre a las 13:13 me escribiste:
 Hello Michel,

if the function which throws exception is pure, then there is no
world invariant to hold on after function exits (only return value is
to be checked on success). Is there reason to have out(Exception ex)
{} postcondition for pure function, or it should be compile time
error to specify one?

out (LoginException ex) { assert(ex.errorDescription != ""); } So, although I can't really find an example that looks useful, someone might and I don't think it should be disallowed.

Yes, you could provide more specific error message (or maybe throw more specific exception), but I'm not sure how useful is this. I'm also not sure about how some specifics should work: currently, it is not allowed to throw Exception from postcondition, it is only possible to throw Error (assert). Should it be possible to throw Exception from error handling postcondition or not?

I don't think so, postconditions should not change the programs behavior, it's like asserts or any other DbC feature. You can compile the program without it, and it should work the same. I think postconditions should only be able to inspect (in a read-only manner) the exception; once the postcondition finished executing, the exception should be propagated as is.
 If exception handling postcondition is empty (or does not throw any
 Error or Exception), should the exception throw in body be
 suppressed or not?

No.
 If you throw in postcondition, what to do with Exception throw in body ?

You can't throw in postconditions.

You can't throw in pre/postconditions, but it's a bug: http://d.puremagic.com/issues/show_bug.cgi?id=3388 http://d.puremagic.com/issues/show_bug.cgi?id=3400
Dec 04 2009
prev sibling parent "Denis Koroskin" <2korden gmail.com> writes:
On Fri, 04 Dec 2009 16:13:53 +0300, Michal Minich  
<michal.minich gmail.com> wrote:

 Hello Michel,

 if the function which throws exception is pure, then there is no
 world invariant to hold on after function exits (only return value is
 to be checked on success). Is there reason to have out(Exception ex)
 {} postcondition for pure function, or it should be compile time
 error to specify one?

out (LoginException ex) { assert(ex.errorDescription != ""); } So, although I can't really find an example that looks useful, someone might and I don't think it should be disallowed.

Yes, you could provide more specific error message (or maybe throw more specific exception), but I'm not sure how useful is this. I'm also not sure about how some specifics should work: currently, it is not allowed to throw Exception from postcondition, it is only possible to throw Error (assert). Should it be possible to throw Exception from error handling postcondition or not?

Yes (it's already allowed in DMD trunk).
 If exception handling postcondition is empty (or does not throw any  
 Error or Exception), should the exception throw in body be suppressed or  
 not? If you throw in postcondition, what to do with Exception throw in  
 body ?

I guess that's what exception chaining is for.
Dec 04 2009
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Michal Minich wrote:
 Hello Andrei,
 
 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.

 Andrei

if the function which throws exception is pure, then there is no world invariant to hold on after function exits (only return value is to be checked on success). Is there reason to have out(Exception ex) {} postcondition for pure function, or it should be compile time error to specify one?

Good point. Probably a pure function has no place to define an out(Exception) guarantee.
 Similarly, when function is nothrow or when is not marked pure but does 
 not make any side effect either.

Such functions may choose to simply omit the out(Exception) clause. Andrei
Dec 04 2009
prev sibling parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Thu, 03 Dec 2009 13:47:25 -0500, Andrei Alexandrescu  
<SeeWebsiteForEmail 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


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
Dec 03 2009
prev sibling next sibling parent Brad Roberts <braddr puremagic.com> writes:
Walter Bright wrote:
 Rory McGuire wrote:
 I would think that if a method in a class throws then at least the
 class' invariant should be run? does it?

No.

Do you consider that broken or correct?
Dec 03 2009
prev sibling next sibling parent reply Don <nospam nospam.com> writes:
Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. an 
 unrecoverable error), then the postcondition doesn't need to be satisfied.
 
 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. For 
 example, a function reading text from a file may have the postcondition 
 that it closes the file, even though it may throw a malformed file 
 exception.
 
 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.
 
 
 Andrei

If you mean that all class invariants must be satisfied regardless of exceptions, then I agree. But if you mean the function postcondition, I don't think that makes sense. If the file needs to be closed, that should be part of the File invariant.
Dec 03 2009
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Don wrote:
 Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. 
 an unrecoverable error), then the postcondition doesn't need to be 
 satisfied.

 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. 
 For example, a function reading text from a file may have the 
 postcondition that it closes the file, even though it may throw a 
 malformed file exception.

 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.


 Andrei

If you mean that all class invariants must be satisfied regardless of exceptions, then I agree. But if you mean the function postcondition, I don't think that makes sense. If the file needs to be closed, that should be part of the File invariant.

The file invariant can't be "the file is closed". A free function readAllText(File f) could say that the postcondition is that the file is closed, even though a UTF exception does get thrown. Andrei
Dec 03 2009
prev sibling next sibling parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. an
 unrecoverable error), then the postcondition doesn't need to be satisfied.

If an 'Error' is truly unrecoverable, then there's no point in treating it as an exception. Just dump the core and get out. The very existence of 'Error' suggests that recovery is possible, so the same rules should apply to 'Error' and 'Exception'.
 I just realized that postconditions, however, must be satisfied if the
 function throws an Exception-derived object. There is no more return
 value, but the function must leave everything in a consistent state. For
 example, a function reading text from a file may have the postcondition
 that it closes the file, even though it may throw a malformed file
 exception.

Throwing an exception usually indicates a failure to reach the normal postcondition, but functions often have another postcondition that applies when the function terminates from an exception. Common postconditions in the case of an exception include: - The object is in a undetermined but valid state. (The basic exception guarantee in C++ lingo.) - The function has no side effects, i.e. all objects are in the same state as they were before the function was called. (The strong exception guarantee.) -- Rainer Deyke - rainerd eldwood.com
Dec 03 2009
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. an
 unrecoverable error), then the postcondition doesn't need to be satisfied.

If an 'Error' is truly unrecoverable, then there's no point in treating it as an exception. Just dump the core and get out. The very existence of 'Error' suggests that recovery is possible, so the same rules should apply to 'Error' and 'Exception'.

Actually, it's not that bad. TDPL explains that in detail, but there are a number of guarantees given by the language even if you catch Error.
 I just realized that postconditions, however, must be satisfied if the
 function throws an Exception-derived object. There is no more return
 value, but the function must leave everything in a consistent state. For
 example, a function reading text from a file may have the postcondition
 that it closes the file, even though it may throw a malformed file
 exception.

Throwing an exception usually indicates a failure to reach the normal postcondition, but functions often have another postcondition that applies when the function terminates from an exception. Common postconditions in the case of an exception include: - The object is in a undetermined but valid state. (The basic exception guarantee in C++ lingo.) - The function has no side effects, i.e. all objects are in the same state as they were before the function was called. (The strong exception guarantee.)

Yah, something like that. Andrei
Dec 03 2009
prev sibling next sibling parent reply =?UTF-8?B?UGVsbGUgTcOlbnNzb24=?= <pelle.mansson gmail.com> writes:
Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. an 
 unrecoverable error), then the postcondition doesn't need to be satisfied.
 
 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. For 
 example, a function reading text from a file may have the postcondition 
 that it closes the file, even though it may throw a malformed file 
 exception.
 
 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.
 
 
 Andrei

value? Or at least partially? The output cannot be correct if an exception is thrown, so any assertion in the post condition concerning the output would fail by definition, right? I would say the invariant() is the correct part to run.
Dec 03 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Pelle Månsson wrote:
 Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. 
 an unrecoverable error), then the postcondition doesn't need to be 
 satisfied.

 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. 
 For example, a function reading text from a file may have the 
 postcondition that it closes the file, even though it may throw a 
 malformed file exception.

 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.


 Andrei

value? Or at least partially? The output cannot be correct if an exception is thrown, so any assertion in the post condition concerning the output would fail by definition, right? I would say the invariant() is the correct part to run.

As others have mentioned, you may have different postconditions depending on whether an exception was thrown or not. I think a major failure of exceptions as a language mechanism is that they gave the illusion that functions need not worry about what happens when an exception traverses them, and only need to focus on the success case. Andrei
Dec 03 2009
parent reply =?UTF-8?B?UGVsbGUgTcOlbnNzb24=?= <pelle.mansson gmail.com> writes:
Andrei Alexandrescu wrote:
 Pelle Månsson wrote:
 Andrei Alexandrescu wrote:
 If a function throws a class inheriting Error but not Exception (i.e. 
 an unrecoverable error), then the postcondition doesn't need to be 
 satisfied.

 I just realized that postconditions, however, must be satisfied if 
 the function throws an Exception-derived object. There is no more 
 return value, but the function must leave everything in a consistent 
 state. For example, a function reading text from a file may have the 
 postcondition that it closes the file, even though it may throw a 
 malformed file exception.

 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.


 Andrei

return value? Or at least partially? The output cannot be correct if an exception is thrown, so any assertion in the post condition concerning the output would fail by definition, right? I would say the invariant() is the correct part to run.

As others have mentioned, you may have different postconditions depending on whether an exception was thrown or not. I think a major failure of exceptions as a language mechanism is that they gave the illusion that functions need not worry about what happens when an exception traverses them, and only need to focus on the success case. Andrei

be there. Something to replace the finally.
Dec 03 2009
parent Brad Roberts <braddr bellevue.puremagic.com> writes:
On Thu, 3 Dec 2009, Pelle M?nsson wrote:

 Andrei Alexandrescu wrote:
 As others have mentioned, you may have different postconditions depending on
 whether an exception was thrown or not.
 
 I think a major failure of exceptions as a language mechanism is that they
 gave the illusion that functions need not worry about what happens when an
 exception traverses them, and only need to focus on the success case.
 
 
 Andrei

there. Something to replace the finally.

No, post conditions do NOT replace finally. Finally is body code, often cleanup functionality. Post-conditions are validation.. checking correctness. PC is specifically NOT about cleanup or any data modification.
Dec 03 2009
prev sibling next sibling parent reply "Denis Koroskin" <2korden gmail.com> writes:
On Thu, 03 Dec 2009 06:51:32 +0300, Andrei Alexandrescu  
<SeeWebsiteForEmail erdani.org> wrote:

 If a function throws a class inheriting Error but not Exception (i.e. an  
 unrecoverable error), then the postcondition doesn't need to be  
 satisfied.

 I just realized that postconditions, however, must be satisfied if the  
 function throws an Exception-derived object. There is no more return  
 value, but the function must leave everything in a consistent state. For  
 example, a function reading text from a file may have the postcondition  
 that it closes the file, even though it may throw a malformed file  
 exception.

 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.


 Andrei

I'm not sure about post-conditions, but invariants have to be called. Exception-safe programming is a must. Any function may fail, and in that happens, the function should leave an object it operates on in a correct state. With post-conditions, there is a pitfall: if function throws an exception, there is no return value, and nothing to verify. For example: float sqrt(float value) out (result) { assert(value * value == result); } body { assert(value >= 0); // might throw. What value the 'result' variable in a post-condition would store? return core.stdc.sqrt(value); } Reading your post for a second time, I think you are confusing post-condition with something else. How would you close a file in a post-condition (or an invariant)? I believe both should be relaxedPure/hasNoSideEffects. File closing should be done in a function body using scope (exit) mechanism.
Dec 03 2009
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Denis Koroskin wrote:
 On Thu, 03 Dec 2009 06:51:32 +0300, Andrei Alexandrescu 
 <SeeWebsiteForEmail erdani.org> wrote:
 
 If a function throws a class inheriting Error but not Exception (i.e. 
 an unrecoverable error), then the postcondition doesn't need to be 
 satisfied.

 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. 
 For example, a function reading text from a file may have the 
 postcondition that it closes the file, even though it may throw a 
 malformed file exception.

 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.


 Andrei

I'm not sure about post-conditions, but invariants have to be called. Exception-safe programming is a must. Any function may fail, and in that happens, the function should leave an object it operates on in a correct state. With post-conditions, there is a pitfall: if function throws an exception, there is no return value, and nothing to verify. For example: float sqrt(float value) out (result) { assert(value * value == result); } body { assert(value >= 0); // might throw. What value the 'result' variable in a post-condition would store? return core.stdc.sqrt(value); } Reading your post for a second time, I think you are confusing post-condition with something else. How would you close a file in a post-condition (or an invariant)? I believe both should be relaxedPure/hasNoSideEffects. File closing should be done in a function body using scope (exit) mechanism.

The language would need to allow you to write an out(result) postcondition and an out(Exception) postcondition. Andrei
Dec 03 2009
prev sibling parent Sean Kelly <sean invisibleduck.org> writes:
Andrei Alexandrescu Wrote:

 If a function throws a class inheriting Error but not Exception (i.e. an 
 unrecoverable error), then the postcondition doesn't need to be satisfied.
 
 I just realized that postconditions, however, must be satisfied if the 
 function throws an Exception-derived object. There is no more return 
 value, but the function must leave everything in a consistent state. For 
 example, a function reading text from a file may have the postcondition 
 that it closes the file, even though it may throw a malformed file 
 exception.
 
 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.

Postconditions serve two purposes in my mind: to verify that object details are in a valid state when this checking isn't possible or appropriate in an invariant, and to check that the return value is in range. It seems quite reasonable to want the object validation to occur, but impossible for return value checking to occur... unless a feature is added to test if an exception is in flight and then expect the user to call this in postconditions to see if they should omit return value checking. This seems like it may be too onerous of a requirement.
Dec 03 2009