contract/doc/contract_programming_overview.qbk

[/ Copyright (C) 2008-2012 Lorenzo Caminiti ]
[/ Distributed under the Boost Software License, Version 1.0 ]
[/ (see accompanying file LICENSE_1_0.txt or a copy at ]
[/ http://www.boost.org/LICENSE_1_0.txt) ]
[/ Home at http://sourceforge.net/projects/contractpp ]

[section Contract Programming Overview]

[:['["It is absurd to make elaborate security checks on debugging runs, when no trust is put in the results, and then remove them in production runs, when an erroneous result could be expensive or disastrous. What would we think of a sailing enthusiast who wears his life-jacket when training on dry land but takes it off as soon as he goes to sea?]]]
[:['-- Charles Antony Richard Hoare (see __Hoare73__)]]

This section gives an overview of Contract Programming (see __Meyer97__, __Mitchell02__, and __N1613__ for a detailed introduction to Contract Programming).

[note
The objective of this library is /not/ to convince programmers to use Contract Programming.
It is assumed that programmes understand the benefits and trade-offs associated with Contract Programming and they have already decided to use this methodology to formally program specifications.
Then, this library aims to be the best Contract Programming library for C++.
]

[section Assertions]

Contract Programming is characterized by the following type of assertion mechanisms.

[table
[ [Assertion] [Purpose] ]
[ [Preconditions] [
These are logical conditions that programmers expect to be true when the function is called (e.g., to check constraints on the function arguments).
] ]
[ [Postconditions] [
These are logical conditions that programmers expect to be true when the  function has ended normally (e.g., to check the result and any side effect that a function might have).
Postconditions can usually access the function result value (for non-void functions) and /old values/ that expressions had before the body execution.
] ]
[ [Class Invariants] [
These are logical conditions that programmers expect to be true after the constructor has been executed successfully, before and after the execution of every non-static public member function, and before the destructor is executed (e.g, class invariants can define valid states of all objects of a class).
It is possible to describe a different set of class invariants for volatile member functions but /volatile class invariants/ are assumed to be same as class invariants unless differently specified.
It is also possible to describe /static class invariants/ which are excepted to be true before and after the execution of any public member function (even if static), including constructor entry and destructor exit.
[footnote
*Rationale.*
Static and volatile class invariants were first introduced by this library to reflect the fact that C++ support both static and volatile member functions.
Static and volatile class invariants are not part of __N1962__.
]
] ]
[ [Subcontracting] [
Subcontracting is defined using the __substitution_principle__ and it predicates that: Preconditions cannot be strengthen, postconditions and class invariants cannot be weaken.
] ]
[ [Block Invariants] [
These are logical conditions that programmers except to be true every time the execution reaches the point where the condition is asserted.
When used within a loop (i.e., a block of code that can be executed in iteration), block invariants are also called /loop invariants/ and they assert conditions that are expected to be true for every loop iteration.
] ]
[ [Loop Variants] [
For a given loop, a [@http://en.wikipedia.org/wiki/Loop_variant loop variant] is a non-negative integer expression (`>= 0`) with a value that is expected to decrease at every subsequent loop iteration.
Loop variants are used to ensure that loops terminate avoiding infinite iterations.
] ]
]

It is a common Contract Programming requirement to disable other contracts while a contract assertions is being evaluated (in order to avoid infinite recursive calls).
This library implement this feature however it should be noted that in order to globally disable assertions while checking another assertion, some type of global variable needs to be used.
In multi-threaded environments, programmers can define the [macroref CONTRACT_CONFIG_THREAD_SAFE] configuration macro to protect such a global variable from racing conditions (but that will effectively introduce a global lock in the program).

A limited form of Contract Programming is the use of the C++ `assert` macro.
Using `assert` is common practice for many programmers but unfortunately it suffers from the following problems (that are instead resolved by using Contract Programming):

# `assert` is used within the implementation therefore the asserted conditions are not easily visible to the caller which is only familiar with the class and function declarations.
# `assert` does not distinguish between preconditions and postconditions.
In well-tested production code, postconditions can be disabled trusting the correctness of the implementation while preconditions might still need to remain enabled because of the evolution of the calling code.
Using `assert` it is not possible to selectively disable only postconditions and all assertions must be disabled at once.
# `assert` requires to manually program extra code to check class invariants (e.g., extra member functions and try blocks).
# `assert` does not support subcontracting.

[endsect]

[section Benefits]

The main use of Contract Programming is to improve software quality.
__Meyer97__ discusses how Contract Programming can be used as the basic tool to write ["correct] software.
Furhtermore, __Stroustrup97__ discusses the key importance of class invariants plus advantages and disadvantages of preconditions and postconditions.
The following is a short summary of the benefits associated with Contract Programming mainly taken from __N1613__.

[table
[ [#] [Topic] [Benefit] ]
[ [1.] [Preconditions and Postconditions] [
Using function preconditions and postconditions, programmers can give a precise semantic description of what a function requires at its entry and what it ensures under its (normal) exit.
In particular, using postcondition old values, Contract Programming provides a mechanism that allows programmers to compare values of an expression before and after the function body execution.
This mechanism is powerful enough to enable programmers to express many constraints within the code, constraints that would otherwise have to be captured at best only informally by the code documentation.
] ]
[ [2.] [Class Invariants] [
Using class invariants, programmers can describe what to expect from a class and the logic dependencies between the class members.
It is the job of the constructor to ensure that the class invariants are satisfied when the object is first created.
Then the implementation of the member functions can be largely simplified as they can be written knowing that the class invariants are satisfied because Contract Programing checks them before and after the execution of every member function. 
Finally, the destructor makes sure that the class invariants hold for the entire life of the object, checking the class invariants one last time before the object is destructed.
] ]
[ [3.] [Self-Documenting Code] [
Contracts are part of the source code, they are executed and verified at run-time so they are always up to date with the code itself.
Therefore the specifications, as documented by the contracts, can be trusted to always be up to date with the implementation code.
] ]
[ [4.] [Easier Debugging] [
Contract Programming can provide a powerful debugging facility because, if contracts are well written, bugs will cause contract assertions to fail exactly where the problem first occurs instead than at some later stage of the program execution in an apparently unrelated manner.
Note that a precondition failure points to a bug in the function caller, a postcondition failure points instead to a bug in the function implementation. 
Furthermore, in case of contract failure, this library provides detailed error messages that greatly helps debugging.
[footnote Of course, if the contract is ill written then Contract Programming is of little use.
However, it is less likely to have a bug in both the function body and the contract than in the function body only.
For example, consider the validation of a result in postconditions.
Validating the return value might seem redundant, but in this case we actually want that redundancy.
When programmers write a function, there is a certain probability that they make a mistake in implementing the function body.
When programmers specify the result of the function in the postconditions, there is also a certain probability that they make a mistake in writing the contract. 
However, the probability that programmers make a mistake twice (in both the body /and/ the contract) is lower than the probability that the mistake is made just once (in either the body or the contract).]
] ]
[ [5.] [Easier Testing] [
Contract Programming facilitates testing because a contract naturally specifies what a test should check.
For example, preconditions of a function state which inputs cause the function to fail and postconditions state which outputs are produced by the function on normal exit.
] ]
[ [6.] [Formal Design] [
Contract Programming can serve to reduce the gap between designers and programmers by providing a precise and unambiguous specification language.
Moreover, contracts can make code reviews easier.
] ]
[ [7.] [Formal Inheritance] [
Contract Programming formalizes the virtual function overriding mechanism using subcontracting as justified by the __substitution_principle__.
This keeps the base class programmers in control as overriding functions still have to fully satisfy the base class contracts.
] ]
[ [8.] [Replace Defensive Programming] [
Contract Programming assertions can replace [@http://en.wikipedia.org/wiki/Defensive_programming Defensive Programming] checks localizing these checks within the contract and making the code more readable.
] ]
]

[endsect]

[section Costs]

Contract Programming benefits come to the cost of performance as discussed in detail by both __Stroustrup97__ and __Meyer97__.
However, while performance trade-offs should be carefully considered depending on the specific application domain, software quality cannot be sacrificed (it is difficult to see the value of software that quickly and efficiently provides an incorrect result).

The run-time performances are negatively impacted by Contract Programming mainly because of the following:

# The extra processing required to check the assertions.
# The extra processing required by the additional function calls (additional functions are invoked to check preconditions, postconditions, class invariants, etc).
# The extra processing required to copy expression results when old values that are used in postconditions.

To mitigate the run-time performance impact, programmers can selectively turn off some of the contract compilation and the related run-time checking.
Programmers will have to decide based on the performance trade-offs required by their applications but a reasonable approach usually is to:

* Always write contracts to clarify the semantics of the design embedding the specifications directly into the code and making the code self-documenting.
* Enable preconditions, postconditions, and class invariants compilation and checking during initial testing.
* Enable only preconditions (and possibly class invariants) during release testing and for the final release (see also [macroref CONTRACT_CONFIG_NO_PRECONDITIONS], [macroref CONTRACT_CONFIG_NO_POSTCONDITIONS], and [macroref CONTRACT_CONFIG_NO_CLASS_INVARIANTS]).

This approach is usually reasonable because in well-tested production code, validating the function body implementation using postconditions and class invariants is rarely needed since the function has shown itself to be ["correct] during testing.
On the other hand, checking function arguments using postconditions is always needed because of the evolution of the calling code.
Furthermore, postconditions are usually computationally more expensive to check (see the __Assertion_Requirements__ section for a mechanism to selectively enable assertions also based on their computational complexity).

Compile-time performances are also impacted by this library mainly because:

# The contracts appear in class and function declarations (usually header files) so they have to be re-compiled for each translation unit.
# The library implementation extensively uses preprocessor and template meta-programming which significantly stress compiler performances.

[#compilation_time_warning_anchor]
[warning
Unfortunately, the current implementation of this library significantly slows down compilation.
For example, for a project with 122 files and 15,471 lines of code, adding contracts to a total of 50 classes and 302 functions increased compilation time from 1 minute to 26 minutes when compilation was enabled for all contracts, and from 1 minute to 2 minutes when contracts were left in the code but contract compilation was disabled using this library configuration macros `CONTRACT_CONFIG_NO_...`.
[footnote
This library macros always need to expand to generate the class and function declarations even when contract compilation is disabled.
That is why there is a compile-time overhead, even if significantly smaller, also when contracts are all disabled (in this case however there is zero run-time overhead).
The compilation time overhead when all contracts are turned off could be further reduced by optimizing the library implementation to not include internal headers that are not required when contracts are off (this type of optimizations will be a major focus on future releases).
]

On compilers that support [@http://en.wikipedia.org/wiki/Precompiled_header pre-compiled headers] (GCC, MSVC, etc), these can be used to reduce re-compilation time.
For example, re-compilation time of [link contract__.examples.__n1962___vector__comparison_with_c___proposed_syntax =vector.cpp=] from the __Examples__ section is reduced from 44 seconds to 24 seconds (55% faster) when its header [link contract__.examples.__n1962___vector__comparison_with_c___proposed_syntax =vector.hpp=] is pre-compiled (with all contracts enabled).
[footnote
There is essentially no gain in pre-compiling this library headers because most of the compilation time is taken by expanding and compiling this library macros as they appear in the user code (and not by the library implementation code itself).
Furthermore, pre-compiled headers should be used with the usual care because they can complicate the build system and they introduce extra dependencies that might limit the amount of targets that can be built simultaneously in a parallel build.
However, if properly used, pre-compiled headers can significantly reduce re-compilation time when using this library.
]

The authors have not done a detailed preprocessing-time and compile-time analysis of the performances of this library.
Therefore, the authors have not yet tried to optimize this library compilation-time.
Reducing compilation-time will be a major focus of future releases (see also [@https://sourceforge.net/apps/trac/contractpp/ticket/48 Ticket 48]).
]

Finally, Contract Programming should be seen as a tool to complement (and not to substitute) testing.

[endsect]

[section Free Function Calls]

A /free function/
[footnote
In C++, a free function is any function that is not a member function.
]
call executes the following steps:

# Check the function preconditions.
# Execute the function body.
# Check the function postconditions.

[endsect]

[section Member Function Calls]

A member function call executes the following steps:

# Check the static class invariants.
# Check the non-static class invariants (in __logic_and__ with the base class invariants when subcontracting).
These are checked only for non-static member functions.
[footnote
Static member functions cannot be virtual so they cannot be overridden and they do not subcontract.
]
Volatile member functions check volatile class invariants instead.
# Check the function preconditions (in __logic_or__ with the overridden function preconditions when subcontracting).
# Execute the function body.
# Check the static class invariants (even if the body throws an exception).
# Check the non-static class invariants (in __logic_and__ with the base class invariants when subcontracting).
These are checked only for non-static member functions and even if the body throws an exception.
Volatile member functions check volatile class invariants instead.
# Check the function postconditions (in __logic_and__ with the overridden function postconditions when subcontracting).
These are checked only if the body does not throw an exception.

[#logic_and_anchor] [#logic_or_anchor]
In this documentation __logic_and__ and __logic_or__ are the logic /and/ and /or/ operations evaluated in short-circuit:

* `p` __logic_and__ `q` is true if and only if both `p` and `q` are true but `q` is evaluated only when `p` is true.
* `p` __logic_or__ `q` is true if and only if either `p` or `q` is true but `q` is evaluated only when `p` is false.

Class invariants are checked before preconditions and postconditions so that preconditions and postconditions assertions can be simplified by being programmed under the assumption that class invariants are satisfied (e.g., if class invariants assert that a pointer cannot be null then preconditions and postconditions can safety dereference the pointer without additional checking).
Similarly, subcontracting checks contracts of base classes before checking the derived class contracts so that the base class contract can be programmed under the assumption that the base class contracts are satisfied.
When a member function overrides more than one virtual base function because of multiple inheritance:

* Class invariants are checked in __logic_and__ with the class invariants of all base classes following the inheritance order.
* Preconditions are checked in __logic_or__ with the preconditions of all overridden functions following the inheritance order.
* Postconditions are checked in __logic_and__ with the postconditions of all overridden functions following the inheritance order.

Note that:

* Preconditions and postconditions of static member functions cannot access the object.
* Preconditions, postconditions, and volatile class invariants of volatile member functions access the object as (constant) volatile.

[endsect]

[section Constructor Calls]

A constructor call executes the following steps:

# Check the constructor preconditions.
# Initialize base classes and members executing the constructor member initialization list if present.
# Check the static class invariants (but not the non-static class invariants).
# Execute the constructor body.
# Check the static class invariants (even if the body throws an exception).
# Check the non-static class invariants, but only if the body did not throw an exception.
# Check the constructor postconditions, but only if the body did not throw an exception.

Preconditions are checked before initializing base classes and members so that these initializations can relay on preconditions to be true (for example to validate constructor arguments before they are used to initialize member variables).
C++ object construction mechanism will automatically check base class contracts when subcontracting.

Note that:

* Non-static class invariants are not checked at constructor entry (because there is no object before the constructor body is executed).
* Preconditions cannot access the object (because there is no object before the constructor body is executed).
* Postconditions cannot access the object old value (because there was no object before the constructor body was executed).
* The object is never volatile within constructors so constructors do not check volatile class invariants.

[endsect]

[section Destructor Calls]

A destructor call executes the following steps:

# Check the static class invariants.
# Check the non-static class invariants.
# Execute the destructor body.
# Check the static class invariants (even if the body throws an exception).
[footnote
For generality, this library does not require the destructor body to not throw exceptions.
However, in order to comply with the STL exception safety requirements, destructors should never throw.
]
# Check the non-static class invariants, but only if the body threw an exception.

C++ object destruction mechanism will automatically check base class contracts when subcontracting.

Note that:

* Destructors have no parameter and they can be called at any time after object construction so they have no preconditions.
* After the destructor body is executed, the object no longer exists so non-static class invariants do not have to be true and they are not checked at destructor exit.
* Destructors have no postconditions because they have no parameter and after the body execution there is no object.
[footnote
In theory, destructors could have static postconditions (i.e., postconditions that are not allowed to access the object which no longer exists after destruction).
Still destructors shall never have preconditions because a destructor can be called at any point after the object is constructed as long the class invariants hold.
None of the Contract Programming references that the authors have studied propose static postconditions for destructor (neither __N1962__ nor __Meyer97__, but __Eiffel__ has no static data member).
Future revisions of this library might implement destructor static postconditions (e.g., a destructor postconditions of a class that counts object instances could assert that the instance counter stored in a static data member should be decreased of one because the object has been destructed, see also [@https://sourceforge.net/apps/trac/contractpp/ticket/41 Ticket 41]).
]
* The object is never volatile within destructors so destructors do not check volatile class invariants.

[endsect]

[section Constant-Correctness]

Contracts are only responsible to check the program state in oder to ensure its compliance with the specifications.
Therefore, contracts should not be able to modify the program state and exclusively "read-only" operations (or /queries/) should be used to program contracts.

This library enforces this constraint at compile-time using C++ `const` qualifier.
[footnote
As usual in C++, constant-correctness can be enforced at compile-time only as long as programmers do not use `const_cast` and `mutable`.
]
Contracts only have access to the object, function arguments, and function return value via constant references `const&` or pointers `const*`.
Other variables (static data members, global variables, etc) can be explicitly made constant using /constant assertions/ (see the __Advanced_Topics__ section).

[endsect]

[section Specification vs. Implementation]

Contracts are part of the program specification and not of its implementation.
Therefore, contracts should appear within C++ declarations and not within definitions.
[footnote
This is a major conceptual difference with respect to [@http://en.wikipedia.org/wiki/Defensive_programming Defensive Programming] and using `assert` because they program assertions within the function body instead that with the function declaration.
]

Contracts are most useful when they assert conditions only using public members.
For example, the caller of a member function cannot in general make sure that the member function preconditions are satisfied if these preconditions use private members that are not accessible by the caller.
Therefore, a failure in the preconditions will not necessarily indicate a bug in the caller given that the caller was not able to fully check the preconditions before calling the member function.
In most cases, the need of using non-public members to check contracts indicates an error in the design of the class.
However, given that C++ provides programmers ways around access level restrictions (e.g., `friend` and function pointers), this library leaves it up to the programmers to make sure that only public members are used in contract assertions (__N1962__ follows the same approach not forcing contracts to only use public members, __Eiffel__ instead generates a compiler error if preconditions use non-public members).
[footnote
*Rationale.*
In theory, if C++ [@http://www.open-std.org/jtc1/sc22/wg21/docs/cwg_defects.html#45 defect 45] were not fixed, this library could have generated a compile-time error for preconditions that use non-public members.
]

Finally, only public member functions shall check class invariants.
Private and protected member functions are allowed to brake class invariants because private and protected member are part of the class implementation and not of its specification.

[endsect]

[section Broken Contracts]

After programmers specify contracts, this library automatically checks preconditions, postconditions, class invariants, block invariants, and loop variants at run-time.
If a precondition, postcondition, class invariant, block invariants, or loop variant is checked to be false or throws an exception then the library invokes the [funcref contract::precondition_broken], [funcref contract::postcondition_broken], [funcref contract::class_invariant_broken_on_entry] or [funcref contract::class_invariant_broken_on_exit] or [funcref contract::class_invariant_broken_on_throw], [funcref contract::block_invariant_broken], and [funcref contract::loop_variant_broken] function respectively.

These function invoke `std::terminate()` by default but programmers can redefine them to take a different action (throw an exception, exit the program, etc) using [funcref contract::set_precondition_broken], [funcref contract::set_postcondition_broken], [funcref contract::set_class_invariant_broken], [funcref contract::set_block_invariant_broken], and [funcref contract::set_loop_variant_broken] (this mechanism is similar to the one of C++'s `std::terminate()`).
See the __Contract_Broken_Handlers__ section for an example.

[endsect]

[section Features]

The design of this library was largely based on __N1962__ and on the __Eiffel__ programming language as specified by __Meyer97__.
The following table compares features between this library, the proposal for adding Contract Programming to the C++ standard __N1962__, the __Eiffel__ programming language __Meyer97__, and the __D__ programming language __Bright04__.

[table
[
    [Feature]
    [This Library (C++03)]
    [\[N1962\] Proposal (not part of C++)]
    [ISE Eiffel 5.4]
    [D]
][
    [['Keywords and Specifiers]]
    [`precondition`, `postcondition`, `extends`, `initialize`, `requires`, `in`, `out`, `deduce`, `comma` (these are specifiers and not keywords, they have special meaning only in specific positions within the declarations passed to this library macros)]
    [`invariant`, `precondition`, `postcondition`, `oldof`]
    [=invariant=, =require=, =ensure=, =do=, =require else=, =ensure then=, =old=, =result=, =variant=]
    [=invariant=, =in=, =out=, =assert=, =static=]
][
    [['On contract failure]]
    [Default to `std::terminate()` (but can be customized to exit, abort, throw exceptions, etc).]
    [Default to `std::terminate()` (but can be customized to exit, abort, throw exceptions, etc).]
    [Throw exceptions]
    [Throw exceptions]
][
    [['Result value in postconditions]]
    [Yes, `auto `[^['result-variable-name]]` = return`.]
    [Yes, `postcondition (`[^['result-variable-name]]`)`.]
    [Yes, =result= keyword.]
    [No.]
][
    [['Old values in postconditions]]
    [Yes, `auto `[^['old-variable-name]]` = CONTRACT_OLDOF `[^['oldof-expression]].]
    [Yes, `oldof `[^['oldof-expression]].]
    [Yes, [^old ['old-expression]].]
    [No.]
][
    [['Subcontracting]]
    [Yes, also support multiple base contracts for multiple inheritance (can force preconditions to be specified only by base classes using [macroref CONTRACT_CONFIG_DO_NOT_SUBCONTRACT_PRECONDITIONS]).]
    [Yes, also support multiple base contracts but only base classes can specify preconditions.]
    [Yes.]
    [Yes.]
][
    [['Contracts for pure virtual functions]]
    [Yes.]
    [Yes.]
    [Yes (contracts for abstract functions).]
    [No (but planned).]
][
    [['Arbitrary code in contracts]]
    [No, assertions only.]
    [No, assertions only.]
    [No, assertions only plus preconditions can only access public members.]
    [Yes.]
][
    [['Constant-correct]]
    [Yes.]
    [Yes.]
    [Yes.]
    [No.]
][
    [['Function code ordering]]
    [Preconditions, postconditions, body.]
    [Preconditions, postconditions, body.]
    [Preconditions, body, postconditions.]
    [Preconditions, postconditions, body.]
][
    [['Static assertions]]
    [Yes, can use `static_assert` (internally implemented using `BOOST_MPL_ASSERT_MSG`, no __CXX11__ required).]
    [Yes, can use __CXX11__ `static_assert`.]
    [No.]
    [Yes.]
][
    [['Block invariants]]
    [Yes, [macroref CONTRACT_BLOCK_INVARIANT].]
    [Yes, `invariant`.]
    [Yes (`check` instruction and loop invariants).]
    [No (just `assert`).]
][
    [['Loop variants]]
    [Yes, [macroref CONTRACT_LOOP_VARIANT].]
    [No.]
    [Yes.]
    [No.]
][
    [['Disable assertion checking within assertions checking]]
    [
    Yes (use [macroref CONTRACT_CONFIG_PRECONDITIONS_DISABLE_NO_ASSERTION] for preconditions to disable no assertion).
    Use [macroref CONTRACT_CONFIG_THREAD_SAFE] to make the implementation of this feature thread-safe in multi-threaded programs (but it will introduce a global lock).
    ]
    [Yes for class invariants and postconditions but preconditions disable no assertion.]
    [Yes.]
    [No.]
][
    [['Assertion requirements]]
    [Yes (compilation and run-time checking of single assertions can be disabled when specific assertion requirements are not met).]
    [No.]
    [No (but all types are __CopyConstructible__, __Assignable__, and __EqualityComparable__ in __Eiffel__ so there is not a real need for this).]
    [No.]
][
    [['Nested member function calls]]
    [
        Disable nothing.
        [footnote
        *Rationale.*
        Older versions of this library automatically defined a data member used to disable checking of class invariants within member function calls.
        However, this feature, which was required by older revisions of __N1962__, is no longer required by __N1962__, it complicates the implementation, and in multi-thread programs would introduce a lock that synchronizes all member functions calls for a given object so it was removed in the current revision of the library.
        ]
    ]
    [Disable nothing.]
    [Disable all checks.]
    [Disable nothing.]
][
    [['Non-static class invariants checking]]
    [
        At constructor exit, at destructor entry, and at public member function entry, exit, and on throw (but only if programmers declare these functions using this library macros).
        Same for volatile class invariants.]
    [At constructor exit, at destructor entry, and at public member function entry, exit, and on throw (volatile class invariants not supported).]
    [At constructor exit, and around public member functions.]
    [At constructor exit, at destructor entry, an around public member functions.]
][
    [['Static class invariants checking]]
    [At entry and exit of any (also static) member function, constructor, and destructor.]
    [No.]
    [No (but __Eiffel__ does not have static members).]
    [No.]
][
    [['Removable from object code]]
    [Yes, using any combination of [macroref CONTRACT_CONFIG_NO_PRECONDITIONS], [macroref CONTRACT_CONFIG_NO_POSTCONDITIONS], [macroref CONTRACT_CONFIG_NO_CLASS_INVARIANTS], [macroref CONTRACT_CONFIG_NO_BLOCK_INVARIANTS], and [macroref CONTRACT_CONFIG_NO_LOOP_VARIANTS].]
    [Yes.]
    [Yes (but predefined combinations only).]
    [Yes.]
]
]

Contract Programming is also provided by the following references.

[table
[ [Reference] [Language] [Notes] ]
[ [__Bright04b__] [C++] [
The Digital Mars C++ compiler extends C++ adding Contract Programming language support (among many other features).
] ]
[ [__Lindrud04__] [C++] [
This supports class invariants and old values but it does not support subcontracting, contracts are specified within definitions instead of declarations, assertions are not constant-correct (unfortunately, these missing features are all essential to Contract Programming).
] ]
[ [__Tandin04__] [C++] [
Interestingly, these contract macros automatically generate __Doxygen__ documentation
[footnote
*Rationale.*
Older versions of this library used to automatically generate __Doxygen__ documentation from the contract macros.
This functionality was abandoned for a number of reasons: this library macros became too complex and the __Doxygen__ preprocessor is no longer able to expand them; the __Doxygen__ documentation was just a repeat of the contract code (so programmers can directly look at contracts in the header files), __Doxygen__ might not necessarily be the documentation tool chosen by all programmers.
]
but old values, class invariants, and subcontracting are not supported plus contracts are specified within definitions instead of declarations (unfortunately, these missing features are all essential to Contract Programming).
] ]
[ [__Maley99__] [C++] [
This supports Contract Programming including subcontracting but with some limitations (e.g., programmers need to manually build an inheritance tree using artificial template parameters), it does not use macros so programmers are required to write by hand a significant amount of boiler-plate code.
(The authors have found this work very inspiring when they started to develop this library.)
] ]
[ [__C2__] [C++] [
This uses an external preprocessing tool (the authors could no longer find this project code-base to evaluate it).
] ]
[ [__iContract__] [Java] [
This uses an external preprocessing tool.
] ]
[ [__Jcontract__] [Java] [
This uses an external preprocessing tool.
] ]
[ [__CodeContracts__] [.NET] [
Microsoft Contract Programming for .NET programming languages.
] ]
[ [__SpecSharp__] [C#] [
This is a C# extension with Contract Programming language support.
] ]
[ [__Chrome02__] [Object Pascal] [
This is the .NET version of Object Pascal and it has language support for Contract Programming.
] ]
[ [__SPARKAda__] [Ada] [
This is an Ada-like programming language with Contract Programming support.
] ]
]

Typically, preprocessing tools external to the language work by transforming specially formatted code comments into contract code that is then checked at run-time.
One of this library primary goals was to support Contract Programming entirely within C++ and without using any tool external to the standard language (C++ macros were used instead of external preprocessing tools).

To the authors' knowledge, this the only library that fully support Contract Programming for C++ (see the __Bibliography__ section for the complete list of Contract Programming references studied by the authors).

[endsect]

[endsect]