www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Why is there no static contract verification?

reply "Mario Schmidt" <jack_sabbath gmx.de> writes:

for a secondary, or even new main language that D might become.

One of the features that I found most promising in D is DbC. 
However, I was very disappointed when I realized that the current 
implementation is not much more than an assert that is evaluated 
during runtime.

What i mean is.. look at this code:

void goCrazy(Person p)
in { assert(p); }
body {
// whatever
}

void main()
{
Person goku = null;
goCrazy(goku);
}


This a rather simple example where the compiler would be 
perfectly able to realize that the procedure goCrazy won't be 
called according it's specified contracts.

I know that these contracts would help me to find bugs faster or 
better during testing. But if the compiler would do a static 
verification you could even be sure that a procedure will always 
be called correctly.

I'm sure in some cases it would indeed be possible to check 
certain conditions at compile time. This includes ins, outs and 
invariants.
Maybe a subset of checks could be implemented in D.. like range 
checking of numerical values or something..
Feb 02 2014
next sibling parent "bearophile" <bearophileHUGS lycos.com> writes:
Mario Schmidt:


 One of the features that I found most promising in D is DbC. 
 However, I was very disappointed when I realized that the 
 current implementation is not much more than an assert that is 
 evaluated during runtime.


Recently I have written something on a related topic:

Bye,
bearophile
Feb 02 2014
prev sibling next sibling parent "Jesse Phillips" <Jesse.K.Phillips+D gmail.com> writes:
On Sunday, 2 February 2014 at 18:37:34 UTC, Mario Schmidt wrote:


 for a secondary, or even new main language that D might become.

 One of the features that I found most promising in D is DbC. 
 However, I was very disappointed when I realized that the 
 current implementation is not much more than an assert that is 
 evaluated during runtime.

 What i mean is.. look at this code:

 void goCrazy(Person p)
 in { assert(p); }
 body {
 // whatever
 }

 void main()
 {
 Person goku = null;
 goCrazy(goku);
 }


The compiler may be able to identify simple cases, but reality is 
going to be a hit and miss. I think the goal here would be for 
goCrazy to take a NotNull!Person (but that implementation isn't 
finish).

On another note, in/out contracts don't appear to get much use in 
the community. I use them once in awhile, but don't feel I get 
much out of them.
Feb 02 2014
prev sibling parent "Daniel Murphy" <yebbliesnospam gmail.com> writes:
"Mario Schmidt"  wrote in message 
news:uftxdqcyjyermmthtwwt forum.dlang.org...


 This a rather simple example where the compiler would be perfectly able to 
 realize that the procedure goCrazy won't be called according it's 
 specified contracts.


Pull requests welcome.
Feb 02 2014