Design by Contract != Runtime Assertion

[Walter Bright]

bearophile wrote:
> Walter:
> 
>>>> Spec# generates code for and checks its contracts at runtime.
>>> Right, because there are external libs that may not use contracts, etc.
>>> But it tests the contracts at compile-time too where possible.
>> That's not what I read about it.
> 
> If you go to the online site that allows you to test Spec#: 
> http://www.rise4fun.com/SpecSharp And you run the demo test, modify it as you
> like, copy&paste examples from this paper, and you modify the examples as you
> like: http://research.microsoft.com/en-us/um/people/leino/papers/krml189.pdf 
> you will able to see that that Spec# tests the contracts at compile time. On
> the rise4fun.com site you may also try its verifiers (like Boogie) directly.
> 
> The have chosen to leave the contracts at runtime too, despite they are
> verified at compile-time where possible (this means in most cases).

Most cases? I see it does some easy ones, but I'm skeptical it goes much beyond 
that. It fails on this one:

class Example {
   int x;

   void Inc(int y)
           ensures (x & 1) == 0;
   {
     x += x;
   }
}



>> Getting rid of polymorphic behavior to enhance static verifiability doesn't
>> make much sense in an OOP language.<
> 
> The krml189 paper says things like:
> 
>> Calls to virtual methods are dynamically bound. That is, the method
>> implementation to be executed is selected at run time based on the type of
>> the receiver object. Which implementation will be selected is in general
>> not known at compile (verification) time. Therefore, Spec# verifies a call
>> to a virtual method M against the specification of M in the static type of
>> the receiver and enforces that all overrides of M in subclasses live up to
>> that specification [16, 14].<
> 
> They have done this to allow static verifiability. They want static
> verifiability because Spec# is not a near-general-purpose language like D,
> Spec# is for places where bugs must be avoided in most situations (short time
> after designing Spec# they have created the Sing# language, that is a system
> language. I think this was their purpose from the beginning. They have tried
> to invent a language that allows to write a kernel in a much safer way). This
> requirement changes lot of things. In the Spark language, that is designed
> for situations where you allow an even lower bug count compared to Spec#, to
> allow static verifiability they accept only pure functions, recursion is not
> allowed, and so on.

This defeats the entire purpose of polymorphism. It doesn't make sense for Spec# 
to be a polymorphic language if they're going to defeat it like this. It shows a 
fundamental misunderstanding of polymorphism.

The article: "It may declare additional postconditions, but not additional
preconditions or modifies clauses because a stronger precondition or a more 
permissive modifies clause would come as a surprise to a caller of the 
superclass method." A surprise? Please read Meyer's book on this. That's the 
whole point of an override, to loosen the preconditions and tighten the 
postconditions. Otherwise, it isn't inheritance.


> This is also probably why Spec# has reintroduced the design of Java
> assertions. They are a wrong design in a general purpose language, because as
> you have recently shown me in two interesting pages, they end leading to less
> safe code, because normal programmers are lazy, and those exceptions give
> other kind of troubles. But people that write high integrity systems probably
> want to endure the pain of using that kind of exceptions, because those
> programmers don't leave any stone unturned, anyway.

I think this is a complete misunderstanding of what I wrote about asserts.


> Then they are better for the programmer only (just as Python list comps) to
> decrease bug counts and improve contracts readability. I hope you agree with
> me that keeping very short the code inside contracts is a good thing.

Whether they are more understandable or not has nothing to do with dbc.