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


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


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


 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?


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.


 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?


 
 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.


 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?


 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.


 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?


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 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
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?


 No.


 
 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?


 No.


 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?


 No.


 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?


 No.


 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?


 No.


 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?


 No.


 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?


 No.


 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 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
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 reply "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


  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
Dec 03 2009
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


  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


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
parent reply 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?
 


 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.


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.
 


 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.
 


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
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?


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.


 
 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 "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?


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.


 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 reply 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
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 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?


 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.


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


Isn't the post-condition mainly to assert the correctness of the 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.
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


 Isn't the post-condition mainly to assert the correctness of the 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
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


 Isn't the post-condition mainly to assert the correctness of the 
 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


In the case of special postconditions for exceptions, I agree it should 
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


 In the case of special postconditions for exceptions, I agree it should be
 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