www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Design by Contract != Runtime Assertion

reply %u <mehrdad nospamm.com> writes:
Hello!

I just became an incredibly big fan of D; it has everything I've wanted,
except one thing:
It is said that D supports Design by Contract (DbC) programming, when in fact
what it has is runtime assertions. There is, however, a big difference. DbC
necessarily means that a compiler would have a theorem prover and would need
to prove at /Compile/-time whether or not an expression can be satisfied
(similar to what is done in the Spec# language by Microsoft Research), because
the name is /Design/ by contract. It is not the same as assertions, which
occur at run time.
I was wondering if actual design-by-contract programming (rather than mere
assertions) will be available in D at a later time?

Thank you!
Nov 21 2010
next sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 11/22/10 12:46 AM, %u wrote:
 Hello!

 I just became an incredibly big fan of D; it has everything I've wanted,
 except one thing:
 It is said that D supports Design by Contract (DbC) programming, when in fact
 what it has is runtime assertions. There is, however, a big difference. DbC
 necessarily means that a compiler would have a theorem prover and would need
 to prove at /Compile/-time whether or not an expression can be satisfied
 (similar to what is done in the Spec# language by Microsoft Research), because
 the name is /Design/ by contract. It is not the same as assertions, which
 occur at run time.
 I was wondering if actual design-by-contract programming (rather than mere
 assertions) will be available in D at a later time?

 Thank you!

Contracts based on theorem proving postdate contract programming as defined by Meyer by a long time, and are in fact a fairly new and active research topic. It would be a misrepresentation to equate theorem proving with contracts. You may want to consult TDPL for a related discussion. D currently defines contract programming in keeping with Meyer's definition. There are no plans to integrate static theorem proving abilities with contracts. Andrei
Nov 21 2010
prev sibling next sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
On Sunday 21 November 2010 22:46:38 %u wrote:
 Hello!
 
 I just became an incredibly big fan of D; it has everything I've wanted,
 except one thing:
 It is said that D supports Design by Contract (DbC) programming, when in
 fact what it has is runtime assertions. There is, however, a big
 difference. DbC necessarily means that a compiler would have a theorem
 prover and would need to prove at /Compile/-time whether or not an
 expression can be satisfied (similar to what is done in the Spec# language
 by Microsoft Research), because the name is /Design/ by contract. It is
 not the same as assertions, which occur at run time.
 I was wondering if actual design-by-contract programming (rather than mere
 assertions) will be available in D at a later time?
 
 Thank you!

As I recall, all design by contract says is that a function has a contract saying that if you give it input which follows a certain set of guidelines, it will give you output which follows a certain set of guidelines. It says nothing about enforcement or proving that a function actually follows the contract. If you violate the contract by giving it bad data, then it's implementation-defined as to what happens. And obviously, if the function doesn't follow the contract, then it's implementation-defined as to what happens. What D does is give you a means of making sure that a function is following the contract that you intended for it. pre-conditions verify that it's given arguments which follow the contract, post-conditions verify that the function's output follows the contract, and invariants help guarantee that the state of an object is within _its_ contract. All of it is a way to verify that the contracts are kept. All DbC says is that the contracts exist. How you guarantee that they're followed is another matter entirely. And having pre-conditions and post- conditions verified programmatically at runtime is a classic way to do that. Actually doing proofs of any sort - programmatically or otherwise - can be very difficult, and there's no way that that sort of thing is going to make it into the language. It's totally unnecessary, it would be an absolute nightmare to implement, and now you have another source of potential error: your proof. By verify that the contract is followed at runtime, D has implemented the _least_ error-prone solution to guaranteeing that function contracts are adhered to. - Jonathan m Davis
Nov 21 2010
prev sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
%u:

 It is said that D supports Design by Contract (DbC) programming, when in fact
 what it has is runtime assertions. There is, however, a big difference. DbC
 necessarily means that a compiler would have a theorem prover and would need
 to prove at /Compile/-time whether or not an expression can be satisfied
 (similar to what is done in the Spec# language by Microsoft Research), because
 the name is /Design/ by contract. It is not the same as assertions, which
 occur at run time.

From what I have read of DbC it is acceptable to call it DbC even if the enforcements are done at run time. Having the tests done at compile time as in Spec# and Spark is a nice thing, but it requires a constraint solver inside the compiler, that Walter doesn't seem interested in (and it probably requires a more rigid way of writing code).
 I was wondering if actual design-by-contract programming (rather than mere
 assertions) will be available in D at a later time?

If D becomes widespread, then sooner or later someone will surely try to write an external constraint solver to try to verify the assertions at compile time. But the style normal D contracts are written doesn't lead to a simple analysis. In Spec# and Eiffel and Spark they use specific constructs inside contracts, that look more like math, they help static verifiers. I have uncovered and reported here this problem some weeks ago, but it was ignored. People aren't seeing it as problem yet, it's an invisible problem still. So so far there is really no interest even in making the job of static D verifiers easer. Bye, bearophile
Nov 22 2010
parent reply Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 But the style normal D contracts are written doesn't lead to a simple
 analysis. In Spec# and Eiffel and Spark they use specific constructs inside
 contracts, that look more like math,

look more like math???
 they help static verifiers. I have
 uncovered and reported here this problem some weeks ago, but it was ignored.
 People aren't seeing it as problem yet, it's an invisible problem still. So
 so far there is really no interest even in making the job of static D
 verifiers easer.

Spec# does not do proper inheritance of preconditions (they cannot be weakened). It missed half of what dbc is all about with polymorphism. C# missed the boat on polymorphic dbc completely. Spec# generates code for and checks its contracts at runtime. And lastly, please demonstrate how: requires a == b; is checkable with a static verifier and: assert(a == b); is not, and how: static assert(a == b); is not. Because I cannot figure out where you uncovered a problem.
Nov 22 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Walter:

 look more like math???

Right. In Spec# (and similar things are present in Eiffel, Spark and a DbC for Java) you write things like: invariant 0 <= n && n <= a.Length; invariant forall{int i in (n: a.Length); a[i] != key}; ensures result == exists{int x in a; x == key}; return exists{int x in a; x == key}; requires forall{int i in (0:a.Length), int j in (i:a.Length); a[i]<=a[j]}; ensures 1 <= result && result < a.Length; ensures 0 <= result ==> a[result] == key; ensures result == -1 ==> forall{int i in (0: a.Length); a[i] != key}; invariant forall{int i in (0: a.Length), i < low || high <= i; b[i] == a[a.Length1i]}; To me those lines look more like math formulas than normal D code. This is useful because the contract code needs to be as much bug-free as possible, otherwise the contracts don't help. The short syntax helps the eye see that the code is correct, and having a declarative style this probably helps the analyser too. In D you need loops, sets, and other things there, that I think are less easy to analyse (because it is possible to analyse them, because commercial Lints for C are probably able to do it).
 Spec# does not do proper inheritance of preconditions (they cannot be
weakened).
 It missed half of what dbc is all about with polymorphism.

It seems you and me are both blind: you see only the downsides of Spec# and I see only the good sides of it. I don't know why they have taken those decisions. Maybe to allow the static verifiability.
 C# missed the boat on polymorphic dbc completely.

They have decided that it's better to not change the C# language to add DbC to it, so they have implemented DbC as a library only (but it contains a simplified static analyser too), so I think they have had constraints.
 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.
 And lastly, please demonstrate how:
 ...
 is not. Because I cannot figure out where you uncovered a problem.

You are right, in simple cases it's the same thing. Maybe for a good enough static analyser it's the same thing for more complex cases too, that contains nested loops, etc. Thank you, bye, bearophile
Nov 22 2010
next sibling parent bearophile <bearophileHUGS lycos.com> writes:
 Maybe for a good enough static analyser it's the same thing for more complex
cases too, that contains nested loops, etc.

But I dont' believe it. Bye, bearophile
Nov 22 2010
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 To me those lines look more like math formulas than normal D code.

This makes no sense to me. Programming languages *are* math. There is no "more like math".
 This is useful because the contract code needs to be as much bug-free as
 possible, otherwise the contracts don't help. The short syntax helps the eye
 see that the code is correct, and having a declarative style this probably
 helps the analyser too. In D you need loops, sets, and other things there,
 that I think are less easy to analyse (because it is possible to analyse
 them, because commercial Lints for C are probably able to do it).

Again, this makes no sense. Furthermore, as I've attempted to explain before, doing automated analysis on loops, etc., is well-trod and well-understood territory. It's 1970's technology.
 Spec# does not do proper inheritance of preconditions (they cannot be
 weakened). It missed half of what dbc is all about with polymorphism.

see only the good sides of it.

I suggest Meyer's epic tome "Object-Oriented Software Construction" for the rationale and theory behind dbc. Once you have, it's pretty obvious where these well-designed languages completely missed the boat on dbc. Every one of them (except Eiffel, of course) punted on contract inheritance, which is inexcusable in a language that is centered around polymorphism and inheritance. Dbc without contract inheritance is nothing more than an assert. NOTHING more.
 I don't know why they have taken those
 decisions. Maybe to allow the static verifiability.

Getting rid of polymorphic behavior to enhance static verifiability doesn't make much sense in an OOP language.
 C# missed the boat on polymorphic dbc completely.

They have decided that it's better to not change the C# language to add DbC to it, so they have implemented DbC as a library only (but it contains a simplified static analyser too), so I think they have had constraints.

I.e. they missed the boat. It is not dbc. (And Microsoft has exhibited no reluctance to add features to the C# language, so this makes no sense either.) Frankly, because of contract inheritance, you cannot implement dbc without language changes.
 Spec# generates code for and checks its contracts at runtime.

it tests the contracts at compile-time too where possible.

That's not what I read about it.
 And lastly, please demonstrate how: ... is not. Because I cannot figure out
 where you uncovered a problem.

static analyser it's the same thing for more complex cases too, that contains nested loops, etc.

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.
Nov 22 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Walter:

 Spec# generates code for and checks its contracts at runtime.

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
Nov 22 2010
parent reply Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 Walter:
 
 Spec# generates code for and checks its contracts at runtime.

But it tests the contracts at compile-time too where possible.


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.
Nov 22 2010
parent bearophile <bearophileHUGS lycos.com> writes:
Walter:

 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;
    }
 }

 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.

At the moment I have nothing more to add on this, thank you for your good answers. You and other people here have taught me tons of things :-) Bye, bearophile
Nov 22 2010