On Sep 9, 6:07?am, "Daniel T." <danie...@earthlink.net> wrote:
Joshua Maurice <joshuamaur...@gmail.com> wrote:
"Daniel T." <danie...@earthlink.net> wrote:
Joshua Maurice <joshuamaur...@gmail.com> wrote:
"Daniel T." <danie...@earthlink.net> wrote:
"joe" <jc1...@att.net> wrote:
Daniel T. wrote:
As more of a matter of an educated guess, if you want more
maintainable code, then if you have an error condition which is
unlikely to be handled at the caller, and is instead likely to be
handled much farther up the call stack, then use an exception.
Here you are saying the same thing that Stroustrup and I are saying,
but using different words. If the library can solve the problem then
fine; if it can't then the calling code must ensure that the issue
never gets to the library, i.e., it's a precondition for calling the
library that the issue not exist. Now the only question is what
should the library code do if it happens to detect that the
precondition was not met? terminate the app, throw an exception, or
leave the behavior undefined. Clearly, throwing an exception is the
best choice.
Meh. That's an interesting way of putting it. It rubs me the wrong way
to say that operator new has a precondition that sufficient memory be
available. A precondition to me means something which the caller can
check for or code for.
That is a pretty standard conception, but I don't think it is supported
well in the literature. For example:
? ?Meaning of a correctness formula: {P} A {Q}
? ?"Any execution of A, starting in a state where P holds, will
? ?terminate in a state where Q holds." (Meyer)
In the above, the precondition is P, the postcondition is Q and the
action to be performed is A. As Meyer tells us, this is not a
programming construct, it is a mathematical notation, a conceptual
framework within which to discuss the correctness of programming
constructs. If we allow 'operator new' to have as part of its
postcondition "or throws bad_alloc()", then we cannot call such an
action failure. An implementation of 'operator new' that throws
bad_alloc 10% of the time, even if memory is available would be working
correctly if this were the case.
Stroustrup reminds us that "Unfortunately, the assertions we would like
to make are often at a higher level than the programming language allows
us to express conveniently and efficiently." Yes it is difficult, if not
impossible, to check for adequate memory before calling operator new,
but that does not eliminate the assertion as a candidate for a
precondition.
More generally, there are a class of things which can have their
preconditions met, but still fail. You don't like operator new, so how
about network calls? When I send a large chunk of data, it can confirm
at the front that the socket is still open, and every other
precondition possible. However, I can unplug the cord halfway through,
making the call fail. The network code can do nothing about it. That's
a postcondition violation, or you change its post conditions into the
drivel "may work, may not". The only sensible thing to do is return an
error code or throw an exception stating that it cannot fulfill its
post conditions.
I agree with your assessment above. Watering down the postcondition such
that code that does nothing can still be considered correct is not the
way to go. However, as I have shown above, the correctness formula
*requires* that the action must terminate with the postcondition true if
the precondition was met.
Remember, preconditions and postconditions are not just a correctness
criteria, they can also be used to determine who's at fault. If the
precondition is met, but the postcondition is not, then the action
itself is at fault. I think we can both agree that it would be wrong to
lay the blame on the writer of the network code for failing in the
situation you describe. If the precondition is not met, then something
outside the action is at fault, which we can agree is the case here.
I'm not sure if I'm agreeing. Your quote of Meyers says that
preconditions are restrictions on the state (of the universe) when the
action commences. In my example of the network cord being unplugged
halfway through, the preconditions are true when the call begins; the
network cord is plugged in. but the naive postcondition of "data is
sent" is false.
So, given your strict requirement that "Postconditions are met iff
code is correct and preconditions are met", then I think we have two
choices:
1- Redefine preconditions to include not just the state of the
universe at the time of entering the function, but to include the
state of the universe from the start of the function call to the end
of the function call, aka "The network must remain up for the duration
of the call."
2- Water down the postcondition to "maybe it sends it and returns a
'sent' error code (or exception), or maybe it doesn't send it and
returns an 'error' code (or exception)."
This is getting pretty pedantic. I want to conclude that the writer of
the network code is not at fault (and thus needs not be changed), the
writer of the code which calls the network code is not at fault (and
thus needs not be changed), and if the network cord is pulled, then
the network function call should return an error code or throw an
exception indicating that it could not and did not send all of the
data, which the caller should handle in an appropriate way. I'm not
sure I want to continue to argue over the definitions of pre and post
conditions and how we reach these conclusions, but these are the
conclusions which should be reached.
However, I think I'm getting where you're coming from. You want to be
able to prove the correctness of a program piecemeal. Each function
has preconditions, and if those preconditions are met then the
function should be guaranteed to succeed. I think it's a nice model
for some programs, but for other programs it is not. For the memory
subsystem, this depends on state outside the control of the program,
such as the current commit charge, whether overcommit is turned on,
etc. Same for the network. There are some parts of programs which
really don't fit that model which I think you're incorrectly
attempting to shoehorn into the model.