-
Notifications
You must be signed in to change notification settings - Fork 27
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
295 changed files
with
17,515 additions
and
0 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
|
||
List of errors (as generated by GCC 4.2.4) and their common causes. | ||
|
||
error: ‘mem’ is not a template | ||
Make sure class_type is specified to be a template. | ||
MACRO API: (template)(class_type) | ||
CODE API: dbc::fun<>::mem::template class_type | ||
|
||
error: invalid use of non-static data member ‘...’ | ||
Did you forget to use self? | ||
|
||
error: no match for ‘...’ in ‘...’ | ||
Did you forget .now/.old postfix in postconditions? You must use these | ||
postfix in precondition for self as well as all function argument names | ||
(but not for 'result') | ||
|
||
error: ‘...’ has no member named ‘old’ | ||
Are you using old on either the class or on of the member function | ||
arguments without qualifing it with DBC_COPYABLE() (or dbc::copyable<>) | ||
first in the contract signature? | ||
|
||
error: macro "DBC_..." passed ... arguments, but takes just ... | ||
Does one or more passed macro parameter contain a comma "," not wrapped in | ||
parenthesis "()"? If so, wrap this macro parameter with DBC_MPARAM(). (This | ||
is the case for templates with more than 1 argument and for code blocks | ||
containing "," when they are passed as macro parameters.) | ||
|
||
warning: ‘class dbc::fun<...>...’ is already a friend of ‘...’ | ||
Ignore this. This is due to macro APIs automatically specifying same | ||
contract type as friend more than one time when you use DBC_MEM_FUN() | ||
multiple times for different member functions. It would be nice if your | ||
compiler could be configured to not generate just this one warning. This is | ||
the ONLY warning that the DBC++ library generates. | ||
|
||
error: ‘dbc_invariant_’ was not declared in this scope | ||
Did you forget to add DBC_INVARIANT(...) at the end of the class? | ||
|
||
Compile-time errors resulting from DBC static assertions (checks). | ||
|
||
error: ...DBC_ERROR_class_must_privately_inherit_from_dbc_object_... | ||
Did you forget to inherit (privately) from dbc::object<>? (Use | ||
DBC_INHERIT_OBJECT() or DBC_TRAILING_OBJECT() macros.) | ||
|
||
error: ...DBC_ERROR_missing_function_arguments_... | ||
Did you forget to specify the function arguments when using the macro APIs? | ||
Use "()" for no argument -- e.g., DBC_MEM_FUN(... (fun-name)() ...). | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
|
||
all: | ||
@echo "Design by Contract for C++ (DbC++)" | ||
@echo | ||
@echo "This library does not need to be build. It is composed only of " | ||
@echo "C/C++ header files contained int the \"./include/\" directory." | ||
@echo | ||
@echo "make install Install DbC++ files onto your system (you might " | ||
@echo " need to be root). This will prompt for path." | ||
@echo "make example Build example programs in \"./build/example/\" and" | ||
@echo " Doxygen documentation in \"./codedoc/example/\"." | ||
@echo "make test Build test programs in \"./build/test/\" and" | ||
@echo " Doxygen documentation in \"./codedoc/test/\"." | ||
exit 0 | ||
|
||
force_: | ||
|
||
example: force_ | ||
make -f Makefile.example | ||
|
||
test: force_ | ||
make -f Makefile.test | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,80 @@ | ||
# $Id$ # | ||
|
||
def:=-DDBC_ALL -DDBC_CONFIG_LOG_LEVEL=DBC_LOG_LEVEL_ALL | ||
|
||
inc:=-I./include | ||
src:=./example | ||
build:=./build/example | ||
codedoc:=./codedoc/example | ||
|
||
|
||
all: DBC_by_Example OO_SW_Construction CPP_Prog_Lang doc | ||
|
||
clean: | ||
rm -rf build | ||
|
||
force_: | ||
|
||
|
||
DBC_by_Example: CustomerManager Stack Dictionary SimpleQueue Courier NameList Observer Counter | ||
|
||
CustomerManager: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/CustomerManager/CustomerManager.cpp $(src)/DBC_by_Example/CustomerManager/main.cpp -o $(build)/CustomerManager | ||
|
||
Stack: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/Stack/main.cpp -o $(build)/Stack | ||
|
||
Dictionary: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/Dictionary/main.cpp -o $(build)/Dictionary | ||
|
||
SimpleQueue: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/SimpleQueue/main.cpp -o $(build)/SimpleQueue | ||
|
||
Courier: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/Courier/couriers.cpp $(src)/DBC_by_Example/Courier/main.cpp -o $(build)/Courier | ||
|
||
NameList: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/NameList/names.cpp $(src)/DBC_by_Example/NameList/main.cpp -o $(build)/NameList | ||
|
||
Observer: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/Observer/main.cpp -o $(build)/Observer | ||
|
||
Counter: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/DBC_by_Example/Counter/main.cpp -o $(build)/Counter | ||
|
||
|
||
OO_SW_Construction: Gcd Stack4 Stack3 | ||
|
||
Gcd: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/OO_SW_Construction/Gcd/main.cpp -o $(build)/Gcd | ||
|
||
Stack4: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/OO_SW_Construction/Stack4/main.cpp -o $(build)/Stack4 | ||
|
||
Stack3: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/OO_SW_Construction/Stack3/main.cpp -o $(build)/Stack3 | ||
|
||
|
||
CPP_Prog_Lang: String | ||
|
||
String: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/CPP_Prog_Lang/String/main.cpp -o $(build)/String | ||
|
||
|
||
doc: force_ | ||
mkdir -p $(codedoc) | ||
doxygen Doxyfile.example | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,91 @@ | ||
# $Id$ # | ||
|
||
def:=-DDBC_ALL -DDBC_CONFIG_LOG_LEVEL=DBC_LOG_LEVEL_ALL | ||
|
||
inc:=-I./include | ||
src:=./test | ||
build:=./build/test | ||
bin:=./bin | ||
codedoc:=./codedoc/test | ||
|
||
|
||
all: Construction Subcontracting Operators Checking doc | ||
|
||
clean: | ||
rm -rf $(build) | ||
|
||
force_: | ||
|
||
|
||
Construction: construction | ||
|
||
construction: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Construction/construction.cpp -o $(build)/construction | ||
|
||
|
||
Subcontracting: base_class base_template class_subcontracts_template template_subcontracts_template | ||
|
||
base_class: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Subcontracting/base_class.cpp -o $(build)/base_class | ||
|
||
class_subcontracts_class: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Subcontracting/class_subcontracts_class.cpp -o $(build)/class_subcontracts_class | ||
|
||
template_subcontracts_class: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Subcontracting/template_subcontracts_class.cpp -o $(build)/template_subcontracts_class | ||
|
||
base_template: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Subcontracting/base_template.cpp -o $(build)/base_template | ||
|
||
class_subcontracts_template: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Subcontracting/class_subcontracts_template.cpp -o $(build)/class_subcontracts_template | ||
|
||
template_subcontracts_template: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Subcontracting/template_subcontracts_template.cpp -o $(build)/template_subcontracts_template | ||
|
||
|
||
Operators: operators | ||
|
||
operators: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Operators/operators.cpp -o $(build)/operators | ||
|
||
|
||
Checking: checking | ||
|
||
checking: | ||
mkdir -p $(build) | ||
# Compile this test with different DBC_CHECKING... levels. | ||
# Verbose log DBC_CONFIG_LOG_LEVEL set by program code itself. | ||
g++ -Wall $(inc) -DDBC_NO $(src)/Checking/checking.cpp -o $(build)/checking-no | ||
g++ -Wall $(inc) -DDBC_ALL $(src)/Checking/checking.cpp -o $(build)/checking-all | ||
# Only one at the time | ||
g++ -Wall $(inc) -DDBC_CHECK_REQUIRE $(src)/Checking/checking.cpp -o $(build)/checking-require_only | ||
g++ -Wall $(inc) -DDBC_CHECK_ENSURE $(src)/Checking/checking.cpp -o $(build)/checking-ensure_only | ||
g++ -Wall $(inc) -DDBC_CHECK_INVARIANT $(src)/Checking/checking.cpp -o $(build)/checking-invariant_only | ||
# Eiffel like combinations. | ||
g++ -Wall $(inc) -DDBC_CHECK_REQUIRE $(src)/Checking/checking.cpp -o $(build)/checking-require | ||
g++ -Wall $(inc) -DDBC_CHECK_REQUIRE -DDBC_CHECK_ENSURE $(src)/Checking/checking.cpp -o $(build)/checking-require_and_ensure | ||
g++ -Wall $(inc) -DDBC_CHECK_REQUIRE -DDBC_CHECK_ENSURE -DDBC_CHECK_INVARIANT $(src)/Checking/checking.cpp -o $(build)/checking-require_ensure_and_invariant | ||
# Code documentation. | ||
g++ -Wall $(inc) -DDBC_DOC $(src)/Checking/checking.cpp -o $(build)/checking-doc | ||
# Invalid combinations -- compilation must fail. | ||
$(bin)/must-fail g++ -Wall $(inc) -DDBC $(src)/Checking/checking.cpp -o $(build)/checking-dbc | ||
$(bin)/must-fail g++ -Wall $(inc) -DDBC_NO -DDBC_ALL $(src)/Checking/checking.cpp -o $(build)/checking-no_and_all | ||
$(bin)/must-fail g++ -Wall $(inc) -DDBC_DOC -DDBC_ALL $(src)/Checking/checking.cpp -o $(build)/checking-doc_and_all | ||
|
||
|
||
doc: force_ | ||
mkdir -p $(build) | ||
g++ -Wall $(inc) $(def) $(src)/Doc/doc.cpp -o $(build)/doc | ||
mkdir -p $(codedoc) | ||
doxygen Doxyfile.test | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,109 @@ | ||
|
||
/** @note boost::mpl::is_copyable<> could not be used to replace | ||
dbc::copyable<> because Boost's is_copyable<> only works for built-in types. | ||
For user defined types, Boost's is_copyable always returns false unless special | ||
compiler support is provided (and GCC does not provide support for this, | ||
probably only VC++ supports this at the moment...). */ | ||
|
||
/** @note Inheriting from a dbc::object<> base class allows to provide | ||
assertion checking state, mutex, etc. However, the invariant cannot be made | ||
pure virtual function of dbc::object<> otherwise the invariant call will always | ||
be ambiguis when subcontracting -- I did try this! | ||
Note, since dbc::object<> is a template, they are all different from eavery | ||
class type so the inheritance tree is modified by no common anchestor is | ||
intorduced and dbc::object<> should be private base anyway -- so this | ||
modification of inheritance tree is OK as is does not change public APIs. | ||
However, contract cannot access class-type directly from dbc::object because | ||
in order to call dbc::object<C>::class_type, the contract will still need to | ||
specify C -- so class-type must still be specified for each contract mem fun. */ | ||
|
||
/** @note Wanted to provide def constr for all contract class fun, fun::mem, etc | ||
so they are easier to use. In particular if a mem var of a contract class type | ||
is declared, C++ will init automatically using it's default constr. This feature | ||
is currently not used in the library (as contracts are init manually in the | ||
fun declaration that then call operator()) but it might turn out to be handy in | ||
future. */ | ||
|
||
/** @note If only DBC_CHECK_INVARIANT and DBC_CHECK_REQUIRE are #define, DbC++ | ||
can be used to impl invariant checking framework similar to the only proposed | ||
in Str97 (see example/CPP_Prog_Lang/String). In Str97, precondition checking is | ||
not directly discussed (it is actually discouraged in a later section) but | ||
String::operator[] has a check on the range of its index argument that is very | ||
naturally handled with a precondition -- so DbC++ example have implemented that | ||
index range check as a precondition. */ | ||
|
||
/** @note declaring require(), ensure(), and dbc_invariant_() pure virtual | ||
forces the user to define them correctly at compile time. Having them with | ||
params allow user to only use correct param (no old or result in require()) | ||
and to name args as original function args. */ | ||
|
||
/** @note Chosen abbreviation "mem" for member and "fun" for function to follow | ||
C++ STL conventions of std::mem_fun. Chosen "constr" and "destr" | ||
abbreviations trying to follow similar abbreviation philosofy of STL. */ | ||
|
||
/** @note DBC_CONFIG_ macros follow name convention and semantics of | ||
BOOST_PP_CONFIG_ macros. */ | ||
|
||
/** @note Contracts are functor as they provide call operator() that checks | ||
contract and inokes body (this seemed a natural choise since this is indeed | ||
the function call). */ | ||
|
||
/** @note DBC_CONFIG_ENABLE_XYZ_ASSERTIONS do not remove assertions from obj | ||
code. They only run on/off run-time checking of relative assertions (but the | ||
assertions are always compiled). Use DBC_CHECK_XYZ to remove pre/post/inv | ||
assertions (at this regardless of if they throw/exit/terminate) from obj | ||
code. */ | ||
|
||
/** @note DBC_NO and DBC_ALL override #definitions of single DBC_CEHCKING (if | ||
any). */ | ||
|
||
/** @note DbC++ also impl a simple version of Eiffel loop invariant checking | ||
(see example/OO_SW_Contruction/Gcd). This hasn't been tested much... */ | ||
|
||
/** @note Different stylistic naming convetions have been used: C/C++ STL for | ||
DBC library and test, Str97 for Str97 examples, Java-like CaMeL for DBC books | ||
examples. This was to see how DBC will look when in code with different | ||
styles (common C++ situation). */ | ||
|
||
/** @note DBC_CONFIG_MAX_ARGC is set to 5 by default. It can be increased | ||
(probably up to BOOST_PP_MAX_MAG around 255) but it will significantly increase | ||
compilation time. Use only a reasonable number based on the number of fun args | ||
you have (for which you need a contract). */ | ||
|
||
/** @note See examples: Stack4 for general good DBC and library usage; NameList | ||
for inheritance; Observer for more complex inheritance and library usage (where | ||
some classes have contracts and others don't -- but I prefer to have contracts | ||
for all classes and all of their mem-fun/constr/destr). */ | ||
|
||
/** @note If when subcontracting DBC_BASE is omitted then base contract is | ||
ignored. This might be inline with C++ "freedom" given to the programmer, but | ||
in general you must NOT do that... as you will be braking your parent's contract | ||
by not inheriting it. */ | ||
|
||
/** @note Do not enter arg default value in contract (only arg-type and | ||
arg-name). */ | ||
|
||
/** @note require/ensure declared pure virtual (instead of {}) so compiler error | ||
if you miss type them (e.g., incorrect const or post<> for one of the args). | ||
This requires a bit more work from the programmer even for contracts with no | ||
pre/post conditions but allow to catch errors in the contract at | ||
compile-time. */ | ||
|
||
/** @note In quite a few places in the impl (macro, fun, etc) we need to | ||
add and them remove copyable etc because if types do not have excaly the same | ||
signature the compiler will not match them to be the same for templates (as for | ||
templates compiler need to wait and eval the type expression lazily...). */ | ||
|
||
/** @note Argument types are indexed from 0 to n-1 like in Boost.FunctionType | ||
they are returned as Boost.MPL sequence that goes from 0 to n-1. Using symbols | ||
indexed from 1 to n (A1...An, arg1_type...argn_type, etc) would have increased | ||
(but not much) preprocessing time because Boost.Preprocessor enum and | ||
repetition go from 0 to n-1 by default. */ | ||
|
||
/** @note Destructor do not subcontract (i.e., their contract do not accept | ||
DBC_BASE() and fun<>::destr<> does not accept base contract type B param). This | ||
is beacuse C++ will automatically invoke base class destructors (with its | ||
contract that cheks inv if base class destructor has a contract). See the | ||
Courier example: When DifferentCourier is destroied, the base class Courier | ||
destructor is automatically invoked. */ | ||
|
Oops, something went wrong.