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

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

 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

 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

 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.


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.

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

 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.



weakened). 

on 
polymorphic dbc completely.



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



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




weakened).
 It missed half of what dbc is all about with polymorphism.



see only the good sides of it. I don't know why they have taken those
decisions. Maybe to allow the static verifiability.







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.






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.





 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.







 

 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 


Frankly, because of contract inheritance, you cannot implement dbc without 
language changes.






 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.



 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.


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:





 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.



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

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

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



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

static verifiability they accept only pure functions, recursion is not allowed,
and so on.


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:
 




 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.


 

 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 

 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

 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



 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

 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

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.




 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

 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