Velocity Reviews - Computer Hardware Reviews

Velocity Reviews > Newsgroups > Programming > C++ > Released Contract Programming Library for C++

Reply
Thread Tools

Released Contract Programming Library for C++

 
 
Lorenzo Caminiti
Guest
Posts: n/a
 
      06-10-2012
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.ne...tml/index.html

Source:
http://sourceforge.net/projects/cont...atest/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.ne...rview.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.ne...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.ne...warning_anchor

This library could be extended to also support concept definitions (at
least for C++11):
http://contractpp.svn.sourceforge.ne...t_implemented_
 
Reply With Quote
 
 
 
 
Lorenzo Caminiti
Guest
Posts: n/a
 
      06-10-2012
On Jun 10, 2:42*pm, Leigh Johnston <(E-Mail Removed)> wrote:
> On 10/06/2012 15:43, Lorenzo Caminiti wrote:
> > #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_;
> > };

>
> 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.ne.../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.ne...ion.an_example

Strange syntaxes have not stopped other library authors:
http://www.boost.org/doc/libs/1_49_0...tml/index.html
http://zao.se/~zao/boostcon/11/slides/Boost.Generic.pdf
http://boost-sandbox.sourceforge.net...enix/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
 
Reply With Quote
 
 
 
 
Pavel
Guest
Posts: n/a
 
      06-10-2012
Lorenzo Caminiti wrote:
> 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.ne...tml/index.html
>
> Source:
> http://sourceforge.net/projects/cont...atest/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.ne...rview.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.ne...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.ne...warning_anchor
>
> This library could be extended to also support concept definitions (at
> least for C++11):
> http://contractpp.svn.sourceforge.ne...t_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
 
Reply With Quote
 
Lorenzo Caminiti
Guest
Posts: n/a
 
      06-10-2012
On Jun 10, 4:15*pm, Pavel
<(E-Mail Removed)> wrote:
> Lorenzo Caminiti wrote:
> > 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.ne.../releases/cont...

>
> > Source:
> >http://sourceforge.net/projects/cont...atest/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.ne.../releases/cont...

>
> > 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.ne.../releases/cont...

>
> > 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.ne.../releases/cont...

>
> > This library could be extended to also support concept definitions (at
> > least for C++11):
> >http://contractpp.svn.sourceforge.ne.../releases/cont...

>
> 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.ne...oken_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.ne...ow_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.ne...function_calls

Thanks,
--Lorenzo
 
Reply With Quote
 
Lorenzo Caminiti
Guest
Posts: n/a
 
      06-11-2012
On Jun 11, 12:04*pm, (E-Mail Removed) (Scott Lurndal) wrote:
> Lorenzo Caminiti <(E-Mail Removed)> writes:
> >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.

>
> 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.ne...iew.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
 
Reply With Quote
 
 
 
Reply

Thread Tools

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is On
HTML code is Off
Trackbacks are On
Pingbacks are On
Refbacks are Off


Similar Threads
Thread Thread Starter Forum Replies Last Post
VHDL and Verilog - 15 x Contract Engineers Required Urgently - Long Term Contract Specialist Verilog Engineers Roles VHDL 0 06-27-2007 01:09 PM
Seek Contract Programming Work - 17 Years Experience Michael D. Crawford Java 0 02-22-2005 11:42 PM
OT C++ contract programming - how to find? BCC C++ 6 05-09-2004 05:40 AM
Looking for a contract or freelance programming or design job? CorporateRebel.com HTML 2 05-02-2004 05:00 PM



Advertisments