Misleading contract syntax

[Norbert Nemec]

I think, this should be broken down into different issues:

* Is real-life code ever stable enough to take deactivate assertion checks?

I think that there is no simple yes/no question. The best solution would 
probably be to allow selectively deactivating assertions. It may indeed 
be advisable to leave the contract checks between library and 
application activated even when the software is shipped. Even within a 
library, it might make sense to group the assertions into different 
levels that one can activate or deactivate in groups.


* How do contracts fit in?

The interface of a library should fully define the legal set of input 
and output values. Of course, this is difficult to do formally for 
complex libraries, but if you like, you can always call "exceptions" a 
legal form of output. For many cases, these may even be the most 
convenient form. Think, e.g. about numerical instabilities that occur 
deep inside complex algorithms.

So, typically, contracts handle the simple cases that can be checked 
easily. Difficult inputs that cannot be checked easily, on the other 
hand, should simply be considered "legal" by the contract, triggering an 
exception, which also is a perfectly legal output.

Assertions, on the other hand, should never be used in that way. An 
assertion is about as informal as a comment. A broken assertion tells me 
that whoever wrote this "comment" obviously made an incorrect assumption 
and there must be a bug somewhere within the library. Possibly, the bug 
is in the library interface definition, which may need to tighten its 
contracts and thereby require changes in the application code, but 
still: a broken assertion is *always* a bug in the code that contains 
the assertion.


* How far can the library programmer trust the application programmer?

The library programmer does not need to trust anyone. It is the 
application programmer who is ultimately responsible that the program 
works as promised. So the application programmer has to decide whether 
he trusts himself enough to take out the contract checks.

In a user interface, there is effectively never the situation that the 
user is confident enough in his typing ability to take out security 
checks. That is why languages typically do not provide means to 
deactivate them.

In library interfaces, on the other hand, this state can be reached by 
careful coding and sufficient testing. Many project may never reach it 
due to their complexity, but some (parts of) software can certainly get 
there and switch off the checks at the interfaces in release mode.





bearophile wrote:
> Norbert Nemec:
> 
>> No! No! No! Design-by-contract means that it is the application's duty 
>> to make sure that argument values are correct. If the program is 
>> correct, the library can trust that the argument values are correct and 
>> does not need to do checks. This is exactly the same situation that 
>> assertions are for: Double-checking something to catch potential bugs.
> 
> Thinking some more about it, I refuse what you say, or I don't understand it still.
> 
> If your library is very simple, then your application can know what input the function/class wants, but as soon as the library code becomes a little more complex, there can be corner input cases that the calling code doesn't know about, that the library can refuse with a good exception error.
> 
> So generally the only piece of library code that knows (and needs to know) what are its correct inputs, is the library code itself. If you have to feed user interface inputs to some library code, you need to clean and test such inputs well. But if the library is not designed to perform tests for input data, then you need two pieces of code: the library code, plus another piece of code that knows everything about that library code itself, to test the inputs well. This is very bad design.
> 
> 
>> A library interface simply is something different than a user interface.<
> 
> I don't buy this. Complex enough different parts of the same program need "user interfaces" for each other, where the user is the programmer or another part of the program written by the programmer or another programmer. So libraries need to test all their inputs well anyway. I have programmed for enough years to be sure of this.
> So using preconditions based on asserts is not enough.
> 
> -------------------
> 
> Brad Roberts:
> 
>> Asserts in the body of a method have no impact on overridden implementations in subclasses, but in/out contracts do.  So there's a distinct value in using in/out for non-final methods.<
> 
> I like class/struct invariants, I like postconditions, I can probably appreciate loop invariants too. All of them test for code correctness, because they have to fire only if there's a bug in the program.
> 
> But I don't like preconditions done with asserts, because any part of the program can receive wrong inputs from any other part of the code. So in functions/methods of my programs I will keep using exceptions to test inputs.
> 
> So overridden implementations in subclasses will need to know what are their good inputs.
> 
> -------------------
> 
> Norbert Nemec:
> 
>> * A contract should *never* have side effects, otherwise debugging code may behave differently from release mode (which is the ultimate nightmare).<
> 
> I agree, but I have asked for something a little less strong, because I think it's enough and doesn't limit freedom too much:
> http://d.puremagic.com/issues/show_bug.cgi?id=3856
> 
> 
>> * Any reasonable example with contracts contains just a list of assertions.<
> 
> I don't agree. There are many situations where you want to perform more computations, for example if a function needs a sorted input, you need a loop (or a call to a Phobos function like isSorted) to test if it's actually sorted.
> 
> 
>> => Why are contracts defined as lists of statements in the first place?<
> 
> Probably because Walter follows the very good engineering advice of keeping things simple. The current design is probably the simpler thing for the compiler, and it's good enough. I don't think the syntax needs to be changed.
> 
> 
>> B.t.w: to a useful, addition (orthogonal to the above change) would be access to the original state of the class in the out contract, e.g.:<
> 
> I agree it's useful and I'd like to have it, but it seems it's not easy to design it well:
> http://www.digitalmars.com/d/archives/digitalmars/D/Communicating_between_in_and_out_contracts_98252.html
> 
> Bye,
> bearophile