Released Contract Programming Library for C++

[Lorenzo Caminiti]

Hello all,

I have released Contract++ 0.4.0 on SourceForge (this library is being
considered for addition into Boost).

This library implements Contract Programming for the C++ programming
language (see the end of this email). In addition, the library
implements virtual specifiers (final, override, and new, see C++11),
concept checking, and named parameters.
This library is implemented for the C++03 standard and it does not
require C++11.

Documentation:
http://contractpp.svn.sourceforge.n...releases/contractpp_0_4_0/doc/html/index.html

Source:
http://sourceforge.net/projects/contractpp/files/latest/download

Comments are welcome!

Thanks,
--Lorenzo

INTRODUCTION

Contract Programming is also known as Design by Contract(TM) and it
was first introduced by the Eiffel programming language.
All Contract Programming features of the Eiffel programming language
are supported by this library, among others:

* Support for preconditions, postconditions, class invariants, block
invariants, and loop variants.
* Subcontract derived classes (with support for pure virtual functions
and multiple inheritance).
* Access expression old values and function return value in
postconditions.
* Optional compilation and checking of preconditions, postconditions,
class invariants, block invariants, and loop variants.
* Customizable actions on contract assertion failure (terminate by
default but it can throw, exit, etc).

All features:
http://contractpp.svn.sourceforge.n...ract__.contract_programming_overview.features

EXAMPLE

The example below shows how to use this library to program contracts
for the STL member function std::vector:ush_back (in order to
illustrate subcontracting, the vector class inherits from the somewhat
arbitrary pushable base class).

#include <contract.hpp> // This library.
#include <boost/concept_check.hpp>
#include <vector>
#include "pushable.hpp" // Some base class.

CONTRACT_CLASS(
template( typename T ) requires( boost::CopyConstructible<T> ) //
Concepts.
class (vector) extends( public pushable<T> ) // Subcontracting.
) {
CONTRACT_CLASS_INVARIANT_TPL(
empty() == (size() == 0) // More class invariants here...
)

public: typedef typename std::vector<T>::size_type size_type;
public: typedef typename std::vector<T>::const_reference
const_reference;

CONTRACT_FUNCTION_TPL(
public void (push_back) ( (T const&) value ) override
precondition(
size() < max_size() // More preconditions here...
)
postcondition(
auto old_size = CONTRACT_OLDOF size(), // Old-of
values.
size() == old_size + 1 // More postconditions here...
)
) {
vector_.push_back(value); // Original function body.
}

// Rest of class here (possibly with more contracts)...
public: bool empty ( void ) const { return vector_.empty(); }
public: size_type size ( void ) const { return vector_.size(); }
public: size_type max_size ( void ) const { return
vector_.max_size(); }
public: const_reference back ( void ) const { return
vector_.back(); }

private: std::vector<T> vector_;
};

NOTES

This library suffers of two limitations:

1. The unusual syntax used to declare classes and functions within the
macros which causes cryptic compiler errors when not used correctly
(syntax error checking and reporting could be somewhat improved in
future revisions of the library but there are fundamental limitations
on what can be done using the preprocessor).
http://contractpp.svn.sourceforge.n...ct__/grammar.html#syntax_error_warning_anchor

2. High compilation times (the authors have not tried to optimize the
library preproprocessor and template meta-programming code yet, that
will be the focus of future releases).
http://contractpp.svn.sourceforge.n...overview.html#compilation_time_warning_anchor

This library could be extended to also support concept definitions (at
least for C++11):
http://contractpp.svn.sourceforge.n...oncepts.concept_definitions__not_implemented_

 

[Lorenzo Caminiti]

I hate to rain on your parade

No worries

but who do you expect will want to write
C++ code that looks like that?

Yep, that's limitation 1:

NOTES
This library suffers of two limitations:
1. The unusual syntax used to declare classes and functions within the
macros which causes cryptic compiler errors when not used correctly
(syntax error checking and reporting could be somewhat improved in
future revisions of the library but there are fundamental limitations
on what can be done using the preprocessor).
http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/cont...

BTW, check this out for a side-by-side comparison with a proposed
Contract Programming syntax for language support:
http://contractpp.svn.sourceforge.n...index.html#contract__.introduction.an_example

Strange syntaxes have not stopped other library authors:
http://www.boost.org/doc/libs/1_49_0/libs/parameter/doc/html/index.html
http://zao.se/~zao/boostcon/11/slides/Boost.Generic.pdf
http://boost-sandbox.sourceforge.net/libs/phoenix/doc/html/
So for better or for worst the strange syntax did not stop me But I
understand your point and that's why I'm say upfront that's limitation
1.

I guess if you really want to use Contract Programming within C++ then
you don't really have another option, do you?

Ciao.
--Lorenzo

 

[Pavel]

Hello all,

I have released Contract++ 0.4.0 on SourceForge (this library is being
considered for addition into Boost).

This library implements Contract Programming for the C++ programming
language (see the end of this email). In addition, the library
implements virtual specifiers (final, override, and new, see C++11),
concept checking, and named parameters.
This library is implemented for the C++03 standard and it does not
require C++11.

Documentation:
http://contractpp.svn.sourceforge.n...releases/contractpp_0_4_0/doc/html/index.html

Source:
http://sourceforge.net/projects/contractpp/files/latest/download

Comments are welcome!

Thanks,
--Lorenzo

INTRODUCTION

Contract Programming is also known as Design by Contract(TM) and it
was first introduced by the Eiffel programming language.
All Contract Programming features of the Eiffel programming language
are supported by this library, among others:

* Support for preconditions, postconditions, class invariants, block
invariants, and loop variants.
* Subcontract derived classes (with support for pure virtual functions
and multiple inheritance).
* Access expression old values and function return value in
postconditions.
* Optional compilation and checking of preconditions, postconditions,
class invariants, block invariants, and loop variants.
* Customizable actions on contract assertion failure (terminate by
default but it can throw, exit, etc).

All features:
http://contractpp.svn.sourceforge.n...ract__.contract_programming_overview.features

EXAMPLE

The example below shows how to use this library to program contracts
for the STL member function std::vector:ush_back (in order to
illustrate subcontracting, the vector class inherits from the somewhat
arbitrary pushable base class).

#include <contract.hpp> // This library.
#include <boost/concept_check.hpp>
#include <vector>
#include "pushable.hpp" // Some base class.

CONTRACT_CLASS(
template( typename T ) requires( boost::CopyConstructible<T> ) //
Concepts.
class (vector) extends( public pushable<T> ) // Subcontracting.
) {
CONTRACT_CLASS_INVARIANT_TPL(
empty() == (size() == 0) // More class invariants here...
)

public: typedef typename std::vector<T>::size_type size_type;
public: typedef typename std::vector<T>::const_reference
const_reference;

CONTRACT_FUNCTION_TPL(
public void (push_back) ( (T const&) value ) override
precondition(
size() < max_size() // More preconditions here...
)
postcondition(
auto old_size = CONTRACT_OLDOF size(), // Old-of
values.
size() == old_size + 1 // More postconditions here...
)
) {
vector_.push_back(value); // Original function body.
}

// Rest of class here (possibly with more contracts)...
public: bool empty ( void ) const { return vector_.empty(); }
public: size_type size ( void ) const { return vector_.size(); }
public: size_type max_size ( void ) const { return
vector_.max_size(); }
public: const_reference back ( void ) const { return
vector_.back(); }

private: std::vector<T> vector_;
};

NOTES

This library suffers of two limitations:

1. The unusual syntax used to declare classes and functions within the
macros which causes cryptic compiler errors when not used correctly
(syntax error checking and reporting could be somewhat improved in
future revisions of the library but there are fundamental limitations
on what can be done using the preprocessor).
http://contractpp.svn.sourceforge.n...ct__/grammar.html#syntax_error_warning_anchor

2. High compilation times (the authors have not tried to optimize the
library preproprocessor and template meta-programming code yet, that
will be the focus of future releases).
http://contractpp.svn.sourceforge.n...overview.html#compilation_time_warning_anchor

This library could be extended to also support concept definitions (at
least for C++11):
http://contractpp.svn.sourceforge.n...oncepts.concept_definitions__not_implemented_

What does you library do when a precondition or invariant is broken? Is it a
configurable aspect? If yes, with what granularity (whole app/CONTRACT
CLASS/other) and how is it expressed syntactically?

Also, at what points are class invariants checked? At entry and exit to and from
CONTRACT_FUNCTION_TPLs?

Thank you,
Pavel

 

[Lorenzo Caminiti]

What does you library do when a precondition or invariant is broken?

When a precondition assertion evaluates to false or its evaluation
throws an exception (i.e., it's broken), the library calls the
precondition broken handler function contract:recondition_broken.

Is it a configurable aspect?

Yes, by default the precondition broken handler function calls
std::terminate. However, programmers can set their own precondition
broken handler function using contract::set_precondition_broken.
Programmer's broken handler functions can exit, abort, throw an
exception, log an error and continue, or anything else programmers
decide to do in their handler functions.

The same is true to postconditions, class invariants, block
invariants, and loop variants.
http://contractpp.svn.sourceforge.n...ontract_programming_overview.broken_contracts

If yes, with what granularity (whole app/CONTRACT
CLASS/other) and how is it expressed syntactically?

Granularity and syntax are of set_precondition_broken,
set_postcondition_broken, set_class_invariant_broken_on_entry,
set_class_invariant_broken_on_exit,
set_class_invariant_broken_on_throw, set_block_invariant_broken, and
set_loop_variant_broken. For convenience, set_class_invariant_broken
sets all class invariant broken entry/exit/throw to the same handler.
http://contractpp.svn.sourceforge.n...s.contract_broken_handlers__throw_on_failure_

Also, at what points are class invariants checked? At entry and exit to and from
CONTRACT_FUNCTION_TPLs?

Class invariants are checked at public constructor exit (if it doesn't
throw), and public destructor entry, at each non-static public member
function entry and exit (even if it throws). Protected and private
members do not check class invariants. The library also defines static
class invariants and volatile class invariants, these have different
checking semantics.
http://contractpp.svn.sourceforge.n...ct_programming_overview.member_function_calls

Thanks,
--Lorenzo

 

[Lorenzo Caminiti]

How is this any better than just placing explicit calls to
assert() at the appropriately points in the code?

Contract Programming is "better" than assert() (or to say it
correctly, Contract Programming might better fit the need of some
applications than assert() does) in a nutshell because:

1. 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.
2. 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 3. it is not possible to
selectively disable only postconditions and all assertions must be
disabled at once.
4. assert requires to manually program extra code to check class
invariants (e.g., extra member functions and try blocks).
5. assert does not support subcontracting.

http://contractpp.svn.sourceforge.n...ct__.contract_programming_overview.assertions

For example, the STL lists preconditions, postconditions, and
invariants requirements in its documentation (too bad we can't
actually program these requirements because C++ doesn't support
Contract Programming): http://www.sgi.com/tech/stl/

FWIW, MVS (the operating system circa 1974) had pre-assertions, post-assertions, recovery
functions et.al. on pretty much every function; and it was written in assembler. This certainly
predated Eiffel by a considerable margin.

Eiffel was the first programming language to formalize the use of
assertions in OO and that resulted in Contract Programming (again, for
example subcontracting and class invariants, but also that assertions
belong to declarations and not definitions, assertion constant-
correctness, old values in postcondiitons, etc).

From wikipedia:

MVS took a major step forward in fault-tolerance, built on the earlier STAE facility,
that IBM called software recovery. IBM decided to do this after years of practical
real-world experience with MVT in the business world. System failures were now having
major impacts on customer businesses, and IBM decided to take a major design jump, to
assume that despite the very best software development and testing techniques, that
'problems WILL occur.' This profound assumption was pivotal in adding great percentages
of fault-tolerance code to the system, but likely contributed to the system's success
in tolerating software and hardware failures. Statistical information is hard to come
by to prove the value of these design features (how can you measure 'prevented' or
'recovered' problems?), but IBM has, in many dimensions, enhanced these fault-tolerant
software recovery and rapid problem resolution features, over time.

This design specified a hierarchy of error-handling programs, in system
(kernel/'privileged') mode, called Functional Recovery Routines, and in user
('task' or 'problem program') mode, called "ESTAE" (Extended Specified Task Abnormal
Exit routines) that were invoked in case the system detected an error (actually,
hardware processor,  storage error, or software error). Each recovery routine
made the 'mainline' function reinvokable, captured error diagnostic data sufficient
to debug the causing problem, and either 'retried' (reinvoke the mainline) or 'percolated'
(escalated error processing to the next recovery routine in the hierarchy).

Yep, these are good reasons for preconditions and postconditions that
should be extended to class invariants as soon as we cross the OO
line.

Ciao,
--Lorenzo