Last update March 7, 2008

Doc Comments /
DBC



Contract Programming    

Table of contents of this page
Contract Programming   
Comments   
Unimplemented Feature   
Errors/Exceptions   
square_root example   
Suggested Example   
No support for "old" in postconditions   
Broken link   
Links   

Comments    

Put your comments here.

Unimplemented Feature    

Inheritance of in/out contracts in an unimplemented feature ( Issue:302).

Errors/Exceptions    

Currently there are no InException, OutException or InvariantException in Phobos. Just AssertError...

square_root example    

In the square_root example for DBC, what is funny is that the out clause will assert quite a lot: the x and result are of type long, so it means each time the parameter x is not a 'perfect square', assert((result * result) == x) will fail. A very good example!

The sample code is obsolete and won't compile with ver 0.102. Casts are needed, and math.sqrt is now std.math.sqrt

body
{
  return cast(long)std.math.sqrt(cast(double)x);
}

Suggested Example    

Suggestion for another example for a one-based lookup table. Zero is not a valid index to lookup table, and return value must be in certain range.

ushort GetMaxChapInBook(in ushort bk)
in   { assert((bk >= 1) && (bk <= 9)); }
out (result) { assert((result >= 1) && (result <= 50)); }

body {
  ushort maxChap = chapsInBook[bk];
  return maxChap;
}

ushort[] chapsInBook = [
  0,  50, 40, 27, 36, 34, 24, 21,  4, 31     // 0-9
];

No support for "old" in postconditions    

Unfortunately D lacks Eiffel's "old" or any equivalent mechanism for the postcondition ("out") statements to refer to the original value which "this" had at the start of the function call.

Full Design By Contract includes a way to compare the object's values at the start and end of the function invocation, which is often necessary in order to define what the function does to the object. ( http://archive.eiffel.com/doc/manuals/technology/contract/ gives further discussion of this element of DBC.)

Thus something like

void insertFoo(Foo f)
out
{
    assert(numberOfFoos == old(numberOfFoos) + 1);
}
is apparently not easily possible to represent in D without support from the language/compiler itself. (The notation old(numberOfFoos) would mean the value of numberOfFoos at entry to the function insertFoo, as the equivalent notation in Eiffel does.)

Broken link    

The link to Adding Contracts to Java should be http://jan.netcomp.monash.edu.au/java/contracts/paper-long.html.

Links    


FrontPage | News | TestPage | MessageBoard | Search | Contributors | Folders | Index | Help | Preferences | Edit

Edit text of this page (date of last change: March 7, 2008 15:36 (diff))