-
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
117 changed files
with
9,229 additions
and
0 deletions.
There are no files selected for viewing
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,3 @@ | ||
Copyright (C) 2009 Lorenzo Caminiti. | ||
Distributed under DBC++ Software License, Version 1.0 (see LICENSE_1_0.txt). | ||
|
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,7 @@ | ||
To install run `make install'. | ||
|
||
The library is composed of C/C++ header files only and does not need to be | ||
built. The library files are contained in the "include/" directory and they are: | ||
"include/dbc.hpp" Main file that includes entire library. | ||
"include/dbc/*" All other header files that implement the library. | ||
|
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,25 @@ | ||
Design By Contract for C++ (DBC++) Software License, Version 1.0 | ||
April 19th, 2009 | ||
|
||
Permission is hereby granted, free of charge, to any person or organization | ||
obtaining a copy of the software and accompanying documentation covered by | ||
this license (the "Software") to use, reproduce, display, distribute, | ||
execute, and transmit the Software, and to prepare derivative works of the | ||
Software, and to permit third-parties to whom the Software is furnished to | ||
do so, all subject to the following: | ||
|
||
The copyright notices in the Software and this entire statement, including | ||
the above license grant, this restriction and the following disclaimer, | ||
must be included in all copies of the Software, in whole or in part, and | ||
all derivative works of the Software, unless such copies or derivative | ||
works are solely in the form of machine-executable object code generated by | ||
a source language processor. | ||
|
||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR | ||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, | ||
FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT | ||
SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE | ||
FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE, | ||
ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER | ||
DEALINGS IN THE SOFTWARE. | ||
|
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,26 @@ | ||
|
||
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_: | ||
|
||
install: | ||
./bin/install | ||
|
||
example: force_ | ||
make -f build/Makefile.example | ||
|
||
test: force_ | ||
make -f build/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,24 @@ | ||
Design By Contract for C++ (DBC++) | ||
================================== | ||
|
||
The DBC++ library supports Design By Contract (DBC) for the C++ programming | ||
language. | ||
|
||
Essentially, all Eiffel programming language DBC features are supported by | ||
DBC++. Among others: | ||
1) "old" prefix in postconditions; | ||
2) Subcontracting; | ||
3) Optional contract compilation; | ||
4) Full integration with Doxygen. | ||
|
||
IMPORTANT: The library is still under development, its API should be | ||
considered experimental and subject to change. | ||
|
||
The documentation is yet to be written. Please look at the examples in the | ||
"example/" directory for illustrations on how to use the library. | ||
|
||
Run `make' to see how to build examples, test, install, etc. | ||
|
||
The library requires the C++ Boost library http://www.boost.org/. In particular | ||
Boost.Preprocessor and Boost.MPL are required. | ||
|
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,19 @@ | ||
RELEASE HISTORY | ||
=============== | ||
|
||
From current to oldest release. | ||
Release_Number ::= Major_Revision.Minor_Revision.SVN_Revision | ||
|
||
|
||
Release 0.1.55 (2009-04-19) | ||
--------------------------- | ||
|
||
Reorganized files to cleanup root directory. | ||
Added installation program. | ||
|
||
|
||
Release 0.1.50 (2009-04-19) | ||
--------------------------- | ||
|
||
First public release. | ||
|
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,82 @@ | ||
|
||
/** @todo[LC] Add tests to verify that const mem fun body cannot change obj | ||
state (compiler error) while non-const mem fun body can. */ | ||
|
||
/** @todo[LC] Make sure DBC library complies with STL exceptions safety rules | ||
(detructors don't throw, etc) -- read from C++ book. There is also a discussion | ||
of exception safety and invariant checking in Str97! */ | ||
|
||
/** @todo[LC] Shall self be available in constructor preconditions? | ||
Maybe not because technicall there's no object before exec of constrcutor body | ||
(and for example inv was not verified yet so using self of an obj on which inv | ||
is not checked could lead to strange errors and contract violation). However, | ||
then constrcutor preconditions will not be able to call mem functions | ||
(using self.some_function())... is this too much of a limitation to enforce? | ||
What does Eiffel do? Can you call object features from object's constructor | ||
preconditions? */ | ||
|
||
/** @todo[LC] Does "virtual inline" mean anything? Check in Str97 and remove it | ||
from fun.hpp in case it does not mean anything... */ | ||
|
||
/** @todo[LC] I have seen GCC internal segfaul error if DBC_CONFIG_MAX_ARGC is | ||
more than 3 some some of the DBC++ test programs... I wonder is the compiler | ||
gets confused by fun<...> instead of fun0, fun1, ... (maybe the template | ||
specialization with partial default argument is not properly supported...). */ | ||
|
||
/** @todo[LC] Add all @file w/ copyright info -- see what Boost copyright text | ||
says... Add reference to book from which examples where taken to all example | ||
doc comments. */ | ||
|
||
/** @todo[LC] Create a test for copyable where both class and args are declared | ||
copyable and not. */ | ||
|
||
/** @todo[LC] Write a test for required(). */ | ||
|
||
/** @todo[LC] When invoking parent's function directly from overriden function, | ||
must use DBC_BODY() to avoid infinite recursive checking of contract. See | ||
NameList example. | ||
@code | ||
struct B DBC_INHERIT_OBJECT(B) { | ||
virtual void f() DBC_MEM_FUN(..., {}) | ||
... | ||
}; | ||
struct D: public B DBC_TRAILING_OJECT(D) { | ||
virtual void f() DBC_MEM_FUN(..., { B::DBC_BODY(f)(); }) | ||
// This instead, will cause infinite contract checking recursion. | ||
virtual void f() DBC_MEM_FUN(..., { B::f(); }) | ||
... | ||
}; | ||
#endcode | ||
This is quite annoying as a small developper error in omitting DBC_BODY() in | ||
this context will result in a infinite recursion a run-time!!! Can I avoid this | ||
somehow??? Can I check it a compile-time? Can I make it work even if calling | ||
w/out DBC_BODY()? Also, what happens if the body function is not declared | ||
virtual but only the actual function is declared virtual? | ||
More in general than above todo, how shall DbC handle recursion? | ||
Shall contract checking always be disabled when a function recursively invokes | ||
itself? Maybe not, since it might invoke itself w/ different arguments and w/ | ||
obj in a different state (is it is not a const mem fun)... What is Eiffel | ||
policy on DbC and recursion? */ | ||
|
||
/** @todo[LC] When constrcutor contract is delegated to init() initializer, the | ||
contract does not show up in Doxygen... that is because constr (which are | ||
public) have no contract, while init() has the contract but it is private... | ||
is there a way around this? Since Doxygen reports the header files, the contract | ||
code (for init() also) is in the reported header but that's not ideal... It'd be | ||
nice if I could say in the Doxyfile to report init() (and del()) doc even if | ||
they are private... */ | ||
|
||
/** @todo[LC] Make library thread-safe if DBC_THREADING is #define. | ||
In this case: DbC++ will also require Boost.Threading. sync_<> must have mutex. | ||
dbc_global_checking_ must have a mutex. Exectuiong inv+require+body+inv+ensure | ||
must be atomic (sync'd by a mutex) so that effectivelly only 1 operation at the | ||
time for class can be exec among the operations w/ contracts. Consider impl | ||
waiting pre/post conditions. What would this do to performances? This will add | ||
quite a bit on sync at the class level but also at a global level via | ||
dbc_global_checking_... */ | ||
|
||
/** @todo[LC] Can I use Boost.MPL none and/or void to get rid of dbc::none_? */ | ||
|
||
/** @todo[LC] Fix all Boost.MPL static assertions in dbc::fun<>. Do I need to | ||
add any more static assertions? */ | ||
|
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 @@ | ||
Binary files, programs, and scripts. |
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,21 @@ | ||
#!/bin/bash | ||
|
||
echo "Design By Contract for C++ (DBC++) Library Installation" | ||
|
||
dest="" | ||
echo | ||
echo -en "Enter C/C++ header files directory [/use/include/]: " | ||
read dest | ||
if [ -z $dest ]; then dest="/usr/include/"; fi | ||
|
||
mkdir -p $dest && cp -R include/dbc* $dest | ||
ret=$? | ||
echo | ||
if [ $ret -ne 0 ]; then | ||
echo "ERROR: Unable to copy DBC++ header files to \"$dest\"." | ||
echo "Do you need to be root to access this directory?" | ||
else | ||
echo "DBC++ header files successfully copied to \"$dest\"." | ||
echo "Make sure this directory is in your C/C++ headers path (-I compiler option) and you are ready to use DBC++." | ||
fi | ||
|
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,19 @@ | ||
#!/bin/bash | ||
|
||
# Execute program given at command line. | ||
$@ | ||
|
||
# If program did not fail, return error code 1. | ||
if [ $? -eq 0 ]; then | ||
echo | ||
echo "must-fail: error: executed program did not fail as expected" | ||
echo | ||
exit 1; | ||
fi | ||
|
||
# Else (program failed), return OK code 0. | ||
echo | ||
echo "must-fail: executed program failed as expected -- returning OK" | ||
echo | ||
exit 0 | ||
|
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 codedoc/Doxyfile.example | ||
|
||
|
Oops, something went wrong.