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.
