Contracts vs debug

[Timon Gehr]

On 02/04/2012 06:18 PM, F i L wrote:
> Why/where should I use contracts vs debug statements? Is it completely
> arbitrary? If so, I wonder if contracts syntax is even needed:
>
> int foo(int bar)
> in
> {
> assert(bar != 0);
> }
> body
> {
> return bar + 1;
> }
>
> The thing I like more about debug statements, is that I can put them
> anywhere in my code, testing parameters and locals in the same way. If
> "for documentation" is the only argument for contracts, I find that a
> bit weak.
>
> int foo(int bar)
> {
> debug assert(bar != 0);
>
> return bar + 1;
> }
>
> That is much cleaner syntax and just as easy to understand from a
> assertion-failure/documentation standpoint IMO.

First of all, you don't really need the debug statements, assertions are 
stripped from -release'd code anyway.

The assertions in the function body are not part of the function 
interface. (eventually, contracts can be on function declarations 
lacking a function body) Conceptually, with an assert in the function 
body, the bug would be inside the function: If it is not assumed in the 
in-contract it cannot be asserted that bar is != 0. Some code could just 
go ahead and call foo(0). If the assertion is in the in-contract, foo(0) 
is invalid. And in the in-contract, this is supposed to be visible for 
everyone.

For a pragmatic reason, because contracts are supposed to be inherited 
(but due to a bug, in-contracts are not currently inherited without 
adding an in{assert(false);} contract to the overriding function, this 
bug does not break LSP though, it is just a little annoying)

Contracts can also be used for modular static model checking/static 
error detection.

You may want to have a look at the Eiffel and Spec# systems.