mirror of
https://github.com/boostorg/contract.git
synced 2026-01-24 05:42:16 +00:00
<pre>
Design By Contract (DBC) for C++ (DBC++) -- README
==================================================
The DBC++ library supports Design By Contract (DBC) [Mey97] for the C++
programming language [Str97].
Essentially, all Eiffel programming language DBC features are supported by
DBC++. Among others:
1) "old" prefix in postconditions;
2) Subcontracting;
3) Optional contract compilation;
4) Full integration with Doxygen.
NOTE: Most of the documentation still needs to be added. For now, you can
take a look at the examples to see how the DBC++ library works.
AUTHOR: Lorenzo Caminiti, 2009 (lorenzo_caminiti@hotmail.com)
LICENCE: The DBC++ library is distributed under the LGPL licence.
http://sourceforge.net/projects/dbcpp/
1. VERSION
----------
The current DBC++ version is v0.1 (development).
This version is still an early development version and the library could change
quite a bit even in its APIs. Furthermore, validation, debugging, and testing
is happing now. If you see an issue with this library, your are welcome to
report it; but expect to see issues with this early version.
2. EXAMPLES (GETTING STARTED)
-----------------------------
To compile the examples run `make' in the "example" directory, the binaries
will be created in the "example/build" directory.
Examples are mainly taken from [Mey97] and [Mit02]. Start by looking at:
a) "example/OO_SW_Construction/Stack4" for a good general example on how to
write contracts.
b) "example/DBC_by_Example/Courier" for an example on how to write
subcontracts for inherited classes.
c) "Other/Simple" for a real basic example of how to use DBC++ without its
macro APIs (only if you are interested in exploring how the library
actually works, otherwise just use the macro APIs).
3. FEATURES
-----------
This is a list of DBC features and how they are supported by DBC++.
DBC FEATURE DBC++ SUPPORT
Class invariants Yes
Contracts for member functions Yes
Contracts for constructors Yes(2)
Contracts for destructor Yes(3)
"old" and "result" in postconditions Yes(5)
Contracts of overloaded member functions Yes(4)
Contracts for derived class (subcontracting) Yes
Contracts for templates class Yes
Contracts for pure virtual member functions Yes
Contracts for template member functions Yes(1)
Contracts for member operators Yes(1)
Loop invariants Yes
Optional compilation of contracts Yes
Automatic contract documentation (Doxygen) Yes(7)
Limited access in contracts No(6)
Concurrency (multi-threading) Not yet (work in progress)
(1) This is only supported by DBC++ code APIs and not by the macro APIs.
(2) If your constructor implementation uses member initializer syntax to
initialize member variable, the constructor implementation needs to be in the
header file (not in the .cpp). Usually constructor implementations are short
enough that can be put in the header file so this is not an issue. However, a
possible way around this is to delegate the constructor implementation to a
*private* init() member function then write the contract for init() and not for
the constructor. Using a "two stage" construction via init() has its drawbacks
(see [Str97]) so the general reccomandation is to implement the constructors
in .hpp when using DBC++ unless you were already using "two stage" construction
regardless of DBC++ (for example to implement delegating constructors.
(3) This feature is implemented as specified in [C++04] (there is no direct
indication on how DBC should be supported for destructors in [Mey97]).
(4) A limitation is that the overloaded function must use different argument
names (not just argument types). For example, DBC++ will supports contracts for
"C::f(const dobule& d)" and "C::f(const int& i)" because they use differnt
argument names, "d" and "i", when overloading "f". However, DBC++ will not be
able to support contracts for "C::f(const dobule& x)" and "C::f(const int& x)"
because both overloaded member functions use the samebargument name "x". This
is not an important limitation, just use different argument names.
(5) In postconditions, "result" refers to the returned value -- there is no
"result" in contracts for "void" member functions. Also, entities (the object,
named "self", and the arguments) are accessed via: their name ".now", to get
their value now after the function body has been executed; or their name
".old", to get their value before the body was executed. E.g., "self.now"
refers to the object after the function body execution, "self.old" refers to
the object before the body execution. The entity is internally copied by DBC++
before the body execution -- be careful, if the entity copy constructor only
provides a shallow copy then ".old" might not be what you intended. Because not
all entities can be copied in C++ (copy constructor can be made private for non-
copiable objects), you must explicitly indicate to DBC++ that an entity type
"E" is copiable (has a public copy constructor) using "dbc::copiable<E>". This
will allow you to apply ".old" to such entity. By default entities types are
considered non-copiable as being copiable adds an extra requirement on the type
that might not be satisfied by all types (especially if the type is a template
parameter, it might later be set to a non-copiable type). Therefore the
copiability is explicitly required and only when ".old" is needed in your
contract. Furthermore, the copy constrcutor might have performance impact. For
example, if an argument is passed by value or as constant reference, you can
safely use ".now" as the body execution will not have been able to change the
argument value.
(6) In Eiffel, only public features can be called in preconditions -- because
the client of the class should correctly be able to check the contract before
invoking an operation, see [Mey97]. However, DBC++ is not able to restrict
member function or variable access in contracts. Precoditions, postconditions,
and invariant can access public, protected, and private parts of the object. It
is strongly recommended you write contracts that use public members as much as
possible, especially in preconditions -- see good motivations and practices for
this in [Mey97] and [Mit02]. Furthermore, in contracts you can only access
entities as constant references "const&" so you cannot change them. This is
critical as contracts must not alter the state of the object, the operation
argument, or result -- do not mess things up using "const_cast\<\>()". Finally,
you can write any form of C++ code in DBC++ contracts but limit yourself in
writing a list of assertions -- if you write complex code in contracts, you
will likely introduce code bugs in the contract itself instead of writing
assertions to check that there is no bug in the rest of your software.
(7) The documentation generated by Doxygen will essentially look like the
class' "short form" and "flat-short from" defined in [Mey97].
4. APIs
-------
DBC++ provides a macro based APIs. However, you can also write DBC++ contracts
without using such macro APIs.
Pros (+) and cons (-) of macro APIs:
(+) Macro APIs hide all the contract setup framework so you only write the
preconditions, postconditions, and invariants (as it should be).
(+) Macro APIs automatically generate Doxygen documentation for the contracts
you write.
(-) You will have to "trust" the macro APIs without really understanding how
the DBC++ works behind the scene -- most of the times this should be OK.
(-) The macro APIs generate a compilation warning for 'g++' as friend class
declarations are repeated more than one time -- you can just ignore this
warning (this is a very minor cons).
The following is a summary of the macro APIs to write DBC++ contracts. Refer to
the code in the "example" directory to see how these APIs are used.
Class invariant.
DBC_INVARIANT(full_class_type, invariant_code)
Constructor.
DBC_CONSTRUCTORn(access, class_type,
[arg1_type, arg1, arg2_type, arg2, ...],
require_code, ensure_code, body_code)
Constructor of template class.
DBC_TEMPLATE_CONTRUCTORn(/* same as above */)
Destructor.
DBC_DESTRUCTOR(access, virtual_mem_fun], class_type, body_code)
Non-void member function.
DBC_MEM_FUNn(access, virtual_mem_fun, return_type, class_type,
mem_fun, [arg1_type, arg1, arg2_type, arg2, ...], const_mem_fun,
require_code, ensure_code, body_code)
Void member function.
DBC_MEM_VOIDFUNn(/* same as above */)
Non-void member function of template class.
DBC_TEMPLATE_MEM_FUNn(/* same as above */
Void member function of template class.
DBC_TEMPLATE_MEM_VOIDFUNn(/* same as above */)
Derived non-void member function.
DBC_DERIVED_MEM_FUNn(access, virtual_mem_fun, return_type, class_type,
mem_fun, [arg1_type, arg1, arg2_type, arg2, ...], const_mem_fun,
base_class_type, /* new argument */
require_code, ensure_code, body_code)
Derived void member function.
DBC_DERIVED_MEM_VOIDFUNn(/* same as above */)
Derived non-void member function of template class.
DBC_DERIVED_TEMPLATE_MEM_FUNn(/* same as above */
Derived void member function of template class.
DBC_DERIVED_TEMPLATE_MEM_VOIDFUNn(/* same as above */)
Member function name for implementation in .cpp file.
DBC_BODY(mem_fun)
Parameters:
"n" postfix Number of arguments. For example, for a constructor
with 2 arguments, use the 'DBC_CONSTRUCTOR2()' macro. The
current limits for n are [0, 3]. It is trivial to increase
this limit and later versions of DBC++ will be extended to
support at least n in [0, 10] -- 10 arguments.
access Access keyword 'public', 'protected', or 'private'.
virtual_mem_fun Keyword 'virtual' if virtual member function. Leave empty
otherwise.
return_type Return type name. 'void' if void member function.
class_type Class type name (do not specify namespace, template
parameters, etc, just class type name itself).
full_class_type Fully qualified class type name (with namespace prefix,
template parameters postfix*, etc).
mem_fun Member function name.
argI_type Type of argument I-th, for I in [1, n] (not there if n=0).
argI Name of argument I-th, for I in [1, n] (not there if n=0).
const_mem_fun Keyword 'const' if constant member function. Leave empty
otherwise.
base_class_type Type name of base class from which to inherit contract (for
subcontracting only).
require_code Preconditions code block "{ ... }".
ensure_code Postconditions code block "{ ... }".
body_code Member function implementation code block "{ ... }". Use
";" if implementation will instead appear in .cpp file. Use
" = 0;" for pure virtual member functions.
invariant_code Class-invariants code block "{ ... }".
(*) The C++ preprocessor cannot parse templates with more than 1 parameter as a
valid macro parameter. Therefore, if your class is a template with more
than 1 argument, say 'my_namespace::my_class<T1, T2>', you must pass it via
an addional macro definition:
#define _MY_CLASS_TYPE my_namesoace::my_class<T1, T2>
DBC_INVARIANT(_MY_CLASS_TYPE, { /* your invariant assertions */ })
5. ASSERTION
------------
There are two assertion classes to support writing assertion in preconditions,
postconditions, and class invariant code blocks: 'dbc::assertion' and
'dbc::oassertionstream'.
These macros allow to check assertions using the two assertion classes.
DBC_ASSERT(condition, label)
DBC_ASSERT_STREAM(condition, label, stream_label_code)
Parameters:
condition Assertion boolean condition. An exception will the thrown if
this condition is false.
label C-style string to name the assertion. This label is part of the
Doxygen documentation.
stream_label_code Provides a verbose description of the assertion
condition possibly with variables value, etc (for assertion
stream only). The DBC_ASSERT_STREAM declares a local variable
'astream' of type 'dbc::oassertstream'. This label code can be
of the form 'astream << "result " << result << " must be true"'
to write in the assertion stream a description of the assertion
that is more verbose of its "label". This will provide more
information in case the assertion fails. (This code is only
executed in case the condition if false or on verbose DBC++ log
level to avoid evaluating expensive I/O under normal
circumstances.) If this code ends with "<< dbc::raise<E>()"
then an instance of the exception type E is thrown in case of
condition violation. You can use this to throw your own
exceptions instead of the default ones thrown by DBC++ (
'dbc::precondition_violation', 'dbc::postcondition_violation',
and 'dbc::invariant_violation'). The default exceptions thrown
by DBC++ are derived from 'std::logic_error'. The custom
exception E you can throw using '<< dbc::raise<E>()' must have
a constructor accepting a C-style null-terminated string that
will be set by DBC++ to the assertion stream label.
6. CONTRACTS IN HEADER FILES
----------------------------
Contracts are written in the header file (.hpp) together with the code
specification (declaration). Implementation (definition) of the class can either
go in the header file of in the code file (.cpp).
It is strongly recommended to put the implementation in the .cpp file so it is
separate from the specifications -- see [Str97]. Contracts are part of the
specifications so they correctly appear in the header file.
(Templates are usually a known exception to this rule in C++ as in most cases
their implementation will have to leave in the header file -- this depends on
you compiler and build system -- but you can still split the template
specification at the top of the header file, and its implementation at bottom.)
7. COMPILATION OPTIONS
----------------------
A few macro symbols are used to control when contracts are compiled in the
object code, what parts of the contract' assertions are checked at run-time,
and to configure other DBC++ behaviours.
DBC++ will use default #definition of the following symbols unless you #define
them *before* the 1st #inclusion of the "dbc.hpp" header file. To make sure you
#define these symbols before each #inclusion, it is recommended you #include
"dbc.hpp" in one header only, say "mydbc.hpp", and have any other file of your
system include this one header. (Another option would be to #define these
symbols using your build system.)
-- File: mydbc.hpp --
// #define DBC configuration symbols as needed.
#include <dbc.hpp> // Single place that actually #includes "dbc.hpp"
-- File: myprogram1.cpp --
#include "mydbc.hpp"
// Your code...
-- File: myprogram1.cpp --
#include "mydbc.hpp"
// Your code...
The following macro symbols control optional contract compilation and run-time
checking (this is similar to what supported by Eiffel [Mey97]).
MACRO SYMBOL ACTION IF #DEFINED
DBC_NO All symbols below are #undefined.
DBC Do not compile (and do not check) any DBC++ code.
Any DBC++ contract code will be *completely*
stripped out of your object code.
DBC_CHECK_REQUIRE Compile and check preconditions.
DBC_CHECK_ENSURE Compile and check postconditions.
DBC_CHECK_INVARIANT Compile and check class invariants.
DBC_CHECK_LOOP Compile and check loop invariants.
DBC_ALL All symbols above are #defined.
By #defining some of these symbols when generating object code from one class
and a #defining a different set of symbols when compiling a different class,
you can compile and check different contract parts for different components of
your system (this will complicate a bit your build system).
The following macro symbols can be used to customize some DBC++ behaviour.
DBC_CONF_LOG_LEVEL
Indicate that log messages are printed (if a message is not printed, it
is not generated at all so to save a bit in performance).
dbc::LOG_LEVEL_NONE none
dbc::LOG_LEVEL_ASSERTION assertion messages only
dbc::LOG_LEVEL_TRACE assertion and trace messages
dbc::LOG_LEVEL_ALL all the abvoe
Default definition: dbc::LOG_LEVEL_ALL
DBC_CONF_LOG_TRACE(message)
Print specified trace message (null-terminated C-style string).
Default definition: '{ std::clog << "dbc: " << message << std::endl; }'
DBC_CONF_LOG_ASSERTION(message)
Print specified assertion message (null-terminated C-style string).
Default definition: '{ std::cerr << "dbc: " << message << std::endl; }'
DBC_CONF_DOC_ASSERTION(condition, label)
Generate documentation comments for assertion with specified condition
and label. Default definition generates Doxygen comments.
DBC_CONF_DOC_PRE(require_code)
Generate documentation comments for preconditions of the specified
require_code code block. Default definition generates Doxygen comments.
DBC_CONF_DOC_POST(ensure_code)
Generate documentation comments for postconditions of the specified
ensure_code code block. Default definition generates Doxygen comments.
DBC_CONF_DOC_INVARIANT(full_class_type, invariant_code)
Generate documentation comments for class-invariants of the specified
class type name (fully qualified with namespace prefix, template
parameters, etc) and invariant_code code block. Default definition
generates Doxygen comments.
NOTE: Beacuse C++ cannot parse template as macro parametrs and
full_class_type in general can be a template, DBC++ must internally
wrap the calss type within parenthesis when passing it as
full_class_type. For example, for a fully qualified class template type
'my_namespace::my_class<T1, T2>', 'full_class_type' will be
'(my_namespace::my_class<T1, T2>)' (note the extra parenthesis wrapping
the actual type). You documentation tool must be able to deal with this
(e.g., Doxygen ignores the parenthesis wrapping when referring to the
type).
8. CONTRACT DOCUMENTATION
-------------------------
DBC++ automatically documents your contracts using Doxygen. Run `doxygen' in
the "example" directory to generate the documentation for all the examples in
the "example/codedoc" directory.
In [Mey97] the "short form" of a class is essentially defined as the
specification of its public entities (signature and contract) and the related
documentation. If you instruct Doxygen to ignore private entities (option in
Doxyfile), the documentation generated by Doxygen can effectively be considered
a "short form" of your class with the contract documentation atuomatically
added by DBC++. Furthermore, Doxygen will link a derived class and its
inherited member functions to its base, this will effectively allow your to
browse the documentation like the "flat-short form" defined in [Mey97].
In the documentation generated by Doxygen, you will see class invariant,
operation post- and pre- documented from the contract source code in Doxygen
"codedoc/html/index.html". The following configuration is required in the
Doxyfile to support DBC++ (see "example/Doxyfile").
-- File: Doxyfile --
...
MACRO_EXPANSION = YES # Allows for exaping DBC++ macros.
INCLUDE_PATH = ../include # Path to "dbc.hpp" to resolve DBC++ macros.
PREDEFINED = DBC_DOC # Instruct DBC++ to generate assertion doc.
If you want to use a code documentation tools different from Doxygen, you
should be able to integrate with DBC++ by #defining the macros prefixed by
DBC_CONF_DOC_.
9. REFERENCES
-------------
In reference symbol alphabetic order.
[C++04] Proposal to add Design by Contract to C++.
Doc. no. N1613=04-0053, 2004.
[Mey97] B. Meyer. Object Oriented Software Construction, 2nd Edition.
Prentice-Hall, 1997.
[Mit02] R. Mitchell, J. McKim. Design by Contract, by Example.
Addison Wesley, 2002.
[Str97] B. Stroustrup. The C++ Programming Language, Special Edition.
Addison Wesley, 1997.
</pre>