Design by Contract != Runtime Assertion
Walter Bright
newshound2 at digitalmars.com
Mon Nov 22 15:16:29 PST 2010
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.
More information about the Digitalmars-d
mailing list