Design by Contract != Runtime Assertion

[bearophile]

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).


>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 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.


> As I've repeatedly said, loops are not a problem for data flow analysis. If a 
> static analyzer is having problems with loops, I suggest mailing them a book on 
> how to write compilers instead of blaming the language.

When I have seen those formulas that contain exists{...}, set operations (intersections, unions, etc), and so on expressed in a short declarative way I have thought that they are simpler for the formal analyzer. But if you say otherwise, then I believe you :-)

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.

Bye,
bearophile