Discussion:
Design by contract and unit tests
(too old to reply)
Sasa
2006-02-12 09:23:38 UTC
Permalink
Hello,

I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.

Thanks,
Sasa
Daniel T.
2006-02-12 10:33:01 UTC
Permalink
Post by Sasa
Hello,
I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
The definition of a precondition is that the function will give
undefined results if the precondition is not met. How can you test
something that isn't supposed to work any particular way? IE I would say
no as well.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
Miguel Oliveira e Silva
2006-02-12 20:23:21 UTC
Permalink
Post by Daniel T.
Post by Sasa
Hello,
I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
The definition of a precondition is that the function will give
undefined results if the precondition is not met.
No.

If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)

When a precondition fails the responsibility does
not belong to the routine (probably that was what
you were trying say with the "undefined behavior"),
being instead the caller's fault.

In unit testing it does not makes sense to test
the unit with something that is not its
responsibility (it would be like test a car with
a blind "driver").
If the preconditions assertion is executable
(and not simply a comment), it is ensured
that such errors will always be cached.

DbC is very helpful for unit testing as it directs
tests to be restricted to the unit's Abstract Data Type
semantics. Unlike extreme programming approaches
of putting the unit's semantics externally in its
test sets, DbC puts them where they should be:
in the unit's public interface for everyone to
easily see, find, and reason about.
Post by Daniel T.
How can you test something that isn't supposed to work any particular way? IE I would say
no as well.
Agreed.
Post by Daniel T.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
-miguel

--
Miguel Oliveira e Silva
Phlip
2006-02-12 21:27:33 UTC
Permalink
Post by Miguel Oliveira e Silva
Post by Daniel T.
The definition of a precondition is that the function will give
undefined results if the precondition is not met.
No.
Yes. That's the meaning of "contract" in DBC.
Post by Miguel Oliveira e Silva
If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)
Such failures, regardless how they bubble up, are not normal control flow,
they are programming mistakes to be removed. A DBC program should be able to
run the same with all the checks compiled-out. Research the Ariane V
experience to see this effect in action!
--
Phlip
http://www.greencheese.org/ZeekLand <-- NOT a blog!!!
Miguel Oliveira e Silva
2006-02-13 14:53:41 UTC
Permalink
Post by Phlip
Post by Miguel Oliveira e Silva
Post by Daniel T.
The definition of a precondition is that the function will give
undefined results if the precondition is not met.
No.
Yes. That's the meaning of "contract" in DBC.
Its meaning is to state that the supplier (routine)
need not to worry on conditions outside its precondition
(the client need not also to worry about conditions
outside the routine's postcondition).
If the semantics of (runnable) assertions were not to
raise an exception, then you would be right in stating
that the routine would have an undefined behavior.
But that is not the case.
Post by Phlip
Post by Miguel Oliveira e Silva
If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)
Such failures, regardless how they bubble up, are not normal control flow,
they are programming mistakes to be removed.
Of course.
Post by Phlip
A DBC program should be able to
run the same with all the checks compiled-out.
Of course (if, and only if, the software is correct
considering its assertions).

I only disable assertions in my code if a really need
it (and only in loop intensive critical parts of a
program).
Post by Phlip
Research the Ariane V
experience to see this effect in action!
Ariane's software was not correct.
Post by Phlip
--
Phlip
http://www.greencheese.org/ZeekLand <-- NOT a blog!!!
-miguel

--
Miguel Oliveira e Silva
Phlip
2006-02-13 15:15:15 UTC
Permalink
Post by Miguel Oliveira e Silva
Its meaning is to state that the supplier (routine)
need not to worry on conditions outside its precondition
(the client need not also to worry about conditions
outside the routine's postcondition).
If the semantics of (runnable) assertions were not to
raise an exception, then you would be right in stating
that the routine would have an undefined behavior.
But that is not the case.
Research the Ada SPARKS system (including its threads here).

The point of DbC is not what happens at fault time. The point is to roll the
contracts up into a kind of proof that the entire program's contract is
well-defined.

At fault time, an exception might make a function's behavior technically
well-defined, at the language level. The entire program's contract is still
not well-defined.

(Otherwise, you would define in the program's contract that such-and-so
causes an exception, such and so catches it, and the exception itself has
invariants.)
--
Phlip
http://www.greencheese.org/ZeekLand <-- NOT a blog!!!
Dmitry A. Kazakov
2006-02-13 15:28:40 UTC
Permalink
Post by Phlip
The point of DbC is not what happens at fault time. The point is to roll the
contracts up into a kind of proof that the entire program's contract is
well-defined.
Right, there is a fundamental difference between bugs (contract violation
is a bug) and faults (an exceptional state.) A system can be designed
fault-tolerant, but it cannot be bug-tolerant.
Post by Phlip
At fault time, an exception might make a function's behavior technically
well-defined, at the language level. The entire program's contract is still
not well-defined.
(Otherwise, you would define in the program's contract that such-and-so
causes an exception, such and so catches it, and the exception itself has
invariants.)
To put it in other words: the "contract violation exception" is propagated
out of the software up to the software developing circle.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
S Perryman
2006-02-14 11:31:43 UTC
Permalink
Post by Phlip
Post by Miguel Oliveira e Silva
If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)
Such failures, regardless how they bubble up, are not normal control flow,
they are programming mistakes to be removed. A DBC program should be able
to run the same with all the checks compiled-out. Research the Ariane V
experience to see this effect in action!
Please feel free to explain :

1. how a " DBC program should be able to run the same with all the checks
compiled-out" relates to the Ariane V failure.

2. What the behaviour of the Ariane V s/w was, when the DBC checks were
'compiled-in' .


Regards,
Steven Perryman
Daniel T.
2006-02-13 00:33:52 UTC
Permalink
Post by Miguel Oliveira e Silva
Post by Daniel T.
Post by Sasa
Hello,
I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
The definition of a precondition is that the function will give
undefined results if the precondition is not met.
No.
If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)
When a precondition fails the responsibility does
not belong to the routine (probably that was what
you were trying say with the "undefined behavior"),
being instead the caller's fault.
That is not what I was trying to say. A precondtion says, "this function
may do anything 'x' is not true." However, you are saying that the
function does something specific, it must throw an exception. That isn't
a precondtion. An example:

void fn( int x ) {
//precondition: x >= 0
}

Tells us, that there is no guarantee what will happen if x < 0

void fn( int x ) {
// postcondtion: ( x < 0 ) functions will throw bounds_error
}

Now *that* tells us that passing in an x that is less than 0 has a
defined result, it throws an exception.

You see, in the first example, the 'fn' code need not even bother to
check to see if x < 0. In the second example, the code must do something
specific if x < 0. That said, I often will put in an assert, after all
"undefined" means I can do whatever I want, so shutting down in debug
mode, but crashing in run mode are both acceptable behaviors.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
Miguel Oliveira e Silva
2006-02-13 15:40:19 UTC
Permalink
Post by Daniel T.
Post by Miguel Oliveira e Silva
Post by Daniel T.
Post by Sasa
Hello,
I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
The definition of a precondition is that the function will give
undefined results if the precondition is not met.
No.
If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)
When a precondition fails the responsibility does
not belong to the routine (probably that was what
you were trying say with the "undefined behavior"),
being instead the caller's fault.
That is not what I was trying to say. A precondtion says, "this function
may do anything 'x' is not true."
That is not the meaning of a precondition.
A precondition states a correctness condition.
If the condition does not hold then we are in the presence of
a program error. So, you are correct that it is indeed irrelevant
what the routine will do if (and only if) the assertion was not
executed, but the point is that if it is executable, then
a correctly implemented DbC mechanism must raise an
exception before the routine begins its execution.
In either case we are in the presence of a program error
(and that is an unacceptable behavior of any program).
Post by Daniel T.
However, you are saying that the
function does something specific, it must throw an exception. That isn't
void fn( int x ) {
//precondition: x >= 0
}
Tells us, that there is no guarantee what will happen if x < 0
An exception should be raised.
Post by Daniel T.
void fn( int x ) {
// postcondtion: ( x < 0 ) functions will throw bounds_error
}
Now *that* tells us that passing in an x that is less than 0 has a
defined result, it throws an exception.
(If I understand you correctly, you are using as an example an
incorrect implementation of DbC mechanism.)

If you take a look at Eiffel and at the origin of DbC
(Meyer, OOSC) you'll see the importance of clear
semantics for incorrect assertions, and its connection
with the exception mechanism.
Post by Daniel T.
You see, in the first example, the 'fn' code need not even bother to
check to see if x < 0.
Of course not. It is not its responsibility. Nevertheless, if the DbC
mechanism is correctly implemented, on precondition (x<0) failure,
an exception should be raised.
Post by Daniel T.
In the second example, the code must do something
specific if x < 0.
I don't understand your point. If I understand
correctly your code, the routine is stating its
postcondition to be (x<0). Hence, the routine
ensures that (x<0) immediately after its execution.
If that is not the case, an exception must be raised
(the responsibility, being a postcondition, belongs
to the routine).
Post by Daniel T.
That said, I often will put in an assert,
"assert" is a very primitive and limited form to
test assertions (it is not part of the class's interface,
and it is not inherited by descendant classes).
Post by Daniel T.
after all
"undefined" means I can do whatever I want, so shutting down in debug
mode, but crashing in run mode are both acceptable behaviors.
The only acceptable behavior of a program is to be correct.
Only in this case one should disable assertions.

No programming error (failing assertions) error is ever
an acceptable behavior.

Of course, quoting Dijkstra (EWD249, page 7):

"Program testing can be used to show the presence of bugs,
but never to show their absence."

So one should only disable assertions when and where it is
indeed necessary for efficiency concerns (or for non-critical
software in which we can easily pay the price of undetected
false assertions).

DbC is required to be supported by the programming language,
or else, some of its important properties will be lost.
Post by Daniel T.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
-miguel

--
Miguel Oliveira e Silva
Daniel T.
2006-02-13 16:41:25 UTC
Permalink
Post by Miguel Oliveira e Silva
Post by Daniel T.
Post by Miguel Oliveira e Silva
If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)
When a precondition fails the responsibility does
not belong to the routine (probably that was what
you were trying say with the "undefined behavior"),
being instead the caller's fault.
That is not what I was trying to say. A precondtion says, "this function
may do anything 'x' is not true."
That is not the meaning of a precondition.
A precondition states a correctness condition.
If the condition does not hold then we are in the presence of
a program error. So, you are correct that it is indeed irrelevant
what the routine will do if (and only if) the assertion was not
executed, but the point is that if it is executable, then
a correctly implemented DbC mechanism must raise an
exception before the routine begins its execution.
In either case we are in the presence of a program error
(and that is an unacceptable behavior of any program).
You seem quite caught up in the *mechanism* enforcing DbC in the
language rather than DbC as a design tool. Fine. We still agree on the
answer to the OP's question don't we?

void fn( int x );
// precondition x >= 0

means that no test needs to check for proper behavior if x < 0.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
Miguel Oliveira e Silva
2006-02-13 16:43:05 UTC
Permalink
Post by Daniel T.
Post by Miguel Oliveira e Silva
Post by Daniel T.
Post by Miguel Oliveira e Silva
If DbC mechanisms are implemented correctly,
a failure of a precondition (or any other assertion)
implies a failure of the routine raising an exception.
(This is not an undefined behavior.)
When a precondition fails the responsibility does
not belong to the routine (probably that was what
you were trying say with the "undefined behavior"),
being instead the caller's fault.
That is not what I was trying to say. A precondtion says, "this function
may do anything 'x' is not true."
That is not the meaning of a precondition.
A precondition states a correctness condition.
If the condition does not hold then we are in the presence of
a program error. So, you are correct that it is indeed irrelevant
what the routine will do if (and only if) the assertion was not
executed, but the point is that if it is executable, then
a correctly implemented DbC mechanism must raise an
exception before the routine begins its execution.
In either case we are in the presence of a program error
(and that is an unacceptable behavior of any program).
You seem quite caught up in the *mechanism* enforcing DbC in the
language rather than DbC as a design tool.
Actually I'm caught up by both. In my opinion an appropriate language
support is required.
Post by Daniel T.
Fine. We still agree on the
answer to the OP's question don't we?
Yes we do.
Post by Daniel T.
void fn( int x );
// precondition x >= 0
means that no test needs to check for proper behavior if x < 0.
Agreed.
Post by Daniel T.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
Best regards,

-miguel

--
Miguel Oliveira e Silva
Oliver Wong
2006-02-14 18:26:38 UTC
Permalink
Post by Miguel Oliveira e Silva
Post by Daniel T.
That is not what I was trying to say. A precondtion says, "this function
may do anything 'x' is not true."
That is not the meaning of a precondition.
A precondition states a correctness condition.
If the condition does not hold then we are in the presence of
a program error. So, you are correct that it is indeed irrelevant
what the routine will do if (and only if) the assertion was not
executed, but the point is that if it is executable, then
a correctly implemented DbC mechanism must raise an
exception before the routine begins its execution.
In either case we are in the presence of a program error
(and that is an unacceptable behavior of any program).
Post by Daniel T.
However, you are saying that the
function does something specific, it must throw an exception. That isn't
void fn( int x ) {
//precondition: x >= 0
}
Tells us, that there is no guarantee what will happen if x < 0
An exception should be raised.
I'm in agreement with Daniel T. If a pre-condition to a method does not
hold, then the method may do anything it wants. This is distinct from "the
method must throw an exception".

If the desired behaviour is for the method to throw an exception when
some condition does not hold, then that should be documented, e.g.:

<dbc>
pre-conditions:
none

post-conditions:
if x >= 0
return x
if x < 0
throws an exception.
</dbc>

The reason for this is that you may have pre-conditions that may be
difficult to check in the method you're implementing, but which is trivial
to check in the calling code. So by listing the pre-condition, you're
basically saying "I'm not responsible for what happens if [condition foo] is
false; so you'd better check that [condition foo] is true before calling
me."

Imagine, for example, a binary search method. It might have as a
pre-condition that the array passed in is sorted in ascending order, and
then will return true or false depending on whether a given member is
present in the array. It also guarantees O(log(n)) runtime performance. If
the method had to actually *CHECK* the condition that the array was sorted,
the method would be impossible to implement, as it would need at least O(n)
running time, to scan through the whole array and verify that it is sorted.
So the method does NOT check the precondition: it just assumes that the
pre-condition holds, and it is not defined what will happen if the
pre-condition doesn't hold.

- Oliver
GeoffS
2006-02-14 18:49:53 UTC
Permalink
Post by Oliver Wong
If the desired behaviour is for the method to throw an exception when
some condition does not hold, then that should be documented,
Even simpler, replace "should be documented" with "is part of the
contract" - end of discussion.

Cheers,

Geoff S.
Miguel Oliveira e Silva
2006-02-14 22:10:26 UTC
Permalink
Post by Oliver Wong
Post by Miguel Oliveira e Silva
Post by Daniel T.
That is not what I was trying to say. A precondtion says, "this function
may do anything 'x' is not true."
That is not the meaning of a precondition.
A precondition states a correctness condition.
If the condition does not hold then we are in the presence of
a program error. So, you are correct that it is indeed irrelevant
what the routine will do if (and only if) the assertion was not
executed, but the point is that if it is executable, then
a correctly implemented DbC mechanism must raise an
exception before the routine begins its execution.
In either case we are in the presence of a program error
(and that is an unacceptable behavior of any program).
Post by Daniel T.
However, you are saying that the
function does something specific, it must throw an exception. That isn't
void fn( int x ) {
//precondition: x >= 0
}
Tells us, that there is no guarantee what will happen if x < 0
An exception should be raised.
I'm in agreement with Daniel T. If a pre-condition to a method does not
hold, then the method may do anything it wants. This is distinct from "the
method must throw an exception".
At the risk of a circular discussion (I apologize if that is the case),
I must call up to your attention that preconditions (postconditions,
class invariants, and any other type of assertion) are correctness
conditions. Hence, its goal is to ensure that either the program
works as expected (considering the conditions expressed in those
assertions) or does not work at all (no compromise here).

What Daniel and you are saying (in the small part in which
we disagree) is that it may not be important the behavior of
a routine when a (runnable) precondition is false.
However that goes against one of the main goals of DbC: to
ensure that the program does not behave incorrectly (which is not,
in real software, exactly the same as to behave correctly).

So DbC is a tool for constructing not "just" correct software,
but also reliable (correct *and* robust) software
[Meyer, OOSC2ed chapters 11 and 12]. To allow
a routine to proceed "normally" in the presence of a false
(runnable) assertion would be just like the primitive C use
of function return values, or global variables as 'errno',
for signaling program errors (It kind of reminds me
of Douglas Adams's The Hitch Hiker's Guide to the Galaxy,
in which the project to build a bypass intergalactical route
through Earth, had been available for discussion
for many centuries...). Ok the error is detected, but
the program part responsible for it may not be
warned and the program behavior if not forced
to act accordantly.

DbC is not just a high-level design and documentation
tool for quality program construction. It is also a debugging
tool and a powerful technique to built fault-tolerant systems
(if we are not sure to be able to tracks all errors, then we
must find a simple way to live and bypass them).
The exception behavior is essential to use DbC for
all this uses.

To make my case short, my stubbornness in this
particular point is based in two facts:

1. DbC applies to all those uses;

2. The DbC creator - Bertrand Meyer - defined quite
clearly what this technique is, and the exception behavior
was part of it from the very beginning.

We should not use the same terminology - DbC - to
mean different things. There is already enough fuzziness
and confusion in this group with messages mixing
different flavors of OOP and OOL (without, too many times,
a rational constructive debate comparing them),
and - of course - the destructive "contribution" of
anti-OO guys (On the other hand, a circus cannot live
only of acrobats and magicians [*]!).

[*] Anti-OO guys, don't take it personally, it is just a joke.
Post by Oliver Wong
If the desired behaviour is for the method to throw an exception when
It is documented (that was one of my points).
That is part of the DbC semantics [OOSC2d, chapter 12].
Post by Oliver Wong
<dbc>
none
if x >= 0
return x
if x < 0
throws an exception.
</dbc>
The reason for this is that you may have pre-conditions that may be
difficult to check in the method you're implementing, but which is trivial
to check in the calling code.
Either they are runnable, or they are not. In the latter case, DbC can only
be used for design and documentation purposes. In the former, regardless
of how long it takes to execute the assertion, it should be used to
*ensure* that the program is correct (or not at all).

I suppose that by "trivial" you mean "fast" (efficient). That is irrelevant
"99%" of the cases. With the possible exception of real-time programs
(and even here the problem is not efficiency but predictability), there
is no timing constraint inherent to programs. So one should only be concern
with such things if it is really necessary, and after we sufficiently
confident that the program behaves correctly.
Post by Oliver Wong
So by listing the pre-condition, you're
basically saying "I'm not responsible for what happens if [condition foo] is
false; so you'd better check that [condition foo] is true before calling
me."
Your phrase reveals a misconception (sorry for my rudeness).
Assertions are a tool not only to ensure that the unit (class)
behaves correctly, but also its clients (that is the reason why
reusable, even if highly tested, library classes should be
used with preconditions activated) and the program as a whole.
In general, the programmer is responsible for all of them. So although
you are correct in implying that DbC distributes the responsibility
between different parts of a program (the class and its clients),
the ultimate goal is to produce a correct program and that
is the programmer's responsibility (and job).

A runnable precondition that does not trigger an exception
(or terminates the program in the absence of this mechanism)
will not give a fast and precise aid to the programmer.
Half of the programmer - the unit creator - will be pleased
to know that the error is not its responsibility; the other half
- the unit's faulty client - we be furious for not be immediately
warned of the error (who knows, he may even unfairly blame
the DbC technique, when the problem was simply an erroneous
DbC implementation).
Post by Oliver Wong
Imagine, for example, a binary search method. It might have as a
pre-condition that the array passed in is sorted in ascending order, and
then will return true or false depending on whether a given member is
present in the array. It also guarantees O(log(n)) runtime performance. If
the method had to actually *CHECK* the condition that the array was sorted,
the method would be impossible to implement, as it would need at least O(n)
running time, to scan through the whole array and verify that it is sorted.
That is not important (in "90%" of final products of software,
and in 99.9999...% of it when is being developed).

One can always (if decent programming environments) activate or
deactivate assertions within individual objects.

When the program is to be released, and if it matters, deactivate
the assertions you like. That has little to do with the development
phase of program construction in which all the help to track errors
is precious.
Post by Oliver Wong
So the method does NOT check the precondition: it just assumes that the
pre-condition holds, and it is not defined what will happen if the
pre-condition doesn't hold.
(That's playing Russian roulette with your program.)
Post by Oliver Wong
- Oliver
Best regards,

-miguel

--
Miguel Oliveira e Silva
Oliver Wong
2006-02-14 22:53:05 UTC
Permalink
"Miguel Oliveira e Silva" <***@det.ua.pt> wrote in message news:***@det.ua.pt...
[snip]
Post by Miguel Oliveira e Silva
To make my case short, my stubbornness in this
1. DbC applies to all those uses;
2. The DbC creator - Bertrand Meyer - defined quite
clearly what this technique is, and the exception behavior
was part of it from the very beginning.
We should not use the same terminology - DbC - to
mean different things. There is already enough fuzziness
and confusion in this group with messages mixing
different flavors of OOP and OOL (without, too many times,
a rational constructive debate comparing them),
and - of course - the destructive "contribution" of
anti-OO guys (On the other hand, a circus cannot live
only of acrobats and magicians [*]!).
[*] Anti-OO guys, don't take it personally, it is just a joke.
Well, I don't know what Bertrand Meyer said or didn't say, but I'm
looking at this from a utility or expressiveness point of view. If we take
the interpretation that one does not need to check pre-conditions, then we
allow for the non-checking of pre-conditions when such a thing is desired or
needed (e.g. real time code, or that "last 1%" that you mention later on),
and yet we still have the flexibility of expressing that the code *must*
check some condition (which I shall not call a "pre-condition") as part of
the contract.

If we use the interpretation that pre-conditions must always be needed,
then we cannot handle that "last 1%".
Post by Miguel Oliveira e Silva
Post by Oliver Wong
If the desired behaviour is for the method to throw an exception when
It is documented (that was one of my points).
That is part of the DbC semantics [OOSC2d, chapter 12].
Post by Oliver Wong
<dbc>
none
if x >= 0
return x
if x < 0
throws an exception.
</dbc>
The reason for this is that you may have pre-conditions that may be
difficult to check in the method you're implementing, but which is trivial
to check in the calling code.
Either they are runnable, or they are not. In the latter case, DbC can only
be used for design and documentation purposes. In the former, regardless
of how long it takes to execute the assertion, it should be used to
*ensure* that the program is correct (or not at all).
If they are runnable in a given language/environment/whatever, I would
think that there is the possibility to disable the running/verification of
pre-conditions if desired. If they are not runnable, then they won't be run
(by definition).

Either way, to me the testing or non-testing of preconditions is not
part of the behaviour of a program, but rather is a tool for verifying
correctness of a program. If the desired behaviour of the program is to
throw an exception under certain conditions, then that should be documented
as part of the contract, and not merely listed as a pre-condition.
Post by Miguel Oliveira e Silva
I suppose that by "trivial" you mean "fast" (efficient).
No, I did not mean to limit the meaning of "trivial" to
runtime-efficientcy. Imagine, for example, that I am writing a program which
takes as input the string representation of a C++ program and returns a
string representation of what output to standard-out the C++ program would
generate if it were run.

I might have as preconditions "The C++ program must represent a program
that eventually terminates", and "There does not exist an execution path
through the C++ program which requires reading from Standard In", and other
such conditions. It is known that these pre-conditions are impossible to
test on a computer (see Turing's Halting Problem).

My job is developing code-analysis and compiler-like tools, so I have to
write methods which do stuff like the above all the time. Almost everywhere,
we are assuming that we're going to analyze actual valid code, so we don't
actually do type checking on the code or anything like that. We assume the
user is only interested in validating code that would actually compile with
a normal compiler, and not, random garbage files.

We have lots of pre-conditions that we don't check, because it literally
impossible to check them.

[...]
Post by Miguel Oliveira e Silva
Post by Oliver Wong
So by listing the pre-condition, you're
basically saying "I'm not responsible for what happens if [condition foo] is
false; so you'd better check that [condition foo] is true before calling
me."
Your phrase reveals a misconception (sorry for my rudeness).
Assertions are a tool not only to ensure that the unit (class)
behaves correctly, but also its clients (that is the reason why
reusable, even if highly tested, library classes should be
used with preconditions activated) and the program as a whole.
In general, the programmer is responsible for all of them. So although
you are correct in implying that DbC distributes the responsibility
between different parts of a program (the class and its clients),
the ultimate goal is to produce a correct program and that
is the programmer's responsibility (and job).
The problem with your reasoning is that sometimes the person programming
the calling code and the person programming the called code is not the same
person.
Post by Miguel Oliveira e Silva
A runnable precondition that does not trigger an exception
(or terminates the program in the absence of this mechanism)
will not give a fast and precise aid to the programmer.
The requirement that all pre-conditions be runnable places some really
big limitations on what can be expressed with pre-conditions.

But to me, we're just arguing about names. Basically what's happening is
that I'm documenting my code with (non-executable) statements like "Don't
call this method unless [condition foo] is true". You don't want to call
that a pre-condition, and you don't want to call what I do "Design by
Contract". Fine. But what I'm doing is still useful to me and my coworkers,
so we will continue doing it, no matter what label you wish to apply to it.

- Oliver
Miguel Oliveira e Silva
2006-02-15 11:00:30 UTC
Permalink
Post by Oliver Wong
[snip]
Post by Miguel Oliveira e Silva
To make my case short, my stubbornness in this
1. DbC applies to all those uses;
2. The DbC creator - Bertrand Meyer - defined quite
clearly what this technique is, and the exception behavior
was part of it from the very beginning.
We should not use the same terminology - DbC - to
mean different things. There is already enough fuzziness
and confusion in this group with messages mixing
different flavors of OOP and OOL (without, too many times,
a rational constructive debate comparing them),
and - of course - the destructive "contribution" of
anti-OO guys (On the other hand, a circus cannot live
only of acrobats and magicians [*]!).
[*] Anti-OO guys, don't take it personally, it is just a joke.
Well, I don't know what Bertrand Meyer said or didn't say,
Since he is the creator of DbC perhaps you should (or else
use a different terminology).
Post by Oliver Wong
but I'm
looking at this from a utility or expressiveness point of view. If we take
the interpretation that one does not need to check pre-conditions, then we
allow for the non-checking of pre-conditions when such a thing is desired or
needed
Of course. That is part of DbC.
Post by Oliver Wong
(e.g. real time code, or that "last 1%" that you mention later on),
and yet we still have the flexibility of expressing that the code *must*
check some condition (which I shall not call a "pre-condition") as part of
the contract.
I'm not sure I understand your point (sorry). Nothing is lost when using
DbC as it was originally created (raising exceptions for broken runnable contracts).
You can activate or deactivate the assertions you like. Iff the program is
correct - in a sequential program - its logical behavior will be exactly
the same.
Post by Oliver Wong
If we use the interpretation that pre-conditions must always be needed,
then we cannot handle that "last 1%".
Comment can be used in preconditions (read more
carefully my messages).
Post by Oliver Wong
Post by Miguel Oliveira e Silva
Post by Oliver Wong
If the desired behaviour is for the method to throw an exception when
It is documented (that was one of my points).
That is part of the DbC semantics [OOSC2d, chapter 12].
Post by Oliver Wong
<dbc>
none
if x >= 0
return x
if x < 0
throws an exception.
</dbc>
The reason for this is that you may have pre-conditions that may be
difficult to check in the method you're implementing, but which is trivial
to check in the calling code.
Either they are runnable, or they are not. In the latter case, DbC can only
be used for design and documentation purposes. In the former, regardless
of how long it takes to execute the assertion, it should be used to
*ensure* that the program is correct (or not at all).
If they are runnable in a given language/environment/whatever, I would
think that there is the possibility to disable the running/verification of
pre-conditions if desired.
Of course.
Post by Oliver Wong
If they are not runnable, then they won't be run
(by definition).
Right.
Post by Oliver Wong
Either way, to me the testing or non-testing of preconditions is not
part of the behaviour of a program, but rather is a tool for verifying
correctness of a program.
The same for me (in sequential programs).
Post by Oliver Wong
If the desired behaviour of the program is to
throw an exception under certain conditions, then that should be documented
as part of the contract, and not merely listed as a pre-condition.
That behavior it is part of the contract (I've already explained
why, so I won't repeat myself).
Post by Oliver Wong
Post by Miguel Oliveira e Silva
I suppose that by "trivial" you mean "fast" (efficient).
No, I did not mean to limit the meaning of "trivial" to
runtime-efficientcy. Imagine, for example, that I am writing a program which
takes as input the string representation of a C++ program and returns a
string representation of what output to standard-out the C++ program would
generate if it were run.
I might have as preconditions "The C++ program must represent a program
that eventually terminates", and "There does not exist an execution path
through the C++ program which requires reading from Standard In", and other
such conditions. It is known that these pre-conditions are impossible to
test on a computer (see Turing's Halting Problem).
Ok, so you are in the presence of a non-runnable assertion (which - of course -
cannot raise exceptions when it fails because it is not tested).

When using DbC one should as much as possible express runnable
assertions. In your example, a good start would be a precondition
that ensured a syntactic correct C program, hence releasing the routine
for having to worry about this important case.

(I still can't see why do you think that goes against my points.)
Post by Oliver Wong
My job is developing code-analysis and compiler-like tools, so I have to
write methods which do stuff like the above all the time. Almost everywhere,
we are assuming that we're going to analyze actual valid code, so we don't
actually do type checking on the code or anything like that.
(Why not?)
Post by Oliver Wong
We assume the
user is only interested in validating code that would actually compile with
a normal compiler, and not, random garbage files.
(A wrong approach IMO.)

The program should make no assumptions regarding its
interaction with outside entities. However, within itself,
it should clearly delegate responsibilities between its
different parts and make sure - as much as possible -
that those responsibility are enforced.
Post by Oliver Wong
We have lots of pre-conditions that we don't check, because it literally
impossible to check them.
In my programs I have also quite a few.

However, I strongly advise you to make runnable approximations
(if we cannot express a necessary-and-sufficient runnable condition,
we should at least express necessary conditions) of all those
assertions. The quality of your code - and the confidence
that it is correct - will most certainly rise dramatically.
Post by Oliver Wong
[...]
Post by Miguel Oliveira e Silva
Post by Oliver Wong
So by listing the pre-condition, you're
basically saying "I'm not responsible for what happens if [condition foo] is
false; so you'd better check that [condition foo] is true before calling
me."
Your phrase reveals a misconception (sorry for my rudeness).
Assertions are a tool not only to ensure that the unit (class)
behaves correctly, but also its clients (that is the reason why
reusable, even if highly tested, library classes should be
used with preconditions activated) and the program as a whole.
In general, the programmer is responsible for all of them. So although
you are correct in implying that DbC distributes the responsibility
between different parts of a program (the class and its clients),
the ultimate goal is to produce a correct program and that
is the programmer's responsibility (and job).
The problem with your reasoning is that sometimes the person programming
the calling code and the person programming the called code is not the same
person.
Why do you think that is a problem? If you take a closer
look at my arguments you'll see that's not relevant.

In fact, I would say that if the unit's programmer is not the
same as its potential users, then it is even more important
to have runnable assertions that raise exceptions on failure.

Preconditions, postconditions and invariants (should) express
the Abstract Data Type semantics of the class.
It is of paramount importance that those semantics are
not only clearly understood by the class's clients,
but also enforced by the class itself.
Post by Oliver Wong
Post by Miguel Oliveira e Silva
A runnable precondition that does not trigger an exception
(or terminates the program in the absence of this mechanism)
will not give a fast and precise aid to the programmer.
The requirement that all pre-conditions be runnable places some really
big limitations on what can be expressed with pre-conditions.
(Please read more carefully my messages.)

Nobody is saying that only runnable assertions are part of DbC
(comments were there from the very beginning).
The point is that if they are, then on failure an exception is
required to be raised.
Post by Oliver Wong
But to me, we're just arguing about names.
(Yes and no. There are some important technical
aspects of DbC that you are missing.)

Anyway, names and their precise meaning are
very important or else there will be a lot of noise
when we use them to communicate with each other.

And of course, as I said before, DbC is a terminology
coined by Bertrand Meyer (to mean exactly what I
am saying).
Post by Oliver Wong
Basically what's happening is
that I'm documenting my code with (non-executable) statements like "Don't
call this method unless [condition foo] is true". You don't want to call
that a pre-condition,
I never said such a thing (please read more carefully my
messages). Comments are part of DbC.
Post by Oliver Wong
and you don't want to call what I do "Design by
Contract". Fine. But what I'm doing is still useful to me and my coworkers,
so we will continue doing it, no matter what label you wish to apply to it.
It is not my label. It is the *meaning* of DbC (OOSC1ed, chapter 7).

I have no problem (why should I?) that you use whatever suits
your needs, but - when speaking about it - you should not use
an incorrect terminology.
Post by Oliver Wong
- Oliver
Best regards,

-miguel

--
Miguel Oliveira e Silva
Oliver Wong
2006-02-15 18:27:39 UTC
Permalink
Post by Miguel Oliveira e Silva
Post by Oliver Wong
I might have as preconditions "The C++ program must represent a program
that eventually terminates", and "There does not exist an execution path
through the C++ program which requires reading from Standard In", and other
such conditions. It is known that these pre-conditions are impossible to
test on a computer (see Turing's Halting Problem).
Ok, so you are in the presence of a non-runnable assertion (which - of course -
cannot raise exceptions when it fails because it is not tested).
This was all I was saying. There exist situations where the program will
NOT test the pre-condition, because it's impossible to test them. And thus
the program cannot raise exceptions.

Therefore, a programmer/designer should not RELY on the fact that the
pre-conditions will be tested.

Therefore the calling code should not RELY on the method being
guaranteed to throw an exception if the pre-conditions are not met.

Simply, it is not defined what happens when the pre-condition is not
met. Maybe it throws an exception, but maybe it does something else. You
don't know for sure.

- Oliver
Daniel T.
2006-02-15 13:17:40 UTC
Permalink
Post by Miguel Oliveira e Silva
What Daniel and you are saying (in the small part in which
we disagree) is that it may not be important the behavior of
a routine when a (runnable) precondition is false.
However that goes against one of the main goals of DbC: to
ensure that the program does not behave incorrectly (which is not,
in real software, exactly the same as to behave correctly).
Do you see the inherent contradiction in the above? How can a function
behave incorrectly in a situation for which no behavior has has been
defined?

We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
Post by Miguel Oliveira e Silva
So DbC is a tool for constructing not "just" correct software,
but also reliable (correct *and* robust) software
[Meyer, OOSC2ed chapters 11 and 12]. To allow
a routine to proceed "normally" in the presence of a false
(runnable) assertion would be just like the primitive C use
of function return values, or global variables as 'errno',
for signaling program errors
Your comparison is way off. The C use of return values and global
variables for error conditions are *defined* behaviors. We can test to
ensure they happen because we know what is supposed to happen given
certain input. Preconditions are nothing of the sort.
Post by Miguel Oliveira e Silva
Post by Oliver Wong
So the method does NOT check the precondition: it just assumes that the
pre-condition holds, and it is not defined what will happen if the
pre-condition doesn't hold.
(That's playing Russian roulette with your program.)
No, that's proper distribution of responsibility. If it isn't my
function's responsibility to ensure x > 0, why on earth would I have
code in my function checking the value of x? The responsible party
should be doing that.

As soon as you define what the function does if the precondition isn't
met, you *take responsibility* for the error. If your function doesn't
throw, then it's *your* fault, not the clients because *you said* that
your function would throw in that situation.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
S Perryman
2006-02-15 13:59:47 UTC
Permalink
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.

Components are bound to pre/post/invariant conditions.
The behaviour is : pre IMPLIES X

1. When pre is satisifed, X = (post AND invariant)
2. When pre is not satisfied, X = ??

X could actually be (post AND invariant) in "certain situations" (pure luck
etc) ,
but the DBC mindset is to assume it is undefined.
And hope X != physical damage of any kind.


Regards,
Steven Perryman
Dmitry A. Kazakov
2006-02-15 15:25:14 UTC
Permalink
Post by S Perryman
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.
Yes, but the point is true.
Post by S Perryman
Components are bound to pre/post/invariant conditions.
The behaviour is : pre IMPLIES X
1. When pre is satisifed, X = (post AND invariant)
2. When pre is not satisfied, X = ??
Then X can be any. I assume that IMPLIES is the standard implication "=>".
So a=>b is ^aVb. Therefore with false preconditions behavior is always
correct. Or to put it in other words:

Program stays correct whatever it does when the precondition is false.
Post by S Perryman
X could actually be (post AND invariant) in "certain situations" (pure luck
etc) , but the DBC mindset is to assume it is undefined.
Evaluation of program correctness is *not* what the program itself does.
The rest trivially follows [i.e. Miguel is wrong, Daniel is right, though
maybe inaccurate.]
Post by S Perryman
And hope X != physical damage of any kind.
= Correctness is worth of nothing if preconditions aren't satisfied.

Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Phlip
2006-02-15 15:51:53 UTC
Permalink
Post by Dmitry A. Kazakov
Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
Why thank you! It's also an excellent example of a thrown exception not
caught. (The hardware bus interpreted the exception value as a scalar to
move the engines. Way over.)

The root software problem was a typecast, so an int and a float violated
each others's tiny little contract!
--
Phlip
http://www.greencheese.org/ZeekLand <-- NOT a blog!!!
Dmitry A. Kazakov
2006-02-15 17:47:05 UTC
Permalink
Post by Phlip
Post by Dmitry A. Kazakov
Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
Why thank you! It's also an excellent example of a thrown exception not
caught. (The hardware bus interpreted the exception value as a scalar to
move the engines. Way over.)
It need not to be caught, because the precondition [Ariane IV] implied that
it may not be thrown.

Take any program, compile it for x86 and run on a PowerPC. Would it make
program, compiler, processor incorrect?
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Phlip
2006-02-15 17:55:21 UTC
Permalink
Post by Dmitry A. Kazakov
It need not to be caught, because the precondition [Ariane IV] implied
that it may not be thrown.
Take any program, compile it for x86 and run on a PowerPC. Would it make
program, compiler, processor incorrect?
Violent agreement, dude. I was just pointing out the actual facts were the
exception was thrown, not caught, and mis-interpreted.
--
Phlip
http://www.greencheese.org/ZeekLand <-- NOT a blog!!!
S Perryman
2006-02-15 16:09:10 UTC
Permalink
Post by Dmitry A. Kazakov
Post by S Perryman
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.
Yes, but the point is true.
Daniels' overall point, yes (IMHO) . His statement above is not.
Post by Dmitry A. Kazakov
Post by S Perryman
Components are bound to pre/post/invariant conditions.
The behaviour is : pre IMPLIES X
1. When pre is satisifed, X = (post AND invariant)
2. When pre is not satisfied, X = ??
Then X can be any. I assume that IMPLIES is the standard implication "=>".
So a=>b is ^aVb. Therefore with false preconditions behavior is always
No. It only means that the DBC *behavioural relationship* holds.
Post by Dmitry A. Kazakov
Post by S Perryman
X could actually be (post AND invariant) in "certain situations" (pure luck
etc) , but the DBC mindset is to assume it is undefined.
pre IMPLIES (inv AND post)
1. false IMPLIES false
2. false IMPLIES true

Both 1 and 2 evaluate to true. But what do they actually mean ??

For 1, the pre-condition does not hold, and neither does (inv AND post) .
In this case, failure to satisfy the pre-condition has resulted in a failure
to
satisfy (inv AND post) . The relationship holds.

For 2, the pre-condition does not hold, but (inv AND post) does.
In this case, we have been lucky in terms of consequences.
The relationship holds.

Just to complete the relationship :

true IMPLIES false = correct user behaviour, defect in component supplier
true IMPLIES true = correct user/supplier behaviour (the desired goal) .
Post by Dmitry A. Kazakov
Program stays correct whatever it does when the precondition is false.
The program is not correct for 1. Because (inv AND post) does not hold.
The program is correct for 2, because even though pre did not hold, somehow
(inv AND post) has managed to remain correct.

Or a bit more formally :

AND [ pre1, post1 AND inv1, pre2, post2 AND inv2, ... ]

which is not the same as :

AND [ dbc-rel(pre1,post1,inv1) , dbc-rel(pre2,post2,inv2) , ... ]

dbc-rel(pre,post,inv) = (pre IMPLIES (post AND inv) )
Post by Dmitry A. Kazakov
Miguel is wrong, Daniel is right, though maybe inaccurate
The expression of his argument is somewhat wanting IMHO.
Post by Dmitry A. Kazakov
Post by S Perryman
And hope X != physical damage of any kind.
= Correctness is worth of nothing if preconditions aren't satisfied.
Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
A system configuration management (CM) problem.
AFAIK something that was not actually expressed in Ariane s/w as a DBC
pre-condition.


Regards,
Steven Perryman
Dmitry A. Kazakov
2006-02-15 17:49:48 UTC
Permalink
Post by S Perryman
Post by Dmitry A. Kazakov
Post by S Perryman
Components are bound to pre/post/invariant conditions.
The behaviour is : pre IMPLIES X
1. When pre is satisifed, X = (post AND invariant)
2. When pre is not satisfied, X = ??
Then X can be any. I assume that IMPLIES is the standard implication "=>".
So a=>b is ^aVb. Therefore with false preconditions behavior is always
No. It only means that the DBC *behavioural relationship* holds.
There is nothing beyond that at this level. One could go one meta level up
and evaluate correctness of preconditions, but that would be a different
correctness.
Post by S Perryman
Post by Dmitry A. Kazakov
Post by S Perryman
X could actually be (post AND invariant) in "certain situations" (pure
luck etc) , but the DBC mindset is to assume it is undefined.
pre IMPLIES (inv AND post)
1. false IMPLIES false
2. false IMPLIES true
Both 1 and 2 evaluate to true. But what do they actually mean ??
For 1, the pre-condition does not hold, and neither does (inv AND post) .
In this case, failure to satisfy the pre-condition has resulted in a failure
to satisfy (inv AND post) . The relationship holds.
For 2, the pre-condition does not hold, but (inv AND post) does.
In this case, we have been lucky in terms of consequences.
The relationship holds.
true IMPLIES false = correct user behaviour, defect in component supplier
true IMPLIES true = correct user/supplier behaviour (the desired goal) .
Post by Dmitry A. Kazakov
Program stays correct whatever it does when the precondition is false.
The program is not correct for 1. Because (inv AND post) does not hold.
No. In this case the "correctness" would be defined as pre & inv & post. It
can be expressed using implication:

new-pre = true
new-post = old-inv & old-post & old-pre

I.e. under any circumstances old-inv & old-post & old-pre must hold. This
isn't very useful, because, obviously, a program cannot influence its
precondition. So you probably would like to reduce it to a weaker:

new-pre' = true
new-post' = old-inv & old-post

But this is still too strong because it would not allow decomposition.

Probably you meant another correctness and another semantic layer. Ariane V
wasn't correct in the sense that nobody wished it exploding. Nevertheless,
the program was correct. If you add 1 to 1, meaning actually Pi/2, that
wouldn't make an implementation of + returning 2 incorrect.
Post by S Perryman
Post by Dmitry A. Kazakov
Post by S Perryman
And hope X != physical damage of any kind.
= Correctness is worth of nothing if preconditions aren't satisfied.
Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
A system configuration management (CM) problem.
AFAIK something that was not actually expressed in Ariane s/w as a DBC
pre-condition.
When the hardware specification of a sensor defines the values range, you
have to rely on that contract. There is no software way to enforce this
contract. It is a management problem. A review should have been made when
Ariane IV software was reused for Ariane V. It wasn't. AFAIK, software
people warned managers, but those, as always, knew it better. So the
result.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
S Perryman
2006-02-16 08:54:44 UTC
Permalink
SP>Components are bound to pre/post/invariant conditions.
SP>The behaviour is : pre IMPLIES X

SP>1. When pre is satisifed, X = (post AND invariant)
SP>2. When pre is not satisfied, X = ??

DM> Then X can be any. I assume that IMPLIES is the standard implication
"=>".
DM> So a=>b is ^aVb. Therefore with false preconditions behavior is always
Post by Dmitry A. Kazakov
Post by S Perryman
No. It only means that the DBC *behavioural relationship* holds.
There is nothing beyond that at this level.
Correct.
It is only an expression of whether your DBC mechanism is working.
Post by Dmitry A. Kazakov
Post by S Perryman
pre IMPLIES (inv AND post)
1. false IMPLIES false
2. false IMPLIES true
Both 1 and 2 evaluate to true. But what do they actually mean ??
For 1, the pre-condition does not hold, and neither does (inv AND post) .
In this case, failure to satisfy the pre-condition has resulted in a failure
to satisfy (inv AND post) . The relationship holds.
For 2, the pre-condition does not hold, but (inv AND post) does.
In this case, we have been lucky in terms of consequences.
The relationship holds.
true IMPLIES false = correct user behaviour, defect in component supplier
true IMPLIES true = correct user/supplier behaviour (the desired goal) .
DM>Program stays correct whatever it does when the precondition is false.
Post by Dmitry A. Kazakov
Post by S Perryman
The program is not correct for 1. Because (inv AND post) does not hold.
No. In this case the "correctness" would be defined as pre & inv & post.
Which is what I stated in the part of the posting you have snipped.
To re-iterate:

For an executable entity E, with pre/post/invariant conditions :

1. dbc-correct(E) = (pre IMPLIES (post AND inv) )
2. program-correct(E) = ( pre AND (post AND inv) )

which are obviously not the same thing.

So the DBC stuff is not working correctly if 1 does hold for E.
And the program that E is part of, is not correct if 2 does not hold.
Post by Dmitry A. Kazakov
Probably you meant another correctness and another semantic layer.
Nope. I know what I meant
That a pre-condition failure usually means that the post-condition may not
hold.
And even if post does hold, pre-condition failure and post-condition holds
is
correct DBC behaviour. But does not mean that the program is correct.
Post by Dmitry A. Kazakov
Ariane V wasn't correct in the sense that nobody wished it exploding.
Nevertheless,
the program was correct.
You are saying that the s/w was correct, for a target system configuration.
But the sys configuration was not the target configuration.
Post by Dmitry A. Kazakov
[ Ariane V historical info snipped, but acknowledged ... ]
Regards,
Steven Perryman
Miguel Oliveira e Silva
2006-02-15 17:03:57 UTC
Permalink
Post by Dmitry A. Kazakov
Post by S Perryman
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.
Yes, but the point is true.
Which point? That it does not matter what the routine
does in a false (runnable) precondition? Of course not, it
should never be executed (which is my point, and
DbC's correct behavior)!

When using DbC we implement routines assuming
that its precondition and its class invariant holds
(or else, we would be doing defensive programming).
We most certainly won't be worry to provide a
specific behavior in that implementation for those
cases (just because, we are ensured that such
mistakes are caught by assertions).

A false precondition is an incorrect behavior of the
*program* (due to the client's failure).

A false invariant or postcondition is an incorrect behavior
of the program resulting from an incorrect behavior of the
class.

(I do feel I'm repeating myself too much. Please read
more carefully my messages.)
Post by Dmitry A. Kazakov
Post by S Perryman
Components are bound to pre/post/invariant conditions.
The behaviour is : pre IMPLIES X
1. When pre is satisifed, X = (post AND invariant)
2. When pre is not satisfied, X = ??
Then X can be any.
Of course. It does not matter, the program is *incorrect*,
hence it should - as much as possible - behave accordantly
(using the exception mechanism, which exits for this very
reason).

Please remember that preconditions are not part of the
routine's implementation, they belong to its interface,
so it is not acceptable to allow its behavior (of the
preconditions) to ignore a false runnable assertion.
Post by Dmitry A. Kazakov
I assume that IMPLIES is the standard implication "=>".
So a=>b is ^aVb. Therefore with false preconditions behavior is always
Program stays correct whatever it does when the precondition is false.
Post by S Perryman
X could actually be (post AND invariant) in "certain situations" (pure luck
etc) , but the DBC mindset is to assume it is undefined.
Evaluation of program correctness is *not* what the program itself does.
The rest trivially follows [i.e. Miguel is wrong, Daniel is right, though
maybe inaccurate.]
No I'm not (take a closer look at my messages).
Post by Dmitry A. Kazakov
Post by S Perryman
And hope X != physical damage of any kind.
= Correctness is worth of nothing if preconditions aren't satisfied.
Of course, the program is *incorrect*.
Post by Dmitry A. Kazakov
Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
The program was incorrect (or else - by definition - it would
have worked).

The confusion towards what are assertions and their
part and connection to programs, as is surprisingly
happening here, was - probably (I would have to
verify that, so I might be wrong) - the cause of failure.

Of course, taking my argument a little further away, a disciplined
exception mechanism [OOSC2ed, chapter 12] is required to
take the simple (and yet extremely powerful) view of DbC to
its full extent (which is a much stronger semantics
than the basic requirement of simply an exception being
raised when an assertion is false).

Considering all its assertions, either a routine fails or it
succeeds (no "nowhere's" land in between). A routine
can only succeed iff its precondition is true when called
and if it ensures its postcondition and the class's invariant
at exit. A routine failure *always* raises an exception
(the handler may propagate such exception up in the call
stack, or it can solve the problem and *retry* the execution
of the routine).

Anyway, previously in this thread, I was simply stating
that the only acceptable behavior in a program when
an assertion is evaluated to a false value, is to raise
an exception (even within a non-disciplined exception
mechanism as is the case of Java, Ada or C++); and
that this behavior is an integral part of DbC.
Post by Dmitry A. Kazakov
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Best regards,

-miguel

--
Miguel Oliveira e Silva
Dmitry A. Kazakov
2006-02-15 19:22:52 UTC
Permalink
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.
Yes, but the point is true.
Which point? That it does not matter what the routine
does in a false (runnable) precondition? Of course not, it
should never be executed (which is my point, and
DbC's correct behavior)!
The point in particular is that evaluation of correctness is not a
program's objective. Otherwise, it would make no sense to talk about
correctness. Correctness is an invariant of *all* possible program states.
It is not a function of states.
Post by Miguel Oliveira e Silva
When using DbC we implement routines assuming
that its precondition and its class invariant holds
(or else, we would be doing defensive programming).
We most certainly won't be worry to provide a
specific behavior in that implementation for those
cases (just because, we are ensured that such
mistakes are caught by assertions).
A false precondition is an incorrect behavior of the
*program* (due to the client's failure).
Here you are talking about a *different* program. To evaluate:

1. correct (client)
2. correct (callee)
3. correct (client + callee)

Now, when the precondition of callee is false, then 1 is false and 3 is
false. But 2 is true! That's the whole point. When 3 is evaluated to true,
no caller can be incorrect and no precondition can be false. You need not
to check what you know for sure.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
Components are bound to pre/post/invariant conditions.
The behaviour is : pre IMPLIES X
1. When pre is satisifed, X = (post AND invariant)
2. When pre is not satisfied, X = ??
Then X can be any.
Of course. It does not matter, the program is *incorrect*,
hence it should - as much as possible - behave accordantly
(using the exception mechanism, which exits for this very
reason).
It would be meaningless. DbC *requires* the most weak preconditions. So
anything doable is already done. If not, then you have a design problem!
DbC can be effective only when used properly. If you suspect that a
precondition p might be false in *any* of program states, then p is a wrong
precondition and you have a wrong contract. It is meaningless to reason
about program correctness if contracts are wrong. It is like discussing the
sex of the tortoise supporting the Earth. (:-))
Post by Miguel Oliveira e Silva
Please remember that preconditions are not part of the
routine's implementation, they belong to its interface,
so it is not acceptable to allow its behavior (of the
preconditions) to ignore a false runnable assertion.
No. As I said before, program correctness does not depend on any run-time
assertions. So, it is meaningless to check anything at run-time. The thing
is constant.

A trivial proof shows that checking program correctness by a program is
infeasible:

pre : true

procedure p is
begin
while not correct (p) loop
put ("I'm so bad!");
end loop;
end p;

post : Halt (p)

Is p correct? If yes, then it violates its postcondition (loops), so it
isn't. But then the postcondition is true and thus p is correct.

q.e.d.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
And hope X != physical damage of any kind.
= Correctness is worth of nothing if preconditions aren't satisfied.
Of course, the program is *incorrect*.
No. Correct() is a predicate to evaluate. When it evaluates to true, on a
[sub]program, and it does, then the [sub]program is correct, per
definition.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
The program was incorrect (or else - by definition - it would
have worked).
This is an informal notion of correctness. Its subject is not the program,
but the system as a whole. That system was incorrect and exploded. Now to
analyse and prevent such mournful cases, one should investigate *what* was
incorrect there. It was not the "callee" (program), it was not its
counterpart (Ariane V hardware.) It was the integrator who brought these
pieces together ignoring the contracts of these components.
Post by Miguel Oliveira e Silva
Anyway, previously in this thread, I was simply stating
that the only acceptable behavior in a program when
an assertion is evaluated to a false value, is to raise
an exception (even within a non-disciplined exception
mechanism as is the case of Java, Ada or C++); and
that this behavior is an integral part of DbC.
I strongly object. Any behavior is acceptable in the case when contract
assertion fails. Otherwise, it isn't assertion of the contract, but an
ordinary if-statement.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Dmitry A. Kazakov
2006-02-15 20:12:10 UTC
Permalink
Post by Dmitry A. Kazakov
pre : true
procedure p is
begin
while not correct (p) loop
Should be:

while correct (p) loop
Post by Dmitry A. Kazakov
put ("I'm so bad!");
end loop;
end p;
post : Halt (p)
Actually it is even simpler:

pre : true

function p return Boolean is
begin
return correct (p);
end p;

post : not result

p returns true if correct and false if incorrect.

-----------
Ergo: mixing the object [program language] and the meta [contract language]
languages is asking for troubles.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Miguel Oliveira e Silva
2006-02-16 11:20:03 UTC
Permalink
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.
Yes, but the point is true.
Which point? That it does not matter what the routine
does in a false (runnable) precondition? Of course not, it
should never be executed (which is my point, and
DbC's correct behavior)!
The point in particular is that evaluation of correctness is not a
program's objective.
The primary objective of a programmer is to construct a formally
correct program. If one has tools - either within the programming language
itself, or in an intermediary stage before execution time - to statically
prove the correctness of part of the contract (such as, for example,
to ensure that no message is sent to a Void/NULL entity), excellent.
We won't need to be concerned with those cases at run-time, and
assertions aiming that goal can be safely deactivated in run-time.

However, such a desirable goal is *impossible* to attain for *most*
parts of a contract. Hence one - at least for the time being - is
bound to accept that such programming errors might occur at
run-time; hence appropriate programming techniques - which
are part of *DbC* (why do you keep insisting they are not?) - should
me taken to make sure that incorrect programs are - as much as
possible - catched and dealt with.

(See my point?)
Post by Dmitry A. Kazakov
Otherwise, it would make no sense to talk about
correctness. Correctness is an invariant of *all* possible program states.
It is not a function of states.
There is the theoretical goal of formal total correctness and
the practical tool of assertions. The latter, generally, express
necessary conditions for the former. Hence if the later is
proved to be wrong (a unique runtime case is enough)
then so is the former.

So one of the program's objectives (to use your terminology),
can and should be (even more when is being developed) to
ensure that no runnable assertion is false, and to take
appropriate measures if such an error occurs (DbC aimed
also to this goal).

(I'm running out of words! I feel I already said the same
thing too much times.)
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
When using DbC we implement routines assuming
that its precondition and its class invariant holds
(or else, we would be doing defensive programming).
We most certainly won't be worry to provide a
specific behavior in that implementation for those
cases (just because, we are ensured that such
mistakes are caught by assertions).
A false precondition is an incorrect behavior of the
*program* (due to the client's failure).
Here you are talking about a *different* program.
No I'm not. Such as a unique incorrect prediction is
sufficient to prove a scientific theory to be *wrong*,
so is a unique runtime false assertion sufficient
to prove the program to be incorrect.
Post by Dmitry A. Kazakov
1. correct (client)
2. correct (callee)
3. correct (client + callee)
Now, when the precondition of callee is false,
(Just a small correction.)

The precondition does not belong to the callee,
it belongs to the unit (it is part of its contract
to the outside world). The callee is "only" obliged
to meet that condition.
Post by Dmitry A. Kazakov
then 1 is false and 3 is
false. But 2 is true! That's the whole point.
The whole point (in my part) is that when an assertion fails the
program is incorrect (period). It is absurd to think of correctness
(or incorrectness) of a unit simply because a precondition is
false (it has absolutely no practical value). I already wrote
quite a few times, that it is irrelevant what the implementation
of a routine does when a precondition is false! The point
is that such execution should never (ever) occur (when
there is possibility to prevent such a disastrous event).
Post by Dmitry A. Kazakov
When 3 is evaluated to true,
no caller can be incorrect and no precondition can be false. You need not
to check what you know for sure.
Of course.

What about the "99%" remaining assertions that you
are unable to prove statically its correctness? (which
was the ones I have been mostly talking along).
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
Components are bound to pre/post/invariant conditions.
The behaviour is : pre IMPLIES X
1. When pre is satisifed, X = (post AND invariant)
2. When pre is not satisfied, X = ??
Then X can be any.
Of course. It does not matter, the program is *incorrect*,
hence it should - as much as possible - behave accordantly
(using the exception mechanism, which exits for this very
reason).
It would be meaningless. DbC *requires* the most weak preconditions.
Meaningless?

You mean it does not matter what an *incorrect* program does?

DbC - by definition - requires that, in a correct program, all of its
assertions are true.
Post by Dmitry A. Kazakov
So anything doable is already done. If not, then you have a design problem!
Yep. We definitely have a design problem when a program is incorrect.
Post by Dmitry A. Kazakov
DbC can be effective only when used properly.
My whole point.
Post by Dmitry A. Kazakov
If you suspect that a
precondition p might be false in *any* of program states, then p is a wrong
precondition and you have a wrong contract.
The more usual case (aimed to by DbC) is a false precondition,
not due to a incorrect contract, by resulting from a contract
failure (by the client). => program error
Post by Dmitry A. Kazakov
It is meaningless to reason
about program correctness if contracts are wrong.
It is not quite meaningless. The problem there is that
the correctness conditions expressed within the program
cease to be necessary conditions for the intended
formal program correctness.

Nevertheless, obviously I agree that contracts
should be constructed with care, to ensure they
express correctly the class's ADT semantics.

But when contracts are right, even if incomplete,
(which are - by far - the more frequent cases) it is
quite meaningful to talk about program incorrectness
(if any one of them fails).
Post by Dmitry A. Kazakov
It is like discussing the
sex of the tortoise supporting the Earth. (:-))
(Or the other turtle underneath it...)
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Please remember that preconditions are not part of the
routine's implementation, they belong to its interface,
so it is not acceptable to allow its behavior (of the
preconditions) to ignore a false runnable assertion.
No. As I said before, program correctness does not depend on any run-time
assertions.
Precisely my point. So in order for a program to be correct
all of its assertions are required to be verified. If not, the
program is incorrect.
Post by Dmitry A. Kazakov
So, it is meaningless to check anything at run-time.
Only the things you can prove statically to be formally
correct (hardly total program correctness).
Post by Dmitry A. Kazakov
The thing is constant.
If the program is correct in a sequential world it is irrelevant
whether you test or not test assertions (I've already said that
quite a few times).

The problem is how should DbC behave when the program
is not correct (such as when an assertion is false)!
Post by Dmitry A. Kazakov
A trivial proof shows that checking program correctness by a program is
You are the one with that problem (not me).

A trivial proof shows that (correct) assertions are a necessary
condition for program correctness. Hence if any one of
them is false the program is incorrect (recall my analogy
to Popper's falsifiability criteria in physical sciencies).
Post by Dmitry A. Kazakov
(...)
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
And hope X != physical damage of any kind.
= Correctness is worth of nothing if preconditions aren't satisfied.
Of course, the program is *incorrect*.
No.
Yes (considering its assertions).
Post by Dmitry A. Kazakov
Correct() is a predicate to evaluate. When it evaluates to true, on a
[sub]program, and it does, then the [sub]program is correct, per
definition.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Mentioned in this thread Ariane V was an excellent example of a correct
program that made a physical damage because a precondition [use of Ariane
IV hardware] was violated due to mismanagement.
The program was incorrect (or else - by definition - it would
have worked).
This is an informal notion of correctness.
Is it? Do you mean there a formal notion of correctness
in which the program may not work as intended?

In DbC correctness rules are quite simple: All of
its assertions are required to be true in the program
points where they are expressed.
Post by Dmitry A. Kazakov
Its subject is not the program, but the system as a whole.
If the cause of failure was inside the program, then the program
was incorrect (period).
Post by Dmitry A. Kazakov
That system was incorrect and exploded. Now to
analyse and prevent such mournful cases, one should investigate *what* was
incorrect there. It was not the "callee" (program), it was not its
counterpart (Ariane V hardware.) It was the integrator who brought these
pieces together ignoring the contracts of these components.
Post by Miguel Oliveira e Silva
Anyway, previously in this thread, I was simply stating
that the only acceptable behavior in a program when
an assertion is evaluated to a false value, is to raise
an exception (even within a non-disciplined exception
mechanism as is the case of Java, Ada or C++); and
that this behavior is an integral part of DbC.
I strongly object.
Then you are not talking of DbC (please go at its source).
Post by Dmitry A. Kazakov
Any behavior is acceptable in the case when contract
assertion fails.
Including an exploding rocket? A nuclear plant meltdown?

It seems to me that you are a little bit lost within theoretical
formal stuff. For the n'th time, when a program is proved
to be incorrect at runtime, the only behavior acceptable
is to react immediately and exceptionally to the detected
mistake: either to allow the construction of a robust fault
tolerant system (in which is of the utmost importance
a clear identification of the correct point of failure, and
to ensure that its usable objects are in stable states), or to
graciously terminate execution blaming the part of the
program responsible for the mistake.
Post by Dmitry A. Kazakov
Otherwise, it isn't assertion of the contract, but an
ordinary if-statement.
[Runtime] Assertions are required to be linked to
the exception mechanism, not to conditional
instructions (that is also my point).
Post by Dmitry A. Kazakov
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
-miguel

--
Miguel Oliveira e Silva
Dmitry A. Kazakov
2006-02-16 14:25:03 UTC
Permalink
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.
Yes, but the point is true.
Which point? That it does not matter what the routine
does in a false (runnable) precondition? Of course not, it
should never be executed (which is my point, and
DbC's correct behavior)!
The point in particular is that evaluation of correctness is not a
program's objective.
The primary objective of a programmer is to construct a formally
correct program. If one has tools - either within the programming language
itself, or in an intermediary stage before execution time - to statically
prove the correctness of part of the contract (such as, for example,
to ensure that no message is sent to a Void/NULL entity), excellent.
We won't need to be concerned with those cases at run-time, and
assertions aiming that goal can be safely deactivated in run-time.
So far OK.
Post by Miguel Oliveira e Silva
However, such a desirable goal is *impossible* to attain for *most*
parts of a contract.
You are shifting the subject. It is quite possible to make program behavior
independent on whether assertions are evaluated at run-time or not.
Post by Miguel Oliveira e Silva
Hence one - at least for the time being - is
bound to accept that such programming errors might occur at
run-time;
Programming errors do *not* occur at run time! They occur before. At
run-time occur *faults*.
Post by Miguel Oliveira e Silva
hence appropriate programming techniques - which
are part of *DbC* (why do you keep insisting they are not?) - should
me taken to make sure that incorrect programs are - as much as
possible - catched and dealt with.
(See my point?)
Yes, and it is a wrong point. The source of misunderstanding is in the
sloppy language obscuring otherwise obvious thing: anything checked at
run-time could be *in* a contract, but cannot be *the* contract itself.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Otherwise, it would make no sense to talk about
correctness. Correctness is an invariant of *all* possible program states.
It is not a function of states.
There is the theoretical goal of formal total correctness and
the practical tool of assertions. The latter, generally, express
necessary conditions for the former. Hence if the later is
proved to be wrong (a unique runtime case is enough)
then so is the former.
So one of the program's objectives (to use your terminology),
can and should be (even more when is being developed) to
ensure that no runnable assertion is false, and to take
appropriate measures if such an error occurs (DbC aimed
also to this goal).
That is all OK, except that these assertions don't assert whether the
program is correct. They check if the program is in a definite state. Note,
a state. That state might be undesirable for whatever reason, but it is a
legal [=known, predicted, planned, handled, exceptional, alarming, fault,
disastrous] state. Correctness is not a state of a program. The same
program cannot be correct in one state and incorrect in another. Isn't it
obvious? [See the proof I've posted before.]
Post by Miguel Oliveira e Silva
(I'm running out of words! I feel I already said the same
thing too much times.)
Try to formulate it formally, and you will see the problem.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
When using DbC we implement routines assuming
that its precondition and its class invariant holds
(or else, we would be doing defensive programming).
We most certainly won't be worry to provide a
specific behavior in that implementation for those
cases (just because, we are ensured that such
mistakes are caught by assertions).
A false precondition is an incorrect behavior of the
*program* (due to the client's failure).
Here you are talking about a *different* program.
No I'm not. Such as a unique incorrect prediction is
sufficient to prove a scientific theory to be *wrong*,
so is a unique runtime false assertion sufficient
to prove the program to be incorrect.
Again proving correctness isn't an objective of the program. It might be
one of a *different* program. That could be compiler, debugger, the code
reader's brain. But if you don't plan a manned Mars mission, one day you
have to leave the reader on the Earth.

OK, step by step:

1. You have p that does X.
2. You have assertions q about correct (p)
3. What about correct (p+q), which does X + checks correct (p)?

You are keep on talking about p. All others in this thread do about p+q!

Note that from very practical and sane point of view, p is of no interest,
because it is p+q, which in the end runs on the computer. See the point?
correct (p+q) is not checked at run-time! If you turn q off, then it will
be a different program: p with correct (p) unchecked. This or that way, but
nothing in a program checks its correctness.
Post by Miguel Oliveira e Silva
What about the "99%" remaining assertions that you
are unable to prove statically its correctness? (which
was the ones I have been mostly talking along).
Then I place them *in* the contract. If I cannot rely on some part of
precondition, I remove it from there and move into behavior. That's the
whole point!

Example:

pre : x is Real & x >= 0
function Sqrt (x : Real) return Real;
post : result = sqrt (x)

is replaced by

pre : x is Real
function Sqrt (x : Real) return Real;
post : (x >= 0 & result = sqrt (x)) V (x < 0 & Constraint_Error)

The code in Sqrt

if x < 0 then
raise Constraint_Error;
end if;

is *not* a contract assertion!
Post by Miguel Oliveira e Silva
You mean it does not matter what an *incorrect* program does?
Yes. You can say absolutely nothing about an incorrect program.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
It is like discussing the
sex of the tortoise supporting the Earth. (:-))
(Or the other turtle underneath it...)
Or the color of the eggs they lay in the course of this connection...
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
No. As I said before, program correctness does not depend on any run-time
assertions.
Precisely my point. So in order for a program to be correct
all of its assertions are required to be verified. If not, the
program is incorrect.
Wrong, whether correct(p) is evaluated or not, does not make it true or
false!
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
The thing is constant.
If the program is correct in a sequential world it is irrelevant
whether you test or not test assertions (I've already said that
quite a few times).
True, but contradicts to what you said before.
Post by Miguel Oliveira e Silva
The problem is how should DbC behave when the program
is not correct (such as when an assertion is false)!
I don't see any problem here. All incorrect programs behave as expected =
incorrectly. Wrong [as a part of *any*] doing is an expected [correct]
behavior of an incorrect program.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
A trivial proof shows that checking program correctness by a program is
You are the one with that problem (not me).
What can be said about an inconsistent theory? Answer: same as about
behavior of an incorrect program...
Post by Miguel Oliveira e Silva
If the cause of failure was inside the program, then the program
was incorrect (period).
Come on! How you define "the cause is inside?" (:-))
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Any behavior is acceptable in the case when contract
assertion fails.
Including an exploding rocket? A nuclear plant meltdown?
In *any* case! Under the condition that turtles supporting the Earth are
laying yellow eggs, a nuclear plant has full right to explode.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Miguel Oliveira e Silva
2006-02-16 16:08:49 UTC
Permalink
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by S Perryman
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is, a precondition specifically states that there *is
no* correct behavior in certain situations.
This is incorrect.
Yes, but the point is true.
Which point? That it does not matter what the routine
does in a false (runnable) precondition? Of course not, it
should never be executed (which is my point, and
DbC's correct behavior)!
The point in particular is that evaluation of correctness is not a
program's objective.
The primary objective of a programmer is to construct a formally
correct program. If one has tools - either within the programming language
itself, or in an intermediary stage before execution time - to statically
prove the correctness of part of the contract (such as, for example,
to ensure that no message is sent to a Void/NULL entity), excellent.
We won't need to be concerned with those cases at run-time, and
assertions aiming that goal can be safely deactivated in run-time.
So far OK.
Post by Miguel Oliveira e Silva
However, such a desirable goal is *impossible* to attain for *most*
parts of a contract.
You are shifting the subject.
(No I'm not.)
Post by Dmitry A. Kazakov
It is quite possible to make program behavior
independent on whether assertions are evaluated at run-time or not.
That's the idea. Normal program behavior should be totally
independent of assertions (meaning that it is correct considering
those assertions).
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Hence one - at least for the time being - is
bound to accept that such programming errors might occur at
run-time;
Programming errors do *not* occur at run time! They occur before. At
run-time occur *faults*.
You are correct. Programming errors are the (main) cause of runtime failures.
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
hence appropriate programming techniques - which
are part of *DbC* (why do you keep insisting they are not?) - should
me taken to make sure that incorrect programs are - as much as
possible - catched and dealt with.
(See my point?)
Yes, and it is a wrong point. The source of misunderstanding is in the
sloppy language obscuring otherwise obvious thing: anything checked at
run-time could be *in* a contract, but cannot be *the* contract itself.
How can you assert that it is a wrong point, if - in this respect - you
are saying basically the same thing as I am?

Runtime assertions are *part of* the contract (necessary
conditions), not necessarily *the* whole contract (necessary
and sufficient conditions).
Some parts of a contract can be handled statically (through
a static type system and eventually a formal tool
able to prove their correctness); others can be approached
at runtime (through runnable assertions); and there might be
even others that cannot be handled in neither of those worlds.

One of the most powerful ideas behind DbC is exactly to
bring ADT semantics to inside the program (look at the
references).
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Otherwise, it would make no sense to talk about
correctness. Correctness is an invariant of *all* possible program states.
It is not a function of states.
There is the theoretical goal of formal total correctness and
the practical tool of assertions. The latter, generally, express
necessary conditions for the former. Hence if the later is
proved to be wrong (a unique runtime case is enough)
then so is the former.
So one of the program's objectives (to use your terminology),
can and should be (even more when is being developed) to
ensure that no runnable assertion is false, and to take
appropriate measures if such an error occurs (DbC aimed
also to this goal).
That is all OK, except that these assertions don't assert whether the
program is correct.
For n'th(+1) time: They assert - when executed - that the program
is not incorrect regarding whatever the condition they assert in the
context of the call.
Post by Dmitry A. Kazakov
They check if the program is in a definite state. Note,
a state. That state might be undesirable for whatever reason, but it is a
legal [=known, predicted, planned, handled, exceptional, alarming, fault,
disastrous] state. Correctness is not a state of a program. The same
program cannot be correct in one state and incorrect in another. Isn't it
obvious? [See the proof I've posted before.]
Quite obvious. (I have already answered that.)
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
(I'm running out of words! I feel I already said the same
thing too much times.)
Try to formulate it formally, and you will see the problem.
A false assertion implies an incorrect program.

Incorrect programs are required to be corrected
as soon as possible.

DbC is a tool aiming (also) that goal.
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
When using DbC we implement routines assuming
that its precondition and its class invariant holds
(or else, we would be doing defensive programming).
We most certainly won't be worry to provide a
specific behavior in that implementation for those
cases (just because, we are ensured that such
mistakes are caught by assertions).
A false precondition is an incorrect behavior of the
*program* (due to the client's failure).
Here you are talking about a *different* program.
No I'm not. Such as a unique incorrect prediction is
sufficient to prove a scientific theory to be *wrong*,
so is a unique runtime false assertion sufficient
to prove the program to be incorrect.
Again proving correctness isn't an objective of the program.
Its (primary) objective is to do what is expected and to
do it correctly!
Post by Dmitry A. Kazakov
It might be one of a *different* program.
(The one talking of a different thing other than
DbC is you.)

DbC allows contracts (not *the* complete formal
totally correct contract, but necessary conditions
towars it) to be *part of* the program.
Post by Dmitry A. Kazakov
That could be compiler, debugger, the code
reader's brain. But if you don't plan a manned Mars mission, one day you
have to leave the reader on the Earth.
1. You have p that does X.
2. You have assertions q about correct (p)
3. What about correct (p+q), which does X + checks correct (p)?
You are keep on talking about p. All others in this thread do about p+q!
I'm talking about DbC (which is the subject of this thread).

Not imagining that a correct knowledge of this methodology
was not widely known, I merely corrected Daniel when he
implied that all behaviors are acceptable - in DbC - when
a preconditions is false. This is wrong. If such fault
is detected at runtime - in DbC - an exception is required
to be raised (no need to put that in the contract, because
in DbC that *is part* of the semantic of runnable
assertions).
Post by Dmitry A. Kazakov
Note that from very practical and sane point of view, p is of no interest,
because it is p+q, which in the end runs on the computer. See the point?
correct (p+q) is not checked at run-time! If you turn q off, then it will
be a different program: p with correct (p) unchecked. This or that way, but
nothing in a program checks its correctness.
Dmitry, we are talking about DbC. Not of the theoretical problem
of proving the total correctness of a program.

So please look at the original references of DbC, so that
we can talk of the same things.
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
What about the "99%" remaining assertions that you
are unable to prove statically its correctness? (which
was the ones I have been mostly talking along).
Then I place them *in* the contract. If I cannot rely on some part of
precondition, I remove it from there and move into behavior. That's the
whole point!
pre : x is Real & x >= 0
function Sqrt (x : Real) return Real;
post : result = sqrt (x)
is replaced by
pre : x is Real
function Sqrt (x : Real) return Real;
post : (x >= 0 & result = sqrt (x)) V (x < 0 & Constraint_Error)
This is not DbC, this is defensive programming.

You are learning DbC from the wrong sources.
Post by Dmitry A. Kazakov
The code in Sqrt
if x < 0 then
raise Constraint_Error;
end if;
is *not* a contract assertion!
You are not talking about DbC.
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
You mean it does not matter what an *incorrect* program does?
Yes. You can say absolutely nothing about an incorrect program.
Except... perhaps... that...well... it is incorrect!

(Hence required immediate and precise corrective measures.)
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
It is like discussing the
sex of the tortoise supporting the Earth. (:-))
(Or the other turtle underneath it...)
Or the color of the eggs they lay in the course of this connection...
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
No. As I said before, program correctness does not depend on any run-time
assertions.
Precisely my point. So in order for a program to be correct
all of its assertions are required to be verified. If not, the
program is incorrect.
Wrong, whether correct(p) is evaluated or not, does not make it true or
false!
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
The thing is constant.
If the program is correct in a sequential world it is irrelevant
whether you test or not test assertions (I've already said that
quite a few times).
True, but contradicts to what you said before.
It does not! Just try to make a little efford to *understand*
what I'm saying (and *again* look at the original references
of DbC).
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
The problem is how should DbC behave when the program
is not correct (such as when an assertion is false)!
I don't see any problem here. All incorrect programs behave as expected =
incorrectly. Wrong [as a part of *any*] doing is an expected [correct]
behavior of an incorrect program.
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
A trivial proof shows that checking program correctness by a program is
You are the one with that problem (not me).
What can be said about an inconsistent theory?
And which one is that?
Post by Dmitry A. Kazakov
Answer: same as about behavior of an incorrect program...
Post by Miguel Oliveira e Silva
If the cause of failure was inside the program, then the program
was incorrect (period).
Come on! How you define "the cause is inside?" (:-))
double x,y;
x = -1;
y = sqrt(x);

Tell me where is the outside cause of failure?
(Other than - of course - the obvious programming
error.)

The programming error is easily detected at runtime
and (who would say?) the assertion responsible for it
is runnable and can exist inside the program itself
(surely - taking your words against my arguments -
there must exist an inconsistency laying somewhere...
afterall I did not prove the total correctness of
the program, did I?).
Post by Dmitry A. Kazakov
Post by Miguel Oliveira e Silva
Post by Dmitry A. Kazakov
Any behavior is acceptable in the case when contract
assertion fails.
Including an exploding rocket? A nuclear plant meltdown?
In *any* case! Under the condition that turtles supporting the Earth are
laying yellow eggs, a nuclear plant has full right to explode.
Sorry. We not arguing anymore. DbC is a well defined methodology
proposed in the 80's by Bertrand Meyer. You don't seem to know
exactly what it is. I can advise you some reading if that will help
you to understand what I'm saying, and what DbC is. I'm sure
that from all my previous messages with little effort you can
understand me without misinterpretations. I'm interested in
explaining what is DbC (and what is not), you seem interested in
discussing the problem of theoretical proofing of programs.
It is a very interesting problem. I have high hopes that in the
future it may became possible to bring program contracts
as much as possible to that area, but DbC is not merely that.
It is a design, documentation, testing, debugging and
fault tolerant programming technique.
Post by Dmitry A. Kazakov
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Best regards,

-miguel

--
Miguel Oliveira e Silva
Miguel Oliveira e Silva
2006-02-15 16:09:47 UTC
Permalink
Post by Daniel T.
Post by Miguel Oliveira e Silva
What Daniel and you are saying (in the small part in which
we disagree) is that it may not be important the behavior of
a routine when a (runnable) precondition is false.
However that goes against one of the main goals of DbC: to
ensure that the program does not behave incorrectly (which is not,
in real software, exactly the same as to behave correctly).
Do you see the inherent contradiction in the above?
No.

(Perhaps the way I constructed the phrase was not the best.)
Post by Daniel T.
How can a function
behave incorrectly in a situation for which no behavior has has been
defined?
In that situation it can not. But it is you who is saying that
there is no program behavior defined on false (runnable)
assertions, not me.

What is your point?

(I was hoping that my opinion was clear enough, but I guess it is not.)

Let me try again.

[In a sequential world] If a program is correct - considering all its runnable
assertions - then it doesn't matter if the assertions are tested or not (we
agree here). However, if it is not correct (or simply if there is such a possibility),
then it can make all the difference in the world how the program reacts
to a false assertion. DbC - as originally defined - imposes the behavior
that an exception is to be raised is such cases, hence it is *not allowed*
for an incorrect program to normally proceed its execution.

So a *necessary* condition for a "program not to behave
incorrectly" is to allow it to proceed its normal execution
if (and only if) no (runnable) assertion fails. That does not mean
that the program is 100% correct, only that it is correct considering
the assertions executed in the context in which they were executed.
Post by Daniel T.
We can only insure the behavior is incorrect *if* we know what the
correct behavior is,
Of course.
Post by Daniel T.
a precondition specifically states that there *is
no* correct behavior in certain situations.
A false (runnable) precondition states that we are in the
presence of an incorrect program behavior (requiring a
corrective action), from which should always result
the exceptional program behavior of raising an exception.

In a similar way as to Karl Popper's falsifiability criteria
to distinguish science from pseudo-"science", (runnable)
assertions are (most of the times) unable to ensure total
correctness (usually, they are only necessary conditions).
However, they are quite capable to ensure when some
incorrect behaviors do exist. So, as in science, when using
assertions we are in fact - most of the time - searching and
excluding incorrect behaviors, and in that way we are
approximating a correct behavior.

So, a clear program semantics - through the exception
mechanism (as in DbC) - in the presence of false runnable
assertions, is as important as the experimentation phase
within physical sciences (a unique wrong prediction is
suficient to prove the theory to be false).

(In programming errors should never be taken lightly.)
Post by Daniel T.
Post by Miguel Oliveira e Silva
So DbC is a tool for constructing not "just" correct software,
but also reliable (correct *and* robust) software
[Meyer, OOSC2ed chapters 11 and 12]. To allow
a routine to proceed "normally" in the presence of a false
(runnable) assertion would be just like the primitive C use
of function return values, or global variables as 'errno',
for signaling program errors
Your comparison is way off. The C use of return values and global
variables for error conditions are *defined* behaviors.
(Runnable assertions also have a well defined behavior: an exception
is raised when they are false.)
Post by Daniel T.
We can test to
ensure they happen because we know what is supposed to happen given
certain input. Preconditions are nothing of the sort.
A false precondition ensures us that we are in the presence
of an incorrect behavior (whereas a true precondition is - in
general - only a necessary condition for the ultimate goal
of total correctness).

Exceptions ensure that no such errors are ignored, requiring an
explicit action from the part of the program responsible for it.
Post by Daniel T.
Post by Miguel Oliveira e Silva
Post by Oliver Wong
So the method does NOT check the precondition: it just assumes that the
pre-condition holds, and it is not defined what will happen if the
pre-condition doesn't hold.
(That's playing Russian roulette with your program.)
No, that's proper distribution of responsibility. If it isn't my
function's responsibility to ensure x > 0, why on earth would I have
code in my function checking the value of x?
You don't. DbC *is not* defensive programming.

The precondition does that job for you.
Post by Daniel T.
The responsible party should be doing that.
Of course. The (runnable) precondition only ensures that
the program is only allowed to proceed normally if that
responsible part really does that (or else an exception
is raised).
Post by Daniel T.
As soon as you define what the function does if the precondition isn't
met, you *take responsibility* for the error.
Who is "you"? If by "you" we mean the client of the
function then yes, you are correct, it is its responsibility
to only call the function ensuring the precondition.
Post by Daniel T.
If your function doesn't
throw, then it's *your* fault, not the clients
A false precondition (in a sequential world) is always the
responsibility of the client.
Post by Daniel T.
because *you said* that
your function would throw in that situation.
DbC says that an exception is to be throwed
whenever exists a false runnable assertion
(no other behavior - except the primitive
C's "assert" behavior - is acceptable).

For some reason (one of it might be the fact
that English is not my birth language), we are
not communicating correctly with each other.

Take a deep breath, and read more carefully
my messages. I'm quite sure that you'll see that
the ideas they convey are quite clear and
without contradictions. I'm also quite sure
they also express Meyer's view of DbC
(just take a look at OOSC1ed/2ed).
Post by Daniel T.
--
Magic depends on tradition and belief. It does not welcome observation,
nor does it profit by experiment. On the other hand, science is based
on experience; it is open to correction by observation and experiment.
Best regards,

-miguel

--
Miguel Oliveira e Silva
S Perryman
2006-02-15 08:48:21 UTC
Permalink
Post by Oliver Wong
Imagine, for example, a binary search method. It might have as a
pre-condition that the array passed in is sorted in ascending order, and
then will return true or false depending on whether a given member is
present in the array. It also guarantees O(log(n)) runtime performance. If
the method had to actually *CHECK* the condition that the array was
sorted, the method would be impossible to implement, as it would need at
least O(n) running time, to scan through the whole array and verify that
it is sorted.
1. The binary search method should *not* be doing the check.
That is the responsibility of the pre-condition.

2. As DBC allows conditions to be turned on/off, the binary search is never
performance-hindered by the pre-condition (ie becomes O(n + log n) ) .


Regards,
Steven Perryman
Robert C. Martin
2006-03-14 04:59:12 UTC
Permalink
On Sun, 12 Feb 2006 20:23:21 +0000, Miguel Oliveira e Silva
Post by Miguel Oliveira e Silva
In unit testing it does not makes sense to test
the unit with something that is not its
responsibility (it would be like test a car with
a blind "driver").
True. On the other hand it *does* make sense to test the contract. If
a method is going to throw an exception when the precondition fails,
then the precondition should be unit-tested.


-----
Robert C. Martin (Uncle Bob) | email: ***@objectmentor.com
Object Mentor Inc. | blog: www.butunclebob.com
The Agile Transition Experts | web: www.objectmentor.com
800-338-6716


"The aim of science is not to open the door to infinite wisdom,
but to set a limit to infinite error."
-- Bertolt Brecht, Life of Galileo
Oliver Wong
2006-03-14 15:05:46 UTC
Permalink
Post by Robert C. Martin
On Sun, 12 Feb 2006 20:23:21 +0000, Miguel Oliveira e Silva
Post by Miguel Oliveira e Silva
In unit testing it does not makes sense to test
the unit with something that is not its
responsibility (it would be like test a car with
a blind "driver").
True. On the other hand it *does* make sense to test the contract. If
a method is going to throw an exception when the precondition fails,
then the precondition should be unit-tested.
Miguel claims that there is "one true" definition for design by
contract, and in it, precondition checking may be disabled. So it is not
nescessarily true that when preconditions fails, an exception will be
thrown.

- Oliver

H. S. Lahman
2006-02-12 15:16:26 UTC
Permalink
Responding to Sasa...
Post by Sasa
I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
I agree with Daniel T. One tests to what the conditions allow, not what
they don't allow. OTOH, it is a good idea to provide assertions, at
least in development mode, to ensure that the software isn't allowing
things it shouldn't. IOW, the DbC assertions on the conditions /are/
correctness tests.


*************
There is nothing wrong with me that could
not be cured by a capful of Drano.

H. S. Lahman
***@pathfindermda.com
Pathfinder Solutions -- Put MDA to Work
http://www.pathfindermda.com
blog: http://pathfinderpeople.blogs.com/hslahman
(888)OOA-PATH
Phlip
2006-02-12 15:57:34 UTC
Permalink
Post by Sasa
Hello,
I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
Consider Test-Driven Development tests, where you write a test case that
fails before writing code to pass. One might think you must write test
cases to force DBC assertions to exist.

Use TDD to generate lines of behavioral code. Also write assertions, and
just expect them not to fail. Failure is terminal, and the assertions will
experience many test runs, in many permutations.
--
Phlip
http://www.greencheese.org/ZeekLand <-- NOT a blog!!!
S Perryman
2006-02-14 11:30:45 UTC
Permalink
I am interested in your opinion regarding unit testing of DBC. I.e. should
one test preconditions of a method (by writing tests which violate those
preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
For DBC, normal operation is :

1. Conform to the pre-conditions
2. The supplier component executes such that the post-conditions hold.

On the above basis, what does "fails appropriately" actually mean ??
For DBC, failure to conform to 1 means that 2 is undefined.

How do we test for something that has no definition ??
So IMHO the answer is no.

Testing whether the pre-conditions actually trigger is another story.

This depends on whether your DBC scheme is auto-generated (Eiffel etc) or
hand-coded. For the latter, it is probably worth doing (assuming you have a
more flexible DBC scheme than the std 'program terminate on condition
failure' etc) .


Regards,
Steven Perryman
Robert C. Martin
2006-03-14 04:55:22 UTC
Permalink
Post by Sasa
Hello,
I am interested in your opinion regarding unit testing of DBC. I.e.
should one test preconditions of a method (by writing tests which
violate those preconditions and verify that method fails appropriately)?
Personally I would say no, but I am interested in opinion and arguments
for both ways - testing and not testing DBC.
You only have to test the things you want to work. Anything else can
remain untested.

-----
Robert C. Martin (Uncle Bob) | email: ***@objectmentor.com
Object Mentor Inc. | blog: www.butunclebob.com
The Agile Transition Experts | web: www.objectmentor.com
800-338-6716


"The aim of science is not to open the door to infinite wisdom,
but to set a limit to infinite error."
-- Bertolt Brecht, Life of Galileo
Continue reading on narkive:
Loading...