forked from dlang/dlang.org
-
Notifications
You must be signed in to change notification settings - Fork 0
/
cppcontracts.dd
500 lines (413 loc) · 10.1 KB
/
cppcontracts.dd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
Ddoc
$(COMMUNITY D's Contract Programming vs C++'s,
$(P Many people have written me saying that D's Contract Programming
does not add anything that C++ does not already support.
They go on to illustrate their point with a technique for doing Contracts in
C++.)
$(P It makes sense to review what Contract Programming is, how it is done in D,
and stack that up with what each of the various C++ Contract techniques
can do.)
$(P Digital Mars C++ adds
<a href="http://digitalmars.com/ctg/contract.html">extensions to C++</a>
to support Contracts, but they are not covered here because they are not
part of standard C++ and are not supported by any other C++ compiler.)
$(H2 Contract Programming in D)
This is more fully documented in the D
<a href="contracts.html">Contract Programming</a> document.
To sum up, Contract Programming in D has the following characteristics:
$(OL
$(LI The $(I assert) is the basic contract.
)
$(LI When an assert contract fails, it throws an exception.
Such exceptions can be caught and handled, or allowed to
terminate the program.
)
$(LI Classes can have $(I class invariants) which are
checked upon entry and exit of each public class member function,
the exit of each constructor, and the entry of the destructor.
)
$(LI Assert contracts on object references check the class
invariant for that object.
)
$(LI Class invariants are inherited, that means that a derived
class invariant will implicitly call the base class invariant.
)
$(LI Functions can have $(I preconditions) and $(I postconditions).
)
$(LI For member functions in a class inheritance hierarchy, the
precondition of a derived class function are OR'd together
with the preconditions of all the functions it overrides.
The postconditions are AND'd together.
)
$(LI By throwing a compiler switch, Contracts code can be enabled
or can be withdrawn from the compiled code.
)
$(LI Code works semantically the same with or without Contracts
checking enabled.
)
)
$(H2 Contract Programming in C++)
$(H3 The $(D assert) Macro)
$(P C++ does have the basic $(D assert) macro, which tests its argument
and if it fails, aborts the program. $(D assert) can be turned
on and off with the $(D NDEBUG) macro.)
$(P $(D assert) does not know anything about class invariants,
and does not throw an exception when it fails. It just aborts
the program after writing a message. $(D assert) relies on
a macro text preprocessor to work.)
$(P $(D assert) is where explicit support for Contracts in Standard C++
begins and ends.)
$(H3 Class Invariants)
Consider a class invariant in D:
----------
class A
{
$(CODE_HIGHLIGHT invariant)() { ...contracts... }
this() { ... } // constructor
~this() { ... } // destructor
void foo() { ... } // public member function
}
class B : A
{
$(CODE_HIGHLIGHT invariant)() { ...contracts... }
...
}
----------
To accomplish the equivalent in C++ (thanks to Bob Bell for providing
this):
$(CCODE
template<typename T>
inline void check_invariant(T& iX)
{
#ifdef DBC
iX.invariant();
#endif
}
// A.h:
class A {
public:
#ifdef DBG
virtual void invariant() { ...contracts... }
#endif
void foo();
};
// A.cpp:
void A::foo()
{
check_invariant(*this);
...
check_invariant(*this);
}
// B.h:
#include "A.h"
class B : public A {
public:
#ifdef DBG
virtual void invariant()
{ ...contracts...
A::invariant();
}
#endif
void bar();
};
// B.cpp:
void B::barG()
{
check_invariant(*this);
...
check_invariant(*this);
}
)
There's an additional complication with $(D A::foo()). Upon every
normal exit from the function, the $(D invariant()) should be
called.
This means that code that looks like:
$(CCODE
int A::foo()
{
...
if (...)
return bar();
return 3;
}
)
would need to be written as:
$(CCODE
int A::foo()
{
int result;
check_invariant(*this);
...
if (...)
{
result = bar();
check_invariant(*this);
return result;
}
check_invariant(*this);
return 3;
}
)
Or recode the function so it has a single exit point.
One possibility to mitigate this is to use RAII techniques:
$(CCODE
int A::foo()
{
#if DBC
struct Sentry {
Sentry(A& iA) : mA(iA) { check_invariants(iA); }
~Sentry() { check_invariants(mA); }
A& mA;
} sentry(*this);
#endif
...
if (...)
return bar();
return 3;
}
)
The #if DBC is still there because some compilers may not
optimize the whole thing away if check_invariants compiles to nothing.
$(H2 Preconditions and Postconditions)
Consider the following in D:
----------
void foo()
in { ...preconditions... }
out { ...postconditions... }
body
{
...implementation...
}
----------
This is nicely handled in C++ with the nested Sentry struct:
$(CCODE
void foo()
{
struct Sentry
{
Sentry() { ...preconditions... }
~Sentry() { ...postconditions... }
} sentry;
...implementation...
}
)
$(P If the preconditions and postconditions consist of nothing
more than $(D assert) macros, the whole doesn't need to
be wrapped in a $(D #ifdef) pair, since a good C++ compiler will
optimize the whole thing away if the $(D assert)s are turned off.)
$(P But suppose $(D foo()) sorts an array, and the postcondition needs
to walk the array and verify that it really is sorted. Now
the shebang needs to be wrapped in $(D #ifdef):)
$(CCODE
void foo()
{
#ifdef DBC
struct Sentry
{
Sentry() { ...preconditions... }
~Sentry() { ...postconditions... }
} sentry;
#endif
...implementation...
}
)
$(P (One can make use of the C++ rule that templates are only
instantiated when used can be used to avoid the $(D #ifdef), by
putting the conditions into a template function referenced
by the $(D assert).))
$(P Let's add a return value to $(D foo()) that needs to be checked in
the postconditions. In D:)
----------
int foo()
in { ...preconditions... }
out (result) { ...postconditions... }
body
{
...implementation...
if (...)
return bar();
return 3;
}
----------
In C++:
$(CCODE
int foo()
{
#ifdef DBC
struct Sentry
{
int result;
Sentry() { ...preconditions... }
~Sentry() { ...postconditions... }
} sentry;
#endif
...implementation...
if (...)
{
int i = bar();
#ifdef DBC
sentry.result = i;
#endif
return i;
}
#ifdef DBC
sentry.result = 3;
#endif
return 3;
}
)
Now add a couple parameters to $(D foo()). In D:
----------
int foo(int a, int b)
in { ...preconditions... }
out (result) { ...postconditions... }
body
{
...implementation...
if (...)
return bar();
return 3;
}
----------
In C++:
$(CCODE
int foo(int a, int b)
{
#ifdef DBC
struct Sentry
{
int a, b;
int result;
Sentry(int a, int b)
{
this->a = a;
this->b = b;
...preconditions...
}
~Sentry() { ...postconditions... }
} sentry(a, b);
#endif
...implementation...
if (...)
{
int i = bar();
#ifdef DBC
sentry.result = i;
#endif
return i;
}
#ifdef DBC
sentry.result = 3;
#endif
return 3;
}
)
$(H2 Preconditions and Postconditions for Member Functions)
Consider the use of preconditions and postconditions for a
polymorphic function in D:
----------
class A
{
void foo()
in { ...Apreconditions... }
out { ...Apostconditions... }
body
{
...implementation...
}
}
class B : A
{
void foo()
in { ...Bpreconditions... }
out { ...Bpostconditions... }
body
{
...implementation...
}
}
----------
The semantics for a call to $(D B.foo()) are:
$(UL
$(LI Either Apreconditions or Bpreconditions must be satisfied.)
$(LI Both Apostconditions and Bpostconditions must be satisfied.)
)
Let's get this to work in C++:
$(CCODE
class A
{
protected:
#if DBC
int foo_preconditions() { ...Apreconditions... }
void foo_postconditions() { ...Apostconditions... }
#else
int foo_preconditions() { return 1; }
void foo_postconditions() { }
#endif
void foo_internal()
{
...implementation...
}
public:
virtual void foo()
{
foo_preconditions();
foo_internal();
foo_postconditions();
}
};
class B : A
{
protected:
#if DBC
int foo_preconditions() { ...Bpreconditions... }
void foo_postconditions() { ...Bpostconditions... }
#else
int foo_preconditions() { return 1; }
void foo_postconditions() { }
#endif
void foo_internal()
{
...implementation...
}
public:
virtual void foo()
{
assert(foo_preconditions() || A::foo_preconditions());
foo_internal();
A::foo_postconditions();
foo_postconditions();
}
};
)
Something interesting has happened here. The preconditions can
no longer be done using $(D assert), since the results need
to be OR'd together. I'll leave as a reader exercise adding
in a class invariant, function return values for $(D foo()),
and parameters
for $(D foo()).
$(H2 Conclusion)
$(P These C++ techniques can work up to a point. But, aside from
$(D assert), they are not standardized and so will vary from
project to project. Furthermore, they require much tedious
adhesion to a particular convention, and add significant clutter
to the code. Perhaps that's why it's rarely seen in practice.)
$(P By adding support for Contracts into the language, D offers an easy
way to use Contracts and get it right. Being in the language standardizes
the way it will be used from project to project.)
$(H2 References)
$(P Chapter C.11 introduces the theory and rationale of
Contract Programming in
<a href="http://www.amazon.com/exec/obidos/ASIN/0136291554/classicempire">
Object-Oriented Software Construction
</a><br>
Bertrand Meyer, Prentice Hall)
$(P Chapters 24.3.7.1 to 24.3.7.3 discuss Contract Programming in C++ in
<a href="http://www.amazon.com/exec/obidos/ASIN/0201700735/classicempire">
The C++ Programming Language Special Edition
</a><br>
Bjarne Stroustrup, Addison-Wesley)
)
Macros:
TITLE=D's Contract Programming vs C++'s
WIKI=CppDbc