PrevUpHomeNext

Reference

Header <contract/assert.hpp>
Header <contract/block.hpp>
Header <contract/body.hpp>
Header <contract/config.hpp>
Header <contract/constructor.hpp>
Header <contract.hpp>
Header <contract/destructor.hpp>
Header <contract/from.hpp>
Header <contract/macros.hpp>
Header <contract/nonmember_function.hpp>
Header <contract/nonstatic_member_function.hpp>
Header <contract/old.hpp>
Header <contract/state.hpp>
Header <contract/static_member_function.hpp>
Header <contract/wrap.hpp>

Facilities to assert contract conditions and specify actions to take in case of contract failure.


CONTRACT_ASSERT(boolean_condition)
CONTRACT_ASSERT_MSG(boolean_condition, string_description)
namespace contract {
  class failure;
  typedef __ContractFailedHandler__ contract_failed_handler;
  contract_failed_handler set_block_invariant_failed(contract_failed_handler);
  void block_invariant_failed(const from &);
  contract_failed_handler set_class_invariant_failed(contract_failed_handler);
  void class_invariant_failed(const from &);
  contract_failed_handler set_precondition_failed(contract_failed_handler);
  void precondition_failed(const from &);
  contract_failed_handler set_postcondition_failed(contract_failed_handler);
  void postcondition_failed(const from &);
}

Assert block (and loop) invariants and loop variants.


CONTRACT_ASSERT_BLOCK_INVARIANT(boolen_condition)
CONTRACT_ASSERT_BLOCK_INVARIANT_MSG(boolean_condition, string_description)
CONTRACT_ASSERT_LOOP_VARIANT(integer_expression)
CONTRACT_ASSERT_LOOP_VARIANT_MSG(integer_expression, string_description)
CONTRACT_INIT_LOOP_VARIANT
namespace contract {
  typedef __Integer__ loop_variant_type;
}

Macros used to name the body function when separating its definition from the contract declaration.

For example, these macros are used when function body definitions are implemented in a source file ".cpp" while the function and contract declarations are given in separate header file ".hpp".

See: Examples and more information in the Tutorial section.


CONTRACT_CONSTRUCTOR_BODY(class_type, class_name)
CONTRACT_DESTRUCTOR_BODY(class_type, class_name)
CONTRACT_BODY(function_name)

Macros to change some of the library compile-time configuration.

Configuration macros can be #defined by the user to change some of the library behaviour. If the user does not #define these macros, the library uses proper default values:

    #ifndef CONTRACT_CONFIG_SOMETHING
    #   define CONTRACT_CONFIG_SOMETHING some-default-value
    #endif

Note: It is strongly recommended not to changed the configuration macro default values unless strictly necessary.


CONTRACT_CONFIG_MAX_FUNCTION_ARITY
CONTRACT_CONFIG_MAX_MULTIPLE_INHERITANCE

Class template used to write contracts for constructors.

namespace contract {
  template<typename F> class constructor;
}

Header <contract.hpp>

Include the entire library.

    #include <contract.hpp>

It is recommended to include the library this way instead of including the single header files from the "contract/" directory.

Metaprogramming Symbols

This documentation source code indicates some metaprogramming constructs using special mixed-case symbols prefixed and postfixed by double underscores "__". These symbols are then expanded to actual code in the documentation text. For example:

    // Metaprogramming conventions for this documentation.
    __AMetaprogrammingConstruct__
    __AMetaprogrammingConstructWithParameters__< X, Y, Z >

In this convention, these metaporgramming constructs are not templates. They are internally implemented by the library using both preprocessor and template metaprogramming (in a way that is intentionally not documented here because it is library implementation specific).

See: Getting Started section.


CONTRACT_CHECK_BLOCK_INVARIANT
CONTRACT_CHECK_CLASS_INVARIANT
CONTRACT_CHECK_PRECONDITION
CONTRACT_CHECK_POSTCONDITION

Class template used to write contracts for destructors.

namespace contract {
  template<typename F> class destructor;
}

Context from which the contract failure was generated.

namespace contract {
  enum from;
}

Contract macros.

These macros are the primary tools to write contracts.

See: See the Tutorial section for examples.


CONTRACT_INVARIANT(sequence)
CONTRACT_CONSTRUCTOR(sequence)
CONTRACT_DESTRUCTOR(sequence)
CONTRACT_FUNCTION(sequence)

Class template used to write contracts non-member functions.

namespace contract {
  template<typename F> class nonmember_function;
}

Class template used to write contracts for non-static member functions.

namespace contract {
  template<typename F, typename BaseContractClass1 = void, ... , 
           typename BaseContractClassM = void> 
    class nonstatic_member_function;
}

Facilities to support old values in postconditions.

Postconditions can access old variable values (before body executions) for types tagged contract::copyable.


CONTRACT_OLDOF(variable_name)
namespace contract {
  template<typename T> class copyable;
  template<typename T> class copy;
}

Augmented object state internally used by the library.

namespace contract {
  class state;
}

Class template used to write contracts for static member functions.

namespace contract {
  template<typename F> class static_member_function;
}

Utilities to pass commas within macro parameters.


CONTRACT_WRAP_TYPE(parenthesized_type)
namespace contract {
  template<typename T> struct wrap;

  template<typename T> struct wrap<void(T)>;
}

PrevUpHomeNext