From 570b283bf20f73d5eb7dcd589a479e3f076ba073 Mon Sep 17 00:00:00 2001 From: Lorenzo Caminiti Date: Sun, 19 Oct 2014 23:44:29 -0700 Subject: [PATCH] tested access on msvc, gcc, clang, and wave --- .gitignore | 9 + Jamroot | 19 + example/Jamfile.v2 | 422 --------------- example/cline90/calendar.cpp | 74 --- example/cline90/stack.cpp | 139 ----- example/cline90/vector.hpp | 73 --- example/cline90/vector_app.hpp | 73 --- example/cline90/vector_main.cpp | 24 - example/cline90/vstack.cpp | 144 ----- .../assertion_complexity_factorial.cpp | 47 -- .../assertion_requirements_push_back.cpp | 77 --- .../contracts/assertion_statement_ialloc.cpp | 42 -- example/contracts/blockinv_loopvar_gcd.cpp | 51 -- example/contracts/body_natural.cpp | 19 - example/contracts/body_natural.hpp | 78 --- example/contracts/body_natural_impl.hpp | 39 -- example/contracts/broken_handler_sqrt.cpp | 92 ---- example/contracts/class_ivector.cpp | 89 ---- example/contracts/class_template_vector.cpp | 88 --- .../contracts/class_template_vector_seq.cpp | 88 --- .../class_template_vector_seq_nova.cpp | 10 - example/contracts/const_assertion_number.cpp | 47 -- .../const_assertion_number_global_error.cpp | 50 -- .../const_assertion_number_static_error.cpp | 50 -- .../const_select_assertion_factorial.cpp | 42 -- ...const_select_assertion_factorial_error.cpp | 46 -- example/contracts/contract_failure.cpp | 474 ----------------- example/contracts/copy_inc.cpp | 76 --- .../contracts/default_subcontracting_base.cpp | 34 -- example/contracts/exception_array.cpp | 75 --- example/contracts/friend_counter.cpp | 106 ---- .../contracts/function_template_postinc.cpp | 35 -- example/contracts/has_oldof_inc.cpp | 68 --- .../macro_commas_symbols_integral_map.cpp | 103 ---- .../macro_commas_symbols_integral_map_seq.cpp | 96 ---- ...o_commas_symbols_integral_map_seq_nova.cpp | 10 - example/contracts/member_operator_string.cpp | 136 ----- example/contracts/nested_class_bitset.cpp | 112 ---- example/contracts/no_contract_ivector.cpp | 48 -- example/contracts/no_contract_postinc.cpp | 27 - example/contracts/no_pre_post_postinc.cpp | 30 -- example/contracts/nova.hpp | 21 - .../contracts/params_funcptr_array_apply.cpp | 50 -- example/contracts/params_postinc.cpp | 37 -- example/contracts/post_also_postinc.cpp | 34 -- example/contracts/pre_only_postinc.cpp | 30 -- example/contracts/push_back.cpp | 56 -- example/contracts/push_back_lines.cpp | 47 -- example/contracts/push_back_npaper.cpp | 47 -- example/contracts/pushable.hpp | 40 -- example/contracts/pushable_seq.hpp | 40 -- .../contracts/select_assertion_factorial.cpp | 37 -- .../contracts/static_assertion_memcopy.cpp | 43 -- .../static_contract_instance_counter.cpp | 77 --- example/contracts/subcontract_identifiers.cpp | 115 ---- .../subcontract_pre_natural_failure.cpp | 69 --- example/contracts/template_params.cpp | 64 --- .../template_specializations_vector.cpp | 128 ----- example/contracts/typed_counter.cpp | 41 -- .../volatile_contract_shared_instance.cpp | 63 --- example/meyer97/gcd.cpp | 42 -- example/meyer97/gcd.e | 42 -- example/meyer97/maxarray.cpp | 44 -- example/meyer97/stack3.cpp | 164 ------ example/meyer97/stack4.e | 211 -------- example/meyer97/stack4.hpp | 212 -------- example/meyer97/stack4_main.cpp | 27 - example/mitchell02/counter/counter.hpp | 59 --- .../mitchell02/counter/decrement_button.hpp | 76 --- example/mitchell02/counter/push_button.hpp | 66 --- example/mitchell02/counter_main.cpp | 64 --- example/mitchell02/courier.cpp | 49 -- example/mitchell02/courier.hpp | 133 ----- example/mitchell02/courier_main.cpp | 23 - example/mitchell02/customer_manager.cpp | 45 -- example/mitchell02/customer_manager.hpp | 109 ---- example/mitchell02/customer_manager_main.cpp | 26 - example/mitchell02/dictionary.cpp | 98 ---- example/mitchell02/name_list.cpp | 40 -- example/mitchell02/name_list.hpp | 99 ---- example/mitchell02/name_list_main.cpp | 27 - example/mitchell02/observer/observer.hpp | 46 -- example/mitchell02/observer/subject.hpp | 151 ------ example/mitchell02/observer_main.cpp | 74 --- example/mitchell02/simple_queue.cpp | 170 ------ example/mitchell02/stack.cpp | 110 ---- example/n1962/block_invariant.cpp | 25 - example/n1962/circle.cpp | 57 -- example/n1962/equal.hpp | 29 - example/n1962/equal_main.cpp | 26 - example/n1962/equal_not.hpp | 29 - example/n1962/factorial.cpp | 56 -- example/n1962/sqrt.cpp | 31 -- example/n1962/sqrt.d | 31 -- example/n1962/sum.cpp | 18 - example/n1962/sum.hpp | 22 - example/n1962/sum_main.cpp | 20 - example/n1962/vector.cpp | 39 -- example/n1962/vector.hpp | 499 ------------------ example/n1962/vector_npaper.hpp | 499 ------------------ example/n2081/add.cpp | 20 - example/n2081/add.hpp | 45 -- example/n2081/add_error.cpp | 25 - example/n2081/advance.cpp | 98 ---- example/n2081/apply.cpp | 70 --- example/n2081/convert.cpp | 19 - example/n2081/convert.hpp | 26 - example/n2081/convert_error.cpp | 18 - example/n2081/count.cpp | 48 -- example/n2081/deref.cpp | 43 -- example/n2081/equal.cpp | 20 - example/n2081/equal.hpp | 27 - example/n2081/equal_error.cpp | 24 - example/n2081/find.cpp | 22 - example/n2081/find.hpp | 43 -- example/n2081/find_error.cpp | 28 - example/n2081/for_each.cpp | 52 -- example/n2081/less_eq.cpp | 36 -- example/n2081/min.cpp | 20 - example/n2081/min.hpp | 31 -- example/n2081/min_error.cpp | 24 - example/n2081/transform.cpp | 68 --- example/stroustrup97/string.cpp | 33 -- example/stroustrup97/string.hpp | 81 --- example/stroustrup97/string_main.cpp | 47 -- tool/boost_setup/cygwin-boost-env.sh | 15 - tool/boost_setup/cygwin-user-config.jam | 10 - tool/boost_setup/linux-boost-env.sh | 15 - tool/boost_setup/linux-user-config.jam | 19 - tool/boost_setup/windows-boost-env.bat | 17 - tool/boost_setup/windows-user-config.jam | 24 - tool/copyright_header.py | 121 ----- tool/release_instructions.txt | 54 -- tool/sh.py | 118 ----- wave.cfg | 9 +- 135 files changed, 36 insertions(+), 9323 deletions(-) create mode 100644 Jamroot delete mode 100644 example/Jamfile.v2 delete mode 100644 example/cline90/calendar.cpp delete mode 100644 example/cline90/stack.cpp delete mode 100644 example/cline90/vector.hpp delete mode 100644 example/cline90/vector_app.hpp delete mode 100644 example/cline90/vector_main.cpp delete mode 100644 example/cline90/vstack.cpp delete mode 100644 example/contracts/assertion_complexity_factorial.cpp delete mode 100644 example/contracts/assertion_requirements_push_back.cpp delete mode 100644 example/contracts/assertion_statement_ialloc.cpp delete mode 100644 example/contracts/blockinv_loopvar_gcd.cpp delete mode 100644 example/contracts/body_natural.cpp delete mode 100644 example/contracts/body_natural.hpp delete mode 100644 example/contracts/body_natural_impl.hpp delete mode 100644 example/contracts/broken_handler_sqrt.cpp delete mode 100644 example/contracts/class_ivector.cpp delete mode 100644 example/contracts/class_template_vector.cpp delete mode 100644 example/contracts/class_template_vector_seq.cpp delete mode 100644 example/contracts/class_template_vector_seq_nova.cpp delete mode 100644 example/contracts/const_assertion_number.cpp delete mode 100644 example/contracts/const_assertion_number_global_error.cpp delete mode 100644 example/contracts/const_assertion_number_static_error.cpp delete mode 100644 example/contracts/const_select_assertion_factorial.cpp delete mode 100644 example/contracts/const_select_assertion_factorial_error.cpp delete mode 100644 example/contracts/contract_failure.cpp delete mode 100644 example/contracts/copy_inc.cpp delete mode 100644 example/contracts/default_subcontracting_base.cpp delete mode 100644 example/contracts/exception_array.cpp delete mode 100644 example/contracts/friend_counter.cpp delete mode 100644 example/contracts/function_template_postinc.cpp delete mode 100644 example/contracts/has_oldof_inc.cpp delete mode 100644 example/contracts/macro_commas_symbols_integral_map.cpp delete mode 100644 example/contracts/macro_commas_symbols_integral_map_seq.cpp delete mode 100644 example/contracts/macro_commas_symbols_integral_map_seq_nova.cpp delete mode 100644 example/contracts/member_operator_string.cpp delete mode 100644 example/contracts/nested_class_bitset.cpp delete mode 100644 example/contracts/no_contract_ivector.cpp delete mode 100644 example/contracts/no_contract_postinc.cpp delete mode 100644 example/contracts/no_pre_post_postinc.cpp delete mode 100644 example/contracts/nova.hpp delete mode 100644 example/contracts/params_funcptr_array_apply.cpp delete mode 100644 example/contracts/params_postinc.cpp delete mode 100644 example/contracts/post_also_postinc.cpp delete mode 100644 example/contracts/pre_only_postinc.cpp delete mode 100644 example/contracts/push_back.cpp delete mode 100644 example/contracts/push_back_lines.cpp delete mode 100644 example/contracts/push_back_npaper.cpp delete mode 100644 example/contracts/pushable.hpp delete mode 100644 example/contracts/pushable_seq.hpp delete mode 100644 example/contracts/select_assertion_factorial.cpp delete mode 100644 example/contracts/static_assertion_memcopy.cpp delete mode 100644 example/contracts/static_contract_instance_counter.cpp delete mode 100644 example/contracts/subcontract_identifiers.cpp delete mode 100644 example/contracts/subcontract_pre_natural_failure.cpp delete mode 100644 example/contracts/template_params.cpp delete mode 100644 example/contracts/template_specializations_vector.cpp delete mode 100644 example/contracts/typed_counter.cpp delete mode 100644 example/contracts/volatile_contract_shared_instance.cpp delete mode 100644 example/meyer97/gcd.cpp delete mode 100644 example/meyer97/gcd.e delete mode 100644 example/meyer97/maxarray.cpp delete mode 100644 example/meyer97/stack3.cpp delete mode 100644 example/meyer97/stack4.e delete mode 100644 example/meyer97/stack4.hpp delete mode 100644 example/meyer97/stack4_main.cpp delete mode 100644 example/mitchell02/counter/counter.hpp delete mode 100644 example/mitchell02/counter/decrement_button.hpp delete mode 100644 example/mitchell02/counter/push_button.hpp delete mode 100644 example/mitchell02/counter_main.cpp delete mode 100644 example/mitchell02/courier.cpp delete mode 100644 example/mitchell02/courier.hpp delete mode 100644 example/mitchell02/courier_main.cpp delete mode 100644 example/mitchell02/customer_manager.cpp delete mode 100644 example/mitchell02/customer_manager.hpp delete mode 100644 example/mitchell02/customer_manager_main.cpp delete mode 100644 example/mitchell02/dictionary.cpp delete mode 100644 example/mitchell02/name_list.cpp delete mode 100644 example/mitchell02/name_list.hpp delete mode 100644 example/mitchell02/name_list_main.cpp delete mode 100644 example/mitchell02/observer/observer.hpp delete mode 100644 example/mitchell02/observer/subject.hpp delete mode 100644 example/mitchell02/observer_main.cpp delete mode 100644 example/mitchell02/simple_queue.cpp delete mode 100644 example/mitchell02/stack.cpp delete mode 100644 example/n1962/block_invariant.cpp delete mode 100644 example/n1962/circle.cpp delete mode 100644 example/n1962/equal.hpp delete mode 100644 example/n1962/equal_main.cpp delete mode 100644 example/n1962/equal_not.hpp delete mode 100644 example/n1962/factorial.cpp delete mode 100644 example/n1962/sqrt.cpp delete mode 100644 example/n1962/sqrt.d delete mode 100644 example/n1962/sum.cpp delete mode 100644 example/n1962/sum.hpp delete mode 100644 example/n1962/sum_main.cpp delete mode 100644 example/n1962/vector.cpp delete mode 100644 example/n1962/vector.hpp delete mode 100644 example/n1962/vector_npaper.hpp delete mode 100644 example/n2081/add.cpp delete mode 100644 example/n2081/add.hpp delete mode 100644 example/n2081/add_error.cpp delete mode 100644 example/n2081/advance.cpp delete mode 100644 example/n2081/apply.cpp delete mode 100644 example/n2081/convert.cpp delete mode 100644 example/n2081/convert.hpp delete mode 100644 example/n2081/convert_error.cpp delete mode 100644 example/n2081/count.cpp delete mode 100644 example/n2081/deref.cpp delete mode 100644 example/n2081/equal.cpp delete mode 100644 example/n2081/equal.hpp delete mode 100644 example/n2081/equal_error.cpp delete mode 100644 example/n2081/find.cpp delete mode 100644 example/n2081/find.hpp delete mode 100644 example/n2081/find_error.cpp delete mode 100644 example/n2081/for_each.cpp delete mode 100644 example/n2081/less_eq.cpp delete mode 100644 example/n2081/min.cpp delete mode 100644 example/n2081/min.hpp delete mode 100644 example/n2081/min_error.cpp delete mode 100644 example/n2081/transform.cpp delete mode 100644 example/stroustrup97/string.cpp delete mode 100644 example/stroustrup97/string.hpp delete mode 100644 example/stroustrup97/string_main.cpp delete mode 100644 tool/boost_setup/cygwin-boost-env.sh delete mode 100644 tool/boost_setup/cygwin-user-config.jam delete mode 100644 tool/boost_setup/linux-boost-env.sh delete mode 100644 tool/boost_setup/linux-user-config.jam delete mode 100644 tool/boost_setup/windows-boost-env.bat delete mode 100644 tool/boost_setup/windows-user-config.jam delete mode 100644 tool/copyright_header.py delete mode 100644 tool/release_instructions.txt delete mode 100644 tool/sh.py diff --git a/.gitignore b/.gitignore index b8bd026..890aba7 100644 --- a/.gitignore +++ b/.gitignore @@ -26,3 +26,12 @@ *.exe *.out *.app + +# Boost.Jam outputs +bin/ + +# Boost.Wave outputs +pp.cpp +pp.dbg +pp.cnt + diff --git a/Jamroot b/Jamroot new file mode 100644 index 0000000..2ed6022 --- /dev/null +++ b/Jamroot @@ -0,0 +1,19 @@ + +import os ; + +if ! [ os.environ BOOST_ROOT ] +{ + exit "Error: Set BOOST_ROOT environment variable to Boost root directory" ; +} +local BOOST_ROOT = [ os.environ BOOST_ROOT ] ; +echo "Using Boost libraries from:" $(BOOST_ROOT) ; + +use-project boost : $(BOOST_ROOT) ; + +project + : requirements + "./include" + $(BOOST_ROOT) + $(BOOST_ROOT)/stage/lib + ; + diff --git a/example/Jamfile.v2 b/example/Jamfile.v2 deleted file mode 100644 index 410b3df..0000000 --- a/example/Jamfile.v2 +++ /dev/null @@ -1,422 +0,0 @@ - -# Copyright (C) 2008-2012 Lorenzo Caminiti -# Distributed under the Boost Software License, Version 1.0 -# (see accompanying file LICENSE_1_0.txt or a copy at -# http://www.boost.org/LICENSE_1_0.txt) -# Home at http://sourceforge.net/projects/contractpp - -import testing ; -import python ; -import type ; -import generators ; - -echo """ -Usage: bjam [TARGET]... [BJAM_OPTION]... -By default, build examples from all directories and with all contract on/off -combinations (this takes a long time). Targets `all_on` and `all_off` build -examples from all directories but only with contracts on and off respectively. -Target `dirname` build examples only in the given directory but with all -contracts on. See TARGET below for a complete list of targets. -Other Bjam options (`-q`, `--clean`, etc) are specified as usual. - -TARGET - [noflags][_dirname][_filename] | dirname_onoff | all_on | all_off -noflags - Turn off specific contract combinations using `no[e][o][i][b][l]`: - noe | noo | noi | nob | nol | noeo | noei | nooi | nobl | noeoi | noeoibl - Where: - e = prEconditions o = pOstconditions i = class Invariants - b = Block invariants l = Loop variants - Turn off no contract when `noflags` is not specified. (Longer flag names - would have caused too long build file names on some OS.) -dirname - Build the specified directory (contracts on if `noflags` not specified). -filename - Build the specified file (contracts on if `noflags` not specified). -dirname_onoff - Build in specified directory name with all contract on/off combinations. -all_on - Build all directories but with all contracts on. -all_off - Build all directories but with all contracts off. - -EXAMPLES - bjam contracts_push_back # only contracts/push_back, contracts on - bjam noeo_contracts_push_back # contract/push_back, pre and post off - bjam contracts # all in contracts/, contracts on - bjam noeo_contracts # all in contracts/, pre and post off - bjam contracts_onoff # all in contracts/, all on/off combinations - bjam all_on # all directories, contracts on - bjam # all directories, all on/off combinations -""" ; - -# Directory Builds # - -# Build from the "contracts" directory. -rule dir-contracts ( name : defines * ) -{ - test-suite $(name) : - [ dir-run contracts : assertion_complexity_factorial - : $(name) : $(defines) ] - [ dir-run contracts : assertion_requirements_push_back - : $(name) : $(defines) ] - [ dir-run contracts : assertion_statement_ialloc - : $(name) : $(defines) ] - [ dir-run contracts : blockinv_loopvar_gcd : $(name) : $(defines) ] - [ dir-run contracts : body_natural : $(name) : $(defines) ] - [ dir-run contracts : broken_handler_sqrt : $(name) : $(defines) ] - [ dir-run contracts : class_ivector : $(name) : $(defines) ] - [ dir-run contracts : class_template_vector : $(name) : $(defines) ] - [ dir-run contracts : class_template_vector_seq - : $(name) : $(defines) ] - [ dir-run contracts : class_template_vector_seq_nova - : $(name) : $(defines) ] - [ dir-run contracts : const_assertion_number : $(name) : $(defines) ] - [ dir-run contracts : contract_failure : $(name) : $(defines) ] - [ dir-err contracts : const_assertion_number_global_error - : $(name) : $(defines) ] - [ dir-err contracts : const_assertion_number_static_error - : $(name) : $(defines) ] - [ dir-run contracts : const_select_assertion_factorial - : $(name) : $(defines) ] - [ dir-err contracts : const_select_assertion_factorial_error - : $(name) : $(defines) ] - [ dir-run contracts : copy_inc : $(name) : $(defines) ] - [ dir-run contracts : default_subcontracting_base - : $(name) : $(defines) ] - [ dir-run contracts : exception_array : $(name) : $(defines) ] - [ dir-run contracts : friend_counter : $(name) : $(defines) ] - [ dir-run contracts : function_template_postinc : $(name) : $(defines) ] - [ dir-run contracts : has_oldof_inc : $(name) : $(defines) ] - [ dir-run contracts : macro_commas_symbols_integral_map - : $(name) : $(defines) ] - [ dir-run contracts : macro_commas_symbols_integral_map_seq - : $(name) : $(defines) ] - [ dir-run contracts : macro_commas_symbols_integral_map_seq_nova - : $(name) : $(defines) ] - [ dir-run contracts : member_operator_string : $(name) : $(defines) ] - [ dir-run contracts : nested_class_bitset : $(name) : $(defines) ] - [ dir-run contracts : no_contract_ivector : $(name) : $(defines) ] - [ dir-run contracts : no_contract_postinc : $(name) : $(defines) ] - [ dir-run contracts : no_pre_post_postinc : $(name) : $(defines) ] - [ dir-run contracts : params_funcptr_array_apply - : $(name) : $(defines) ] - [ dir-run contracts : params_postinc : $(name) : $(defines) ] - [ dir-run contracts : post_also_postinc : $(name) : $(defines) ] - [ dir-run contracts : pre_only_postinc : $(name) : $(defines) ] - [ dir-run contracts : push_back : $(name) : $(defines) ] - [ dir-run contracts : select_assertion_factorial - : $(name) : $(defines) ] - [ dir-run contracts : static_assertion_memcopy : $(name) : $(defines) ] - [ dir-run contracts : static_contract_instance_counter - : $(name) : $(defines) ] - [ dir-run contracts : subcontract_identifiers : $(name) : $(defines) ] - [ dir-run contracts : subcontract_pre_natural_failure - : $(name) : $(defines) ] - [ dir-run contracts : template_params : $(name) : $(defines) ] - [ dir-run contracts : template_specializations_vector - : $(name) : $(defines) ] - [ dir-run contracts : typed_counter : $(name) : $(defines) ] - [ dir-run contracts : volatile_contract_shared_instance - : $(name) : $(defines) ] - ; -} - -# Build from the "virtual_specifiers" directory. -rule dir-virtual_specifiers ( name : defines * ) -{ - test-suite $(name) : - [ dir-run virtual_specifiers : final_class : $(name) : $(defines) ] - [ dir-err virtual_specifiers : final_class_error - : $(name) : $(defines) ] - [ dir-run virtual_specifiers : final_member : $(name) : $(defines) ] - [ dir-err virtual_specifiers : final_member_error - : $(name) : $(defines) ] - [ dir-run virtual_specifiers : new_member : $(name) : $(defines) ] - [ dir-err virtual_specifiers : new_member_error : $(name) : $(defines) ] - [ dir-run virtual_specifiers : override_member - : $(name) : $(defines) ] - [ dir-err virtual_specifiers : override_member_error - : $(name) : $(defines) ] - ; -} - -# Build from the "concepts" directory. -rule dir-concepts ( name : defines * ) -{ - test-suite $(name) : - [ dir-run concepts : class_member_concept_vector - : $(name) : $(defines) ] - [ dir-err concepts : class_member_concept_vector_error - : $(name) : $(defines) ] - [ dir-err concepts : class_member_concept_vector_constructor_error - : $(name) : $(defines) ] - [ dir-err concepts : class_member_concept_vector_member_error - : $(name) : $(defines) ] - [ dir-run concepts : free_concept_operator_preinc - : $(name) : $(defines) ] - [ dir-err concepts : free_concept_operator_preinc_error - : $(name) : $(defines) ] - ; -} - -# Build from the "named_parameters" directory. -rule dir-named_parameters ( name : defines * ) -{ - test-suite $(name) : - [ dir-run named_parameters : constructor_named_params_family - : $(name) : $(defines) ] - [ dir-run named_parameters : member_named_params_callable2 - : $(name) : $(defines) ] - [ dir-run named_parameters : named_param_identifiers_failure - : $(name) : $(defines) ] - [ dir-run named_parameters : named_param_identifiers_positive - : $(name) : $(defines) ] - [ dir-run named_parameters : named_params_dfs - : $(name) : $(defines) ] - [ dir-pymodule named_parameters : deduced_params_pydef - : $(name) : $(defines) ] - [ dir-pymodule named_parameters : named_template_params_pyclass - : $(name) : $(defines) ] - ; -} - -# Build from the "n1962" directory. -rule dir-n1962 ( name : defines * ) -{ - test-suite $(name) : - [ dir-run n1962 : block_invariant : $(name) : $(defines) ] - [ dir-run n1962 : circle : $(name) : $(defines) ] - [ run n1962/equal_main.cpp : : : $(defines) : $(name)_equal ] - [ dir-run n1962 : factorial : $(name) : $(defines) ] - [ dir-run n1962 : sqrt : $(name) : $(defines) ] - [ run n1962/sum.cpp n1962/sum_main.cpp : : : $(defines) : $(name)_sum ] - [ dir-run n1962 : vector : $(name) : $(defines) ] - ; -} - -# Build from the "n2081" directory. -rule dir-n2081 ( name : defines * ) -{ - test-suite $(name) : - [ dir-run n2081 : add : $(name) : $(defines) ] - [ dir-err n2081 : add_error : $(name) : $(defines) ] - [ dir-run n2081 : advance : $(name) : $(defines) ] - [ dir-run n2081 : apply : $(name) : $(defines) ] - [ dir-run n2081 : convert : $(name) : $(defines) ] - [ dir-err n2081 : convert_error : $(name) : $(defines) ] - [ dir-run n2081 : count : $(name) : $(defines) ] - [ dir-run n2081 : deref : $(name) : $(defines) ] - [ dir-run n2081 : equal : $(name) : $(defines) ] - [ dir-err n2081 : equal_error : $(name) : $(defines) ] - [ dir-run n2081 : find : $(name) : $(defines) ] - [ dir-err n2081 : find_error : $(name) : $(defines) ] - [ dir-run n2081 : for_each : $(name) : $(defines) ] - [ dir-run n2081 : less_eq : $(name) : $(defines) ] - [ dir-run n2081 : min : $(name) : $(defines) ] - [ dir-err n2081 : min_error : $(name) : $(defines) ] - [ dir-run n2081 : transform : $(name) : $(defines) ] - ; -} - -# Build from the "meyer97" directory. -rule dir-meyer97 ( name : defines * ) -{ - test-suite $(name) : - [ dir-run meyer97 : gcd : $(name) : $(defines) ] - [ dir-run meyer97 : maxarray : $(name) : $(defines) ] - [ dir-run meyer97 : stack3 : $(name) : $(defines) ] - [ run meyer97/stack4_main.cpp : : : $(defines) : $(name)_stack4 ] - ; -} - -# Build from the "mitchell02" directory. -rule dir-mitchell02 ( name : defines * ) -{ - test-suite $(name) : - [ run mitchell02/counter_main.cpp : : : $(defines) : $(name)_counter ] - [ run mitchell02/courier_main.cpp mitchell02/courier.cpp : : - : $(defines) : $(name)_courier ] - [ run mitchell02/customer_manager_main.cpp - mitchell02/customer_manager.cpp : : : $(defines) - : $(name)_customer_manager ] - [ dir-run mitchell02 : dictionary : $(name) : $(defines) ] - [ run mitchell02/name_list_main.cpp mitchell02/name_list.cpp : : - : $(defines) : $(name)_name_list ] - [ run mitchell02/observer_main.cpp : : : $(defines) : $(name)_observer ] - [ dir-run mitchell02 : simple_queue : $(name) : $(defines) ] - [ dir-run mitchell02 : stack : $(name) : $(defines) ] - ; -} - -# Build from the "stroustrup97" directory. -rule dir-stroustrup97 ( name : defines * ) -{ - test-suite $(name) : - [ run stroustrup97/string_main.cpp stroustrup97/string.cpp : : - : $(defines) : $(name)_string ] - ; -} - -# Build from the "cline90" directory. -rule dir-cline90 ( name : defines * ) -{ - test-suite $(name) : - [ dir-run cline90 : calendar : $(name) : $(defines) ] - [ dir-run cline90 : stack : $(name) : $(defines) ] - [ run cline90/vector_main.cpp : : : $(defines) : $(name)_vector ] - [ dir-run cline90 : vstack : $(name) : $(defines) ] - ; -} - -# Convenience Rules # - -# Compile a file in a directory and run it. -rule dir-run ( dir : cppfile : name : defines * ) -{ - run $(dir)/$(cppfile).cpp : : : $(defines) : $(name)_$(cppfile) ; -} - -# Check compiler-error for a file in a directory. -rule dir-err ( dir : cppfile : name : defines * ) -{ - compile-fail $(dir)/$(cppfile).cpp : $(defines) : $(name)_$(cppfile) ; -} - -type.register UNIT_TEST_RAW : UNIT_TEST ; -generators.register-standard testing.unit-test : : UNIT_TEST_RAW ; -if ! [ python.configured ] -{ - exit "error: python is not configured" ; -} - -# Use Python script to run a test. -rule py-test ( name : pyscript : commandline ) -{ - # Unfortunately, unit-test does not stop compilation when `-q` is used but - # it will signal the failure and build again the test in next runs. - unit-test-raw $(name) : $(pyscript) : - "python "$(pyscript)" "$(commandline) ; - always $(name) ; -} - -# Assume Boost.Python cppfile defines module named `$(name)_$(cppfile)_module`. -# Assume Python test script to run is named "$(cppfile).py". -rule dir-pymodule ( dir : cppfile : name : defines * ) -{ - python-extension $(name)_$(cppfile)_module : - # Need this complex file name because file name is always target of - # this rule so it must be unique across all on/off combinations. - $(dir)/$(cppfile)_module/$(name)_$(cppfile)_module.cpp : - /boost/python//boost_python - /boost/regex//boost_regex - shared:BOOST_REGEX_DYN_LINK=1 - $(defines) - ; - install $(name)_$(cppfile)_install1 : - $(name)_$(cppfile)_module : - on - SHARED_LIB - PYTHON_EXTENSION - $(dir) - ; - install $(name)_$(cppfile)_install2 : - $(name)_$(cppfile)_module : - on - SHARED_LIB - PYTHON_EXTENSION - . - ; - # On Linux, need to install on both `$(dir)` and `.`. - alias $(name)_$(cppfile)_install : - $(name)_$(cppfile)_install1 $(name)_$(cppfile)_install2 ; - py-test $(name)_$(cppfile)_run - : $(dir)/$(cppfile).py - : $(name)_$(cppfile)_module - ; - alias $(name)_$(cppfile) : - $(name)_$(cppfile)_install - $(name)_$(cppfile)_run - ; -} - -# Build all files with all sensible combinations of contract-off config macros. -rule config-combinations ( name ) -{ - # Pre, post, and class-inv are combined with each other but not with - # block-inv and loop-var (unless for all off) because they do not influence - # each other and in the interest to limit the target combinations. - # All on. - dir-$(name) $(name) ; - # 1 off. - dir-$(name) noe_$(name) : - CONTRACT_CONFIG_NO_PRECONDITIONS - ; - dir-$(name) noo_$(name) : - CONTRACT_CONFIG_NO_POSTCONDITIONS - ; - dir-$(name) noi_$(name) : - CONTRACT_CONFIG_NO_CLASS_INVARIANTS - ; - dir-$(name) nob_$(name) : - CONTRACT_CONFIG_NO_BLOCK_INVARIANTS - ; - dir-$(name) nol_$(name) : - CONTRACT_CONFIG_NO_LOOP_VARIANTS - ; - # 2 off. - dir-$(name) noeo_$(name) : - CONTRACT_CONFIG_NO_PRECONDITIONS - CONTRACT_CONFIG_NO_POSTCONDITIONS - ; - dir-$(name) noei_$(name) : - CONTRACT_CONFIG_NO_PRECONDITIONS - CONTRACT_CONFIG_NO_CLASS_INVARIANTS - ; - dir-$(name) nooi_$(name) : - CONTRACT_CONFIG_NO_POSTCONDITIONS - CONTRACT_CONFIG_NO_CLASS_INVARIANTS - ; - dir-$(name) nobl_$(name) : - CONTRACT_CONFIG_NO_BLOCK_INVARIANTS - CONTRACT_CONFIG_NO_LOOP_VARIANTS - ; - # 3 off. - dir-$(name) noeoi_$(name) : - CONTRACT_CONFIG_NO_PRECONDITIONS - CONTRACT_CONFIG_NO_POSTCONDITIONS - CONTRACT_CONFIG_NO_CLASS_INVARIANTS - ; - # All off. - dir-$(name) noeoibl_$(name) : - CONTRACT_CONFIG_NO_PRECONDITIONS - CONTRACT_CONFIG_NO_POSTCONDITIONS - CONTRACT_CONFIG_NO_CLASS_INVARIANTS - CONTRACT_CONFIG_NO_BLOCK_INVARIANTS - CONTRACT_CONFIG_NO_LOOP_VARIANTS - ; - # Target for all contract on/off combinations for a given directory. - alias $(name)_onoff : $(name) noe_$(name) noo_$(name) noi_$(name) - nob_$(name) nol_$(name) noeo_$(name) noei_$(name) nooi_$(name) - nobl_$(name) noeoi_$(name) noeoibl_$(name) ; -} - -# Target Definitions # - -# Define targets for all directories and all contract on/off combinations. -config-combinations contracts ; -config-combinations virtual_specifiers ; -config-combinations concepts ; -config-combinations named_parameters ; -config-combinations n1962 ; -config-combinations n2081 ; -config-combinations meyer97 ; -config-combinations mitchell02 ; -config-combinations stroustrup97 ; -config-combinations cline90 ; -alias all_on : contracts virtual_specifiers concepts named_parameters n1962 - n2081 meyer97 mitchell02 stroustrup97 cline90 ; -alias all_off : noeoibl_contracts noeoibl_virtual_specifiers noeoibl_concepts - noeoibl_named_parameters noeoibl_n1962 noeoibl_n2081 noeoibl_meyer97 - noeoibl_mitchell02 noeoibl_stroustrup97 noeoibl_cline90 ; - diff --git a/example/cline90/calendar.cpp b/example/cline90/calendar.cpp deleted file mode 100644 index 1280f27..0000000 --- a/example/cline90/calendar.cpp +++ /dev/null @@ -1,74 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[cline90_calendar -// File: calendar.cpp -#include -#include - -CONTRACT_CLASS( - class (calendar) -) { - CONTRACT_CLASS_INVARIANT( - month() >= 1, - month() <= 12, - date() >= 1, - date() <= days_in(month()) - ) - - CONTRACT_CONSTRUCTOR( - public (calendar) ( void ) - postcondition( month() == 1, date() == 31 ) - initialize( month_(1), date_(31) ) - ) {} - - CONTRACT_DESTRUCTOR( - public virtual (~calendar) ( void ) - ) {} - - CONTRACT_FUNCTION( - public int (month) ( void ) const - ) { - return month_; - } - - CONTRACT_FUNCTION( - public int (date) ( void ) const - ) { - return date_; - } - - CONTRACT_FUNCTION( - public void (reset) ( int new_month ) - precondition( new_month >= 1, new_month <= 12 ) - postcondition( month() == new_month ) - ) { - month_ = new_month; - } - - CONTRACT_FUNCTION( - private static int (days_in) ( int month ) - precondition( month >= 1, month <= 12 ) - postcondition( auto result = return, result >= 1, result <= 31 ) - ) { - return 31; // For simplicity, assume all months have 31 days. - } - - private: int month_, date_; -}; - -int main ( void ) -{ - calendar c; - BOOST_TEST(c.date() == 31); - BOOST_TEST(c.month() == 1); - c.reset(8); // Set month to August. - BOOST_TEST(c.month() == 8); - return boost::report_errors(); -} -//] - diff --git a/example/cline90/stack.cpp b/example/cline90/stack.cpp deleted file mode 100644 index b980ebb..0000000 --- a/example/cline90/stack.cpp +++ /dev/null @@ -1,139 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[cline90_stack -// File: stack.cpp -#include -#include -#include -#include -#include -#include -#include -#include - -CONTRACT_CLASS( - template( typename T ) - class (stack) -) { - // NOTE: Incomplete set of assertions addressing only `empty` and `full`. - - CONTRACT_CLASS_INVARIANT( void ) - - public: struct out_of_memory {}; - public: struct error {}; - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (stack) ( int capacity ) - precondition( capacity >= 0 ) - postcondition( - empty(), - full() == (capacity == 0) - ) - // Function-Try blocks are programmed within the macros only for - // constructors with member initializers otherwise they are - // programmed with the body definition and outside the macros. - try initialize( // Try-block for constructor initializers and body. - data_(new T[capacity]), - capacity_(capacity), - size_(0) - ) catch(std::bad_alloc& e) ( - std::cerr << "out of memory for " << capacity << "-stack: " << - e.what() << std::endl; - throw out_of_memory(); - // Unfortunately, cannot wrap exception type commas with extra - // parenthesis (because symbol `...` used to catch-all) but - // `BOOST_IDENTITY_TYPE` can be used. - ) catch(BOOST_IDENTITY_TYPE((std::pair&)) e) ( - std::cerr << "error number " << e.first << " for " << - capacity << "-stack: " << e.second << std::endl; - throw error(); - ) catch(...) ( - std::cerr << "unknown error for " << capacity << "-stack" << - std::endl; - throw; // Re-throw exception. - ) - ) { - for(int i = 0; i < capacity_; ++i) data_[i] = T(); - } - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~stack) ( void ) - ) -#if !defined(BOOST_MSVC) // MSVC supports only constructor-try blocks. - try { // Function-try block (outside the macro). - delete[] data_; - } catch(...) { - std::cerr << "error for stack destruction, terminating" << std::endl; - std::terminate(); // Destructor should never throw. - } -#else // MSVC - { - delete[] data_; - } -#endif // MSVC - - CONTRACT_FUNCTION_TPL( - public bool (empty) ( void ) const - ) { - return size_ == 0; - } - - CONTRACT_FUNCTION_TPL( - public bool (full) ( void ) const - ) { - return size_ == capacity_; - } - - CONTRACT_FUNCTION_TPL( - public void (push) ( (T) value ) -#if !defined(BOOST_MSVC) // MSVC only supports throw( void ) exception spec. - throw( std::exception, error ) // Ex spec. -#endif // MSVC - precondition( not full() ) - postcondition( not empty() ) - ) -#if !defined(BOOST_MSVC) // MSVC supports only constructor-try blocks. - try -#endif // MSVC - { // Function-Try block (outside the macro). - data_[size_++] = value; - } -#if !defined(BOOST_MSVC) // MSVC supports only constructor-try blocks. - catch(std::exception& e) { - std::cerr << "error for " << capacity_ << "-stack: " << e.what() << - std::endl; - throw; // Re-throw STL exception. - } catch(...) { - std::cerr << "unknown error for " << capacity_ << "-stack" << - std::endl; - throw error(); - } -#endif // MSVC - - CONTRACT_FUNCTION_TPL( - public (T) (pop) ( void ) - precondition( not empty() ) - postcondition( not full() ) - ) { - return data_[--size_]; - } - - private: T* data_; - private: int capacity_; - private: int size_; -}; - -int main ( void ) -{ - stack s(3); - s.push(123); - BOOST_TEST(s.pop() == 123); - return boost::report_errors(); -} -//] - diff --git a/example/cline90/vector.hpp b/example/cline90/vector.hpp deleted file mode 100644 index 6e3e0ea..0000000 --- a/example/cline90/vector.hpp +++ /dev/null @@ -1,73 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[cline90_vector_header -// File: vector.hpp -#ifndef VECTOR_HPP_ -#define VECTOR_HPP_ - -#include - -CONTRACT_CLASS( - template( typename T ) - class (vector) -) { - // NOTE: Incomplete set of assertions addressing only `size`. - - CONTRACT_CLASS_INVARIANT_TPL( size() >= 0 ) - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (vector) ( int count, default 10 ) - precondition( count >= 0 ) - postcondition( size() == count ) - initialize( data_(new T[count]), size_(count) ) - ) { - for(int i = 0; i < size_; ++i) data_[i] = T(); - } - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~vector) ( void ) - ) { - delete[] data_; - } - - CONTRACT_FUNCTION_TPL( - public int (size) ( void ) const - // postcondition: Result non-negative checked by class invariant - ) { - return size_; - } - - CONTRACT_FUNCTION_TPL( - public void (resize) ( int count ) - precondition( count >= 0 ) - postcondition( size() == count ) - ) { - T* slice = new T[count]; - for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i]; - delete[] data_; - data_ = slice; - size_ = count; - } - - CONTRACT_FUNCTION_TPL( - public (T&) operator([])(at) ( int index ) - precondition( - index >= 0, - index < size() - ) - ) { - return data_[index]; - } - - private: T* data_; - private: int size_; -}; - -#endif // #include guard -//] - diff --git a/example/cline90/vector_app.hpp b/example/cline90/vector_app.hpp deleted file mode 100644 index 2a0207d..0000000 --- a/example/cline90/vector_app.hpp +++ /dev/null @@ -1,73 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[cline90_vector_app_header -// File: vector_app.hpp -// Extra spaces, newlines, etc used to align text with this library code. - - - - - -template< typename T> -class vector -{ - legal: size() >= 0; // Class invariants (legal). - - public: explicit vector ( int count = 10 ) - : data_(new T[count]), size_(count) - { - for(int i = 0; i < size_; ++i) data_[i] = T(); - } - - public: virtual ~vector ( void ) - { - delete[] data_; - } - - public: int size ( void ) const - { - return size_; - } - - public: void resize ( int count ) - { - T* slice = new T[count]; - for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i]; - delete[] data_; - data_ = slice; - size_ = count; - } - - public: T& operator[] ( int index ) - { - return data_[index]; - } - - // Preconditions (require) and postconditions (promise) for each function. - axioms: [ int count; require count >= 0; promise size() == count ] - vector(count); - axioms: [ int count; require count >= 0; promise size() == count ] - resize(count); - axioms: [ int index; require index >= 0 && index < size() ] - (*this)[x]; - - private: T* data_; - private: int size_; -}; - - - - - - - - - - -//] - diff --git a/example/cline90/vector_main.cpp b/example/cline90/vector_main.cpp deleted file mode 100644 index 0f1e892..0000000 --- a/example/cline90/vector_main.cpp +++ /dev/null @@ -1,24 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[cline90_vector_main -// File: vector_main.cpp -#include "vector.hpp" -#include - -int main ( void ) -{ - vector v(3); // Also set all elements to 0.0. - BOOST_TEST(v.size() == 3); - v[0] = 123; - v.resize(2); - BOOST_TEST(v[0] == 123); - BOOST_TEST(v.size() == 2); - return boost::report_errors(); -} -//] - diff --git a/example/cline90/vstack.cpp b/example/cline90/vstack.cpp deleted file mode 100644 index 4557b16..0000000 --- a/example/cline90/vstack.cpp +++ /dev/null @@ -1,144 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[cline90_vstack -// File: vstack.cpp -#include "vector.hpp" -#include -#include - -CONTRACT_CLASS( // Stack Abstract Data Type (ADT). - template( typename T ) - class (stack_adt) -) { - // NOTE: Incomplete set of assertions addressing only empty/full issues. - - CONTRACT_CLASS_INVARIANT_TPL( void ) // no invariants - - CONTRACT_CONSTRUCTOR_TPL( - public (stack_adt) ( void ) - // postcondition: - // empty (cannot be checked because empty's postcondition uses - // length which is pure virtual during construction) - ) {} - - CONTRACT_DESTRUCTOR_TPL( - public (~stack_adt) ( void ) - ) {} - - CONTRACT_FUNCTION_TPL( - public bool (full) ( void ) const - postcondition( - auto result = return, - result == (length() == capacity()) - ) - ) { - return length() == capacity(); - } - - CONTRACT_FUNCTION_TPL( - public bool (empty) ( void ) const - postcondition( auto result = return, result == (length() == 0) ) - ) { - return length() == 0; - } - - CONTRACT_FUNCTION_TPL( - public virtual int (length) ( void ) const - postcondition( auto result = return, result >= 0 ) - ) = 0; - - CONTRACT_FUNCTION_TPL( - public virtual int (capacity) ( void ) const - postcondition( auto result = return, result >= 0 ) - ) = 0; - - CONTRACT_FUNCTION_TPL( - public virtual void (push) ( (T) value ) - precondition( not full() ) - postcondition( not empty() ) - ) = 0; // Contract for pure virtual function. - - CONTRACT_FUNCTION_TPL( - public virtual (T) (pop) ( void ) - precondition( not empty() ) - postcondition( not full() ) - ) = 0; - - CONTRACT_FUNCTION_TPL( - public virtual void (clear) ( void ) - postcondition( empty() ) - ) = 0; -}; - -CONTRACT_CLASS( // Vector-based stack. - template( typename T ) - class (vstack) extends( public stack_adt ) -) { - CONTRACT_CLASS_INVARIANT_TPL( - length() >= 0, - length() < capacity() - ) - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (vstack) ( int count, default 10 ) - precondition( count >= 0 ) - postcondition( length() == 0, capacity() == count ) - initialize( vect_(count), length_(0) ) // OK, after preconditions. - ) {} - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~vstack) ( void ) - ) {} - - // NOTE: All following inherit contracts from `stack_adt`. - - CONTRACT_FUNCTION_TPL( - public int (length) ( void ) const override final - ) { - return length_; - } - - CONTRACT_FUNCTION_TPL( - public int (capacity) ( void ) const - ) { - return vect_.size(); - } - - CONTRACT_FUNCTION_TPL( - public void (push) ( (T) value ) override final - ) { - vect_[length_++] = value; - } - - CONTRACT_FUNCTION_TPL( - public (T) (pop) ( void ) override final - ) { - return vect_[--length_]; - } - - CONTRACT_FUNCTION_TPL( - public void (clear) ( void ) override final - ) { - length_ = 0; - } - - private: vector vect_; - private: int length_; -}; - -int main ( void ) -{ - vstack s(3); - BOOST_TEST(s.capacity() == 3); - s.push(123); - BOOST_TEST(s.length() == 1); - BOOST_TEST(s.pop() == 123); - return boost::report_errors(); -} -//] - diff --git a/example/contracts/assertion_complexity_factorial.cpp b/example/contracts/assertion_complexity_factorial.cpp deleted file mode 100644 index e98cf78..0000000 --- a/example/contracts/assertion_complexity_factorial.cpp +++ /dev/null @@ -1,47 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[assertion_complexity_factorial -// Assertion requirements used to model assertion computational complexity. -#define O_1 0 // O(1) constant (default). -#define O_N 1 // O(n) linear. -#define O_NN 2 // O(n * n) quadratic. -#define O_NX 3 // O(n^x) polynomial. -#define O_FACTN 4 // O(n!) factorial. -#define O_EXPN 5 // O(e^n) exponential. -#define O_ALL 10 -#define COMPLEXITY_MAX O_ALL - -CONTRACT_FUNCTION( - int (factorial) ( int n ) - precondition( n >= 0 ) - postcondition( - auto result = return, - result >= 1, - if(n < 2) ( - result == 1 - ) else ( - // Assertion compiled and checked only if within complexity. - result == n * factorial(n - 1), - requires O_FACTN <= COMPLEXITY_MAX - ) - ) -) { - if(n < 2) return 1; - else return n * factorial(n - 1); -} -//] - -int main ( void ) -{ - BOOST_TEST(factorial(4) == 24); - return boost::report_errors(); -} - diff --git a/example/contracts/assertion_requirements_push_back.cpp b/example/contracts/assertion_requirements_push_back.cpp deleted file mode 100644 index 86769d5..0000000 --- a/example/contracts/assertion_requirements_push_back.cpp +++ /dev/null @@ -1,77 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[assertion_requirements_push_back -#include - -CONTRACT_CLASS( - template( typename T ) - class (vector) -) { - CONTRACT_CLASS_INVARIANT_TPL( - size() <= capacity(), - capacity() <= max_size() - // ... - ) - - CONTRACT_FUNCTION_TPL( - public void (push_back) ( (T const&) value ) - precondition( size() < max_size() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - auto old_capacity = CONTRACT_OLDOF capacity(), - size() == old_size + 1, - capacity() >= old_capacity, - // Requirements disable assertion if `T` has no `operator==`. - back() == value, requires boost::has_equal_to::value - ) - ) { - vector_.push_back(value); - } - - // ... -//] - - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::const_reference const_reference; - - public: size_type size ( void ) const { return vector_.size(); } - public: size_type max_size ( void ) const { return vector_.max_size(); } - public: size_type capacity ( void ) const { return vector_.capacity(); } - public: const_reference back ( void ) const { return vector_.back(); } - - private: std::vector vector_; -}; - -//[assertion_requirements_push_back_call -struct num // Not equality comparable. -{ - int value; - explicit num ( int a_value ) : value(a_value) {} -}; - -int main ( void ) -{ - vector i; - i.push_back(123); - - vector n; - n.push_back(num(123)); - BOOST_TEST(not boost::has_equal_to::value); - - // ... -//] - - BOOST_TEST(i.size() == 1); - BOOST_TEST(n.size() == 1); - return boost::report_errors(); -} - diff --git a/example/contracts/assertion_statement_ialloc.cpp b/example/contracts/assertion_statement_ialloc.cpp deleted file mode 100644 index 6d4180d..0000000 --- a/example/contracts/assertion_statement_ialloc.cpp +++ /dev/null @@ -1,42 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include -#include - -//[assertion_statement_ialloc -CONTRACT_FUNCTION( - template( typename T ) - (T*) (ialloc) ( void ) - precondition( - namespace mpl = boost::mpl, // Namespace aliasing. - using namespace std, // Using directive. - typedef typename allocator::pointer ptr, // Type definition. - static_assert( - (mpl::or_< - mpl::bool_ - , mpl::bool_ - >::value) - , "within max size" - ) - ) -) { - return static_cast(malloc(sizeof(T))); -} -//] - -int main ( void ) -{ - char* p = ialloc(); - BOOST_TEST(p); - return boost::report_errors(); -} - diff --git a/example/contracts/blockinv_loopvar_gcd.cpp b/example/contracts/blockinv_loopvar_gcd.cpp deleted file mode 100644 index 476b90c..0000000 --- a/example/contracts/blockinv_loopvar_gcd.cpp +++ /dev/null @@ -1,51 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[blockinv_loopvar_gcd -CONTRACT_FUNCTION( - template( typename T ) - (T) (gcd) ( (T const&) a, (T const&) b ) - precondition( - static_assert(boost::is_integral::value, "integral type"), - a != 0, - b != 0 - ) - postcondition( - auto result = return, - result <= a, - result <= b - ) -) { - T x = a, y = b; - // Block invariant assert conditions within body, - CONTRACT_BLOCK_INVARIANT_TPL( const( x, a ) x == a, const( y, b ) y == b ) - - CONTRACT_LOOP( while(x != y) ) { // Define a loop with variants (below). - // Block invariant for loops (i.e., loop invariants). - CONTRACT_BLOCK_INVARIANT_TPL( const( x ) x > 0, const( y ) y > 0 ) - // Loop variant checked to be non-negative and monotonically decreasing. - CONTRACT_LOOP_VARIANT_TPL( const( x, y ) std::max(x, y) ) - - if(x > y) x = x - y; - else y = y - x; - } - - return x; -} -//] - -int main ( void ) -{ - BOOST_TEST(gcd(12, 28) == 4); - BOOST_TEST(gcd(4, 14) == 2); - return boost::report_errors(); -} - diff --git a/example/contracts/body_natural.cpp b/example/contracts/body_natural.cpp deleted file mode 100644 index 8e24ca2..0000000 --- a/example/contracts/body_natural.cpp +++ /dev/null @@ -1,19 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include "body_natural.hpp" - -int main ( void ) -{ - natural n, m(123); - BOOST_TEST(n.equal(natural())); - BOOST_TEST(less(n, m)); - BOOST_TEST(greater(m, n)); - return boost::report_errors(); -} - diff --git a/example/contracts/body_natural.hpp b/example/contracts/body_natural.hpp deleted file mode 100644 index cd94dd6..0000000 --- a/example/contracts/body_natural.hpp +++ /dev/null @@ -1,78 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#ifndef BODY_NATURAL_HPP_ -#define BODY_NATURAL_HPP_ - -#include - -//[body_natural -template< typename T, T Default = T() > // Class forward declaration. -class natural ; - -template< typename T > // Function forward declaration. -bool less ( natural const& left, natural const& right ) ; - -CONTRACT_FUNCTION( - template( typename T ) - bool (greater) ( (natural const&) left, (natural const&) right ) - postcondition( - auto result = return, - result ? not less(left, right) : true - ) -) ; // Deferred free function body definition, use `;`. - -CONTRACT_CLASS( // Class declaration (with contracts). - template( typename T, (T) Default ) - class (natural) -) { - CONTRACT_CLASS_INVARIANT_TPL( get() >= 0 ) - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (natural) ( (T const&) value, default Default ) - precondition( value >= 0 ) - postcondition( get() == value ) - // Unfortunately, no member initializers when body deferred. - ) ; // Deferred constructor body definition, use `;`. - - CONTRACT_DESTRUCTOR_TPL( - public (~natural) ( void ) - ) ; // Deferred destructor body definition, use `;`. - - CONTRACT_FUNCTION_TPL( - public bool (equal) ( (natural const&) right ) const - postcondition( - auto result = return, - result == not less(*this, right) && not greater(*this, right) - ) - ) ; // Deferred member function body definition, use `;`. - - CONTRACT_FUNCTION_TPL( - public (T) (get) ( void ) const - ) { - return value_; - } - - private: T value_; -}; - -CONTRACT_FUNCTION( // Function declaration (with contracts). - template( typename T ) - bool (less) ( (natural const&) left, (natural const&) right ) - postcondition( - auto result = return, - result ? not greater(left, right) : true - ) -) { - return left.get() < right.get(); -} -//] - -#include "body_natural_impl.hpp" - -#endif // #include guard - diff --git a/example/contracts/body_natural_impl.hpp b/example/contracts/body_natural_impl.hpp deleted file mode 100644 index a135e2d..0000000 --- a/example/contracts/body_natural_impl.hpp +++ /dev/null @@ -1,39 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include "body_natural.hpp" - -//[body_natural_impl -// Deferred body definitions, separated from their declarations and contracts. - -template< typename T > -bool CONTRACT_FREE_BODY(greater) ( - natural const& left, natural const& right ) -{ - return left.get() > right.get(); -} - -template< typename T, T Default > -CONTRACT_CONSTRUCTOR_BODY((natural), natural) ( T const& value ) -{ - value_ = value; -} - -template< typename T, T Default > -CONTRACT_DESTRUCTOR_BODY((natural), ~natural) ( void ) -{ - // Do nothing. -} - -template< typename T, T Default > -bool natural::CONTRACT_MEMBER_BODY(equal) ( natural const& right ) - const -{ - return not less(*this, right) && not greater(*this, right); -} -//] - diff --git a/example/contracts/broken_handler_sqrt.cpp b/example/contracts/broken_handler_sqrt.cpp deleted file mode 100644 index 10ed041..0000000 --- a/example/contracts/broken_handler_sqrt.cpp +++ /dev/null @@ -1,92 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#if defined(__GNUC__) && defined(__GXX_EXPERIMENTAL_CXX0X__) -# warning "ignored known failure on G++ with C++0x" -# warning "note: maybe a compiler bug catching re-throws" - int main ( void ) { return 0; } // Trivial success. -#else - -#include -#include -#include - -//[broken_handler_sqrt -struct not_a_number {}; // User defined exception. - -CONTRACT_FUNCTION( - double (sqrt) ( double x ) - precondition( - x >= 0.0 ? true : throw not_a_number() // Throw user exception. - ) - postcondition( - auto root = return, - root * root == x // Failure throws `contract::broken` exception. - ) -) { - return 0.0; // Intentionally incorrect to fail postcondition. -} - -void throwing_handler ( contract::from const& context ) -{ - // Failure handlers always called with active exception that failed the - // contract, so re-throw it to catch it below for logging. - try { - throw; - } catch(contract::broken& failure) { - std::cerr << failure.file_name() << "(" << failure.line_number() << - "): contract assertion \"" << failure.assertion_code() << - "\" failed " << std::endl; - } catch(std::exception& failure) { - std::cerr << "contract failed: " << failure.what() << std::endl; - } catch(...) { - std::cerr << "contract failed with unknown error" << std::endl; - } - - // Cannot throw from destructors to comply with STL exception safety, - // otherwise re-throw active exception that failed the contract. - if(context == contract::FROM_DESTRUCTOR) - std::cerr << "Ignoring destructor contract failure (probably " - << "something bad has happened)" << std::endl; - else throw; // Never terminates. -} - -int main ( void ) -{ - // Customize contract broken handlers to throw exceptions instead of - // terminating the program (default). - contract::set_precondition_broken(&throwing_handler); - contract::set_postcondition_broken(&throwing_handler); - -#ifndef CONTRACT_CONFIG_NO_PRECONDITIONS - bool pre = false; - try { - sqrt(-1.0); // Fails precondition. - } catch(not_a_number&) { - pre = true; - std::clog << "Ignoring not-a-number exception" << std::endl; - } - BOOST_TEST(pre); -#endif - -#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS - bool post = false; - try { - sqrt(4.0); // Fails postcondition. - } catch(...) { - post = true; - std::clog << "Unable to calculate square root" << std::endl; - } - BOOST_TEST(post); -#endif - - return boost::report_errors(); -} -//] - -#endif // known failures - diff --git a/example/contracts/class_ivector.cpp b/example/contracts/class_ivector.cpp deleted file mode 100644 index 221d152..0000000 --- a/example/contracts/class_ivector.cpp +++ /dev/null @@ -1,89 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include - -//[class_ivector_classinv -CONTRACT_CLASS( // Declare the class. - class (ivector) -) { - CONTRACT_CLASS_INVARIANT( // Specify the class invariants. - empty() == (size() == 0), - size() <= capacity(), - capacity() <= max_size(), - std::distance(begin(), end()) == int(size()) - ) - - public: typedef std::vector::size_type size_type; - // ... -//] - public: typedef std::vector::const_reference const_reference; - public: typedef std::vector::const_iterator const_iterator; - - - //[class_ivector_constructor - CONTRACT_CONSTRUCTOR( // Declare the constructor and its contract. - public explicit (ivector) ( (size_type) count ) - precondition( count >= 0 ) - postcondition( - size() == count, - boost::algorithm::all_of_equal(begin(), end(), 0) - ) - initialize( vector_(count) ) - ) {} - //] - - //[class_ivector_destructor - CONTRACT_DESTRUCTOR( // Declare the destructor (so it checks invariants). - public virtual (~ivector) ( void ) - ) {} - //] - - //[class_ivector_member - CONTRACT_FUNCTION( // Declare the member function with its contract. - public void (push_back) ( int const value ) - precondition( size() < max_size() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - auto old_capacity = CONTRACT_OLDOF capacity(), - size() == old_size + 1, - capacity() >= old_capacity, - back() == value - ) - ) { - vector_.push_back(value); - } - //] - - 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: size_type capacity ( void ) const { return vector_.capacity(); } - public: const_reference back ( void ) const { return vector_.back(); } - public: const_iterator begin ( void ) const { return vector_.begin(); } - public: const_iterator end ( void ) const { return vector_.end(); } - - private: std::vector vector_; -}; - -int main ( void ) -{ - ivector v(1); - BOOST_TEST(v.size() == 1); - BOOST_TEST(v.back() == 0); - - v.push_back(123); - BOOST_TEST(v.size() == 2); - BOOST_TEST(v.back() == 123); - - return boost::report_errors(); -} - diff --git a/example/contracts/class_template_vector.cpp b/example/contracts/class_template_vector.cpp deleted file mode 100644 index 53b0bc1..0000000 --- a/example/contracts/class_template_vector.cpp +++ /dev/null @@ -1,88 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include - -//[class_template_vector -#include "pushable.hpp" - -CONTRACT_CLASS( - template( typename T ) - class (vector) extends( public pushable ) // Subcontract. -) { - // Within templates, use contract macros postfixed by `_TPL`. - - CONTRACT_CLASS_INVARIANT_TPL( - empty() == (size() == 0), - size() <= capacity(), - capacity() <= max_size(), - std::distance(begin(), end()) == int(size()) - ) - - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::const_reference const_reference; - public: typedef typename std::vector::const_iterator const_iterator; - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (vector) ( (size_type) count ) - precondition( count >= 0 ) - postcondition( - size() == count, - boost::algorithm::all_of_equal(begin(), end(), T()) - ) - initialize( vector_(count) ) - ) {} - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~vector) ( void ) - ) {} - - CONTRACT_FUNCTION_TPL( - public void (push_back) ( (T const&) value ) - precondition( size() < max_size() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - auto old_capacity = CONTRACT_OLDOF capacity(), - size() == old_size + 1, - capacity() >= old_capacity - // Overridden postconditions also check `back() == value`. - ) - ) { - vector_.push_back(value); - } - - // ... -//] - - 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: size_type capacity ( void ) const { return vector_.capacity(); } - public: const_reference back ( void ) const { return vector_.back(); } - public: const_iterator begin ( void ) const { return vector_.begin(); } - public: const_iterator end ( void ) const { return vector_.end(); } - - private: std::vector vector_; -}; - -int main ( void ) -{ - vector v(1); - BOOST_TEST(v.size() == 1); - BOOST_TEST(v.back() == 0); - - v.push_back(123); - BOOST_TEST(v.size() == 2); - BOOST_TEST(v.back() == 123); - - return boost::report_errors(); -} - diff --git a/example/contracts/class_template_vector_seq.cpp b/example/contracts/class_template_vector_seq.cpp deleted file mode 100644 index d53542c..0000000 --- a/example/contracts/class_template_vector_seq.cpp +++ /dev/null @@ -1,88 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include - -//[class_template_vector_seq -#include "pushable_seq.hpp" - -CONTRACT_CLASS( - template( (typename T) ) - class (vector) extends( (public pushable) ) -) { - // Use preprocessor sequences instead of variadic comma-separated lists. - - CONTRACT_CLASS_INVARIANT_TPL( - (empty() == (size() == 0)) - (size() <= capacity()) - (capacity() <= max_size()) - (std::distance(begin(), end()) == int(size())) - ) - - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::const_reference const_reference; - public: typedef typename std::vector::const_iterator const_iterator; - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (vector) ( ((size_type) count) ) - precondition( (count >= 0) ) - postcondition( - (size() == count) - (boost::algorithm::all_of_equal(begin(), end(), T())) - ) - initialize( (vector_(count)) ) - ) {} - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~vector) ( void ) - ) {} - - CONTRACT_FUNCTION_TPL( - public void (push_back) ( ((T const&) value) ) - precondition( (size() < max_size()) ) - postcondition( - (auto old_size = CONTRACT_OLDOF size()) - (auto old_capacity = CONTRACT_OLDOF capacity()) - (size() == old_size + 1) - (capacity() >= old_capacity) - // Overridden postconditions also check `back() == value`. - ) - ) { - vector_.push_back(value); - } - - // ... -//] - - 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: size_type capacity ( void ) const { return vector_.capacity(); } - public: const_reference back ( void ) const { return vector_.back(); } - public: const_iterator begin ( void ) const { return vector_.begin(); } - public: const_iterator end ( void ) const { return vector_.end(); } - - private: std::vector vector_; -}; - -int main ( void ) -{ - vector v(1); - BOOST_TEST(v.size() == 1); - BOOST_TEST(v.back() == 0); - - v.push_back(123); - BOOST_TEST(v.size() == 2); - BOOST_TEST(v.back() == 123); - - return boost::report_errors(); -} - diff --git a/example/contracts/class_template_vector_seq_nova.cpp b/example/contracts/class_template_vector_seq_nova.cpp deleted file mode 100644 index 5569113..0000000 --- a/example/contracts/class_template_vector_seq_nova.cpp +++ /dev/null @@ -1,10 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include "nova.hpp" -#include "class_template_vector_seq.cpp" - diff --git a/example/contracts/const_assertion_number.cpp b/example/contracts/const_assertion_number.cpp deleted file mode 100644 index 42f5576..0000000 --- a/example/contracts/const_assertion_number.cpp +++ /dev/null @@ -1,47 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[const_assertion_number -unsigned even = 0; - -CONTRACT_CLASS( - class (number) -) { - CONTRACT_CLASS_INVARIANT( void ) - - public: static unsigned odd; - - CONTRACT_FUNCTION( - public void (next) ( void ) - postcondition( - auto old_even = CONTRACT_OLDOF even, - auto old_odd = CONTRACT_OLDOF odd, - // `[old_]even` and `[old_]odd` all `const&` within assertions. - const( even, old_even ) even == old_even + 2, - const( odd, old_odd ) odd == old_odd + 2 - ) - ) { - even += 2; - odd += 2; - } -}; - -unsigned number::odd = 1; -//] - -int main ( void ) -{ - number n; - n.next(); - BOOST_TEST(even == 2); - BOOST_TEST(number::odd == 3); - return boost::report_errors(); -} - diff --git a/example/contracts/const_assertion_number_global_error.cpp b/example/contracts/const_assertion_number_global_error.cpp deleted file mode 100644 index d2497be..0000000 --- a/example/contracts/const_assertion_number_global_error.cpp +++ /dev/null @@ -1,50 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -#ifdef CONTRACT_CONFIG_NO_POSTCONDITIONS -# error "constant assertion failure requires postconditions" -#endif - -//[const_assertion_number -unsigned even = 0; - -CONTRACT_CLASS( - class (number) -) { - CONTRACT_CLASS_INVARIANT( void ) - - public: static unsigned odd; - - CONTRACT_FUNCTION( - public void (next) ( void ) - postcondition( - auto old_even = CONTRACT_OLDOF even, - auto old_odd = CONTRACT_OLDOF odd, - const( even, old_even ) even = old_even + 2, // Correctly error. - const( odd, old_odd ) odd == old_odd + 2 - ) - ) { - even += 2; - odd += 2; - } -}; - -unsigned number::odd = 1; -//] - -int main ( void ) -{ - number n; - n.next(); - BOOST_TEST(even == 2); - BOOST_TEST(number::odd == 3); - return boost::report_errors(); -} - diff --git a/example/contracts/const_assertion_number_static_error.cpp b/example/contracts/const_assertion_number_static_error.cpp deleted file mode 100644 index 20e7c63..0000000 --- a/example/contracts/const_assertion_number_static_error.cpp +++ /dev/null @@ -1,50 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -#ifdef CONTRACT_CONFIG_NO_POSTCONDITIONS -# error "constant assertion failure requires postconditions" -#endif - -//[const_assertion_number -unsigned even = 0; - -CONTRACT_CLASS( - class (number) -) { - CONTRACT_CLASS_INVARIANT( void ) - - public: static unsigned odd; - - CONTRACT_FUNCTION( - public void (next) ( void ) - postcondition( - auto old_even = CONTRACT_OLDOF even, - auto old_odd = CONTRACT_OLDOF odd, - const( even, old_even ) even == old_even + 2, - const( odd, old_odd ) odd = old_odd + 2 // Correctly error. - ) - ) { - even += 2; - odd += 2; - } -}; - -unsigned number::odd = 1; -//] - -int main ( void ) -{ - number n; - n.next(); - BOOST_TEST(even == 2); - BOOST_TEST(number::odd == 3); - return boost::report_errors(); -} - diff --git a/example/contracts/const_select_assertion_factorial.cpp b/example/contracts/const_select_assertion_factorial.cpp deleted file mode 100644 index 2f8469d..0000000 --- a/example/contracts/const_select_assertion_factorial.cpp +++ /dev/null @@ -1,42 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[const_select_assertion_factorial -int n = 0; - -CONTRACT_FUNCTION( - int (factorial) ( void ) - precondition( const( n ) n >= 0 ) - postcondition( - auto result = return, - if(const( n ) n == -1 or n == 0) ( // Constant-correct if-condition. - result == 1 - ) else ( - result >= 1 - ) - ) -) { - int m = n; - if(m == 0 or m == 1) { - return 1; - } else { - --n; - return m * factorial(); - } -} -//] - -int main ( void ) -{ - n = 4; - BOOST_TEST(factorial() == 24); - return boost::report_errors(); -} - diff --git a/example/contracts/const_select_assertion_factorial_error.cpp b/example/contracts/const_select_assertion_factorial_error.cpp deleted file mode 100644 index df76e58..0000000 --- a/example/contracts/const_select_assertion_factorial_error.cpp +++ /dev/null @@ -1,46 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -#ifdef CONTRACT_CONFIG_NO_POSTCONDITIONS -# error "constant select assertion failure requires postconditions" -#endif - -//[const_select_assertion_factorial -int n = 0; - -CONTRACT_FUNCTION( - int (factorial) ( void ) - precondition( const( n ) n >= 0 ) - postcondition( - auto result = return, - if(const( n ) n = 0 or n == 1) ( // n is const& within if-condition. - result == 1 - ) else ( - result >= 1 - ) - ) -) { - int m = n; - if(m == 0 or m == 1) { - return 1; - } else { - --n; - return m * factorial(); - } -} -//] - -int main ( void ) -{ - n = 4; - BOOST_TEST(factorial() == 24); - return boost::report_errors(); -} - diff --git a/example/contracts/contract_failure.cpp b/example/contracts/contract_failure.cpp deleted file mode 100644 index 0db6dcc..0000000 --- a/example/contracts/contract_failure.cpp +++ /dev/null @@ -1,474 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include - -bool // Fail the asserted conditions. - class_inv = true - , static_class_inv = true - , volatile_class_inv = true - , pre = true - , post = true -; - -struct check_pre // Check pre asserted before member initializers. -{ - check_pre ( void ) { BOOST_TEST(pre); } -}; - -struct forced_exception {}; - -CONTRACT_CLASS( - struct (failer) extends( check_pre ) -) { - CONTRACT_CLASS_INVARIANT( - class_inv, - static class( static_class_inv ), - volatile class( volatile_class_inv ) - ) - - CONTRACT_CONSTRUCTOR( - public (failer) ( - (bool*) inv, default 0, - bool const throwing, default false - ) - precondition( pre ) - postcondition( post ) - initialize( - check_pre(), - destructor_inv(0), - destructor_throwing(false) - ) - ) { - if(inv) *inv = false; - if(throwing) throw forced_exception(); - } - - bool* destructor_inv; // Destructor has not parameter, - bool destructor_throwing; // use data members instead. - - CONTRACT_DESTRUCTOR( - public virtual (~failer) ( void ) - ) { - if(destructor_inv) *destructor_inv = false; - // STL says destrcutors shall not throw, throwing here just for testing. - if(destructor_throwing) throw forced_exception(); - } - - CONTRACT_FUNCTION( - public void (fail) ( - (bool*) inv, default 0, - bool const throwing, default false - ) - precondition( pre ) - postcondition( post ) - ) { - if(inv) *inv = false; - if(throwing) throw forced_exception(); - } - - CONTRACT_FUNCTION( - public void (fail) ( - (bool*) inv, default 0, - bool const throwing, default false - ) volatile - precondition( pre ) - postcondition( post ) - ) { - if(inv) *inv = false; - if(throwing) throw forced_exception(); - } - - CONTRACT_FUNCTION( - public static void (static_failure) ( - (bool*) inv, default 0, - bool const throwing, default false - ) - precondition( pre ) - postcondition( post ) - ) { - if(inv) *inv = false; - if(throwing) throw forced_exception(); - } -}; - -CONTRACT_FUNCTION( - void (free_failure) ( bool const throwing, default false ) - precondition( pre ) - postcondition( post ) -) { - if(throwing) throw forced_exception(); -} - -std::string str ( contract::from const& context ) -{ - switch(context) { - case contract::FROM_CONSTRUCTOR: return "constructor"; - case contract::FROM_DESTRUCTOR: return "destructor"; - case contract::FROM_NONSTATIC_MEMBER_FUNCTION: - return "non-static member function"; - case contract::FROM_STATIC_MEMBER_FUNCTION: return "static member function"; - case contract::FROM_FREE_FUNCTION: return "free function"; - case contract::FROM_BODY: return "body"; - } - return ""; -} - -#define THROWING_HANDLER(name) \ - struct name \ - { \ - contract::from context; \ - contract::broken error; \ - name ( contract::from const& a_context, \ - contract::broken const& an_error ) \ - : context(a_context), error(an_error) {} \ - }; \ - void BOOST_PP_CAT(name, _handler) ( contract::from const& context ) \ - { \ - try { \ - throw; \ - } catch(contract::broken& error) { \ - std::cerr << "checking " << BOOST_PP_STRINGIZE(name) << \ - " from " << str(context) << ":" << std::endl; \ - std::cerr << " " << error.what() << std::endl; \ - throw name(context, error); \ - } \ - } - -#define CHECK(assertion, exception, from_context, body) \ - pass = false; \ - try { \ - body \ - } catch(exception& ex) { \ - assertion = true; \ - BOOST_TEST(ex.context == from_context); \ - BOOST_TEST(std::string(ex.error.assertion_code()) == \ - BOOST_PP_STRINGIZE(assertion)); \ - BOOST_TEST(ex.error.assertion_number() == 1); \ - pass = true; \ - } \ - assertion = true; \ - BOOST_TEST(pass); \ - -#define CHECK_THROW(body) \ - pass = false; \ - try { \ - body \ - } catch(forced_exception) { \ - std::cerr << "checking throw with no contract failure:" << std::endl; \ - std::cerr << " no broken contract: file \"" << __FILE__ << \ - "\", line " << __LINE__ << std::endl; \ - pass = true; \ - } \ - BOOST_TEST(pass); - -THROWING_HANDLER(class_inv_broken_on_entry) -THROWING_HANDLER(class_inv_broken_on_exit) -THROWING_HANDLER(class_inv_broken_on_throw) -THROWING_HANDLER(pre_broken) -THROWING_HANDLER(post_broken) -THROWING_HANDLER(block_inv_broken) -THROWING_HANDLER(loop_var_broken) - -int main ( void ) -{ - contract::set_class_invariant_broken_on_entry( - &class_inv_broken_on_entry_handler); - contract::set_class_invariant_broken_on_exit( - &class_inv_broken_on_exit_handler); - contract::set_class_invariant_broken_on_throw( - &class_inv_broken_on_throw_handler); - contract::set_precondition_broken(&pre_broken_handler); - contract::set_postcondition_broken(&post_broken_handler); - contract::set_block_invariant_broken(&block_inv_broken_handler); - contract::set_loop_variant_broken(&loop_var_broken_handler); - - bool const throwing = true; - bool* const no_broken_inv = 0; - contract::from context; - bool pass = false; - - // Check constructor contract failures. - context = contract::FROM_CONSTRUCTOR; -#ifndef CONTRACT_CONFIG_NO_CLASS_INVARIANTS - // Fail static class invariants on entry. - CHECK(static_class_inv, class_inv_broken_on_entry, context, - static_class_inv = false; - failer failure; - ) - // Fail static class invariants on exit. - CHECK(static_class_inv, class_inv_broken_on_exit, context, - failer failure(&static_class_inv); - ) - // Fail static class invariants on throw. - CHECK(static_class_inv, class_inv_broken_on_throw, context, - failer failure(&static_class_inv, throwing); - ) - // Class invariants on entry do not apply. - // Fail class invariants on exit. - CHECK(class_inv, class_inv_broken_on_exit, context, - failer failure(&class_inv); - ) - // Class invariants on throw do not apply. - // Volatile class invariants on entry do not apply. - // Volatile class invariants on exit do not apply. - // Volatile class invariants on throw do not apply. -#endif -#ifndef CONTRACT_CONFIG_NO_PRECONDITIONS - // Fail preconditions on entry (before member initializers). - CHECK(pre, pre_broken, context, - pre = false; - failer failure; - ) -#endif -#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS - // Fail postconditions on exit (when no throw). - CHECK(post, post_broken, context, - post = false; - failer failure; - ) -#endif - // Throw with no contract failure. - CHECK_THROW( - failer failure(no_broken_inv, throwing); - ) - std::cerr << std::endl; - - // Check destructor contract failures. - context = contract::FROM_DESTRUCTOR; -#ifndef CONTRACT_CONFIG_NO_CLASS_INVARIANTS - // Fail static class invariants on entry. - CHECK(static_class_inv, class_inv_broken_on_entry, context, - failer failure; - static_class_inv = false; - ) - // Fail static class invariants on exit. - CHECK(static_class_inv, class_inv_broken_on_exit, context, - failer failure; - failure.destructor_inv = &static_class_inv; - ) - // Fail static class invariants on throw. - CHECK(static_class_inv, class_inv_broken_on_throw, context, - failer failure; - failure.destructor_inv = &static_class_inv; - failure.destructor_throwing = true; - ) - // Fail class invariants on entry. - CHECK(class_inv, class_inv_broken_on_entry, context, - failer failure; - class_inv = false; - ) - // Class invariants on exit do not apply. - // Fail class invariants on throw. - CHECK(class_inv, class_inv_broken_on_throw, context, - failer failure; - failure.destructor_inv = &class_inv; - failure.destructor_throwing = true; - ) - // Volatile class invariants on entry do not apply. - // Volatile class invariants on exit do not apply. - // Volatile class invariants on throw do not apply. -#endif - // Preconditions on entry do not apply. - // Postconditions on exit (when no throw) do not apply. - // Throw with no contract failure. - CHECK_THROW( - failer failure; - failure.destructor_throwing = true; - ) - std::cerr << std::endl; - - // Failure objects declared here to they are not destructed within the - // code checking member function contracts (otherwise, that code would also - // re-check constructor and destructor contracts all the times). - failer failure; - failer volatile volatile_failure; - - // Check non-static member function contract failures. - context = contract::FROM_NONSTATIC_MEMBER_FUNCTION; -#ifndef CONTRACT_CONFIG_NO_CLASS_INVARIANTS - // Fail static class invariants on entry. - CHECK(static_class_inv, class_inv_broken_on_entry, context, - static_class_inv = false; - failure.fail(); - ) - // Fail static class invariants on exit. - CHECK(static_class_inv, class_inv_broken_on_exit, context, - failure.fail(&static_class_inv); - ) - // Fail static class invariants on throw. - CHECK(static_class_inv, class_inv_broken_on_throw, context, - failure.fail(&static_class_inv, throwing); - ) - // Fail class invariants on entry. - CHECK(class_inv, class_inv_broken_on_entry, context, - class_inv = false; - failure.fail(); - ) - // Fail class invariants on exit. - CHECK(class_inv, class_inv_broken_on_exit, context, - failure.fail(&class_inv); - ) - // Fail class invariants on throw. - CHECK(class_inv, class_inv_broken_on_throw, context, - failure.fail(&class_inv, throwing); - ) - // Fail volatile class invariants on entry. - CHECK(volatile_class_inv, class_inv_broken_on_entry, context, - volatile_class_inv = false; - volatile_failure.fail(); - ) - // Fail volatile class invariants on exit. - CHECK(volatile_class_inv, class_inv_broken_on_exit, context, - volatile_failure.fail(&volatile_class_inv); - ) - // Fail volatile class invariants on throw. - CHECK(volatile_class_inv, class_inv_broken_on_throw, context, - volatile_failure.fail(&volatile_class_inv, throwing); - ) -#endif -#ifndef CONTRACT_CONFIG_NO_PRECONDITIONS - // Fail preconditions on entry. - CHECK(pre, pre_broken, context, - pre = false; - failure.fail(); - ) -#endif -#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS - // Fail postconditions on exit (when no throw). - CHECK(post, post_broken, context, - post = false; - failure.fail(); - ) -#endif - // Throw with no contract failure. - CHECK_THROW( - failure.fail(no_broken_inv, throwing); - ) - std::cerr << std::endl; - - // Check static member function contract failures. - context = contract::FROM_STATIC_MEMBER_FUNCTION; -#ifndef CONTRACT_CONFIG_NO_CLASS_INVARIANTS - // Fail static class invariants on entry. - CHECK(static_class_inv, class_inv_broken_on_entry, context, - static_class_inv = false; - failer::static_failure(); - ) - // Fail static class invariants on exit. - CHECK(static_class_inv, class_inv_broken_on_exit, context, - failer::static_failure(&static_class_inv); - ) - // Fail static class invariants on throw. - CHECK(static_class_inv, class_inv_broken_on_throw, context, - failer::static_failure(&static_class_inv, throwing); - ) - // Class invariants on entry do not apply. - // Class invariants on exit do not apply. - // Class invariants on throw do not apply. - // Volatile class invariants on entry do not apply. - // Volatile class invariants on exit do not apply. - // Volatile class invariants on throw do not apply. -#endif -#ifndef CONTRACT_CONFIG_NO_PRECONDITIONS - // Fail preconditions on entry. - CHECK(pre, pre_broken, context, - pre = false; - failer::static_failure(); - ) -#endif -#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS - // Fail postconditions on exit (when no throw). - CHECK(post, post_broken, context, - post = false; - failer::static_failure(); - ) -#endif - // Throw with no contract failure. - CHECK_THROW( - failer::static_failure(no_broken_inv, throwing); - ) - std::cerr << std::endl; - - // Check free function contract failures. - context = contract::FROM_FREE_FUNCTION; - // Static class invariants on entry do not apply. - // Static class invariants on exit do not apply. - // Static class invariants on throw do not apply. - // Class invariants on entry do not apply. - // Class invariants on exit do not apply. - // Class invariants on throw do not apply. - // Volatile class invariants on entry do not apply. - // Volatile class invariants on exit do not apply. - // Volatile class invariants on throw do not apply. -#ifndef CONTRACT_CONFIG_NO_PRECONDITIONS - // Fail preconditions on entry. - CHECK(pre, pre_broken, context, - pre = false; - free_failure(); - ) -#endif -#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS - // Fail postconditions on exit (when no throw). - CHECK(post, post_broken, context, - post = false; - free_failure(); - ) -#endif - // Throw with no contract failure. - CHECK_THROW( - free_failure(throwing); - ) - std::cerr << std::endl; - - // Check block invariant contract failure. -#ifndef CONTRACT_CONFIG_NO_BLOCK_INVARIANTS - pass = false; - try { - CONTRACT_BLOCK_INVARIANT(false) - } catch(block_inv_broken) { - pass = true; - } - BOOST_TEST(pass); - std::cerr << std::endl; -#endif - - // Check loop variant contract failures. -#ifndef CONTRACT_CONFIG_NO_LOOP_VARIANTS - // OK, decreasing to 0. - CONTRACT_LOOP( for(int i = 0; i < 10; ++i) ) { - CONTRACT_LOOP_VARIANT( 9 - i ) - } - // Failure, decreasing to negative. - pass = false; - try { - CONTRACT_LOOP( for(int i = 0; i < 10; ++i) ) { - CONTRACT_LOOP_VARIANT( 8 - i ) - } - } catch(loop_var_broken) { - pass = true; - } - BOOST_TEST(pass); - // Failure, not decreasing. - pass = false; - try { - CONTRACT_LOOP( for(int i = 0; i < 10; ++i) ) { - CONTRACT_LOOP_VARIANT( 10 ) - } - } catch(loop_var_broken) { - pass = true; - } - BOOST_TEST(pass); - std::cerr << std::endl; -#endif - - return boost::report_errors(); -} - diff --git a/example/contracts/copy_inc.cpp b/example/contracts/copy_inc.cpp deleted file mode 100644 index facbd7a..0000000 --- a/example/contracts/copy_inc.cpp +++ /dev/null @@ -1,76 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include -#include - -//[copy_inc -CONTRACT_FUNCTION( - template( typename T ) - (T&) (inc) ( (T&) value, (T const&) offset ) - postcondition( - auto old_value = CONTRACT_OLDOF value, // Use `copy`. - auto result = return, // Would use `copy` but reference so no copy. - value == old_value + offset, requires - boost::has_plus::value and - boost::has_equal_to::value, - result == value, requires - boost::has_equal_to::value - ) -) { - return value += offset; -} - -class num : boost::noncopyable // Non-copyable (for some reason...). -{ - friend class contract::copy; // Contract copy is friend. - - public: explicit num ( int value ) : ptr_(new int(value)) {} - private: num ( num const& other ) : ptr_(other.ptr_) {} - public: ~num ( void ) { delete ptr_; } - - public: num operator+ ( num const& right ) const - { return num(*ptr_ + *right.ptr_); } - public: num& operator+= ( num const& right ) - { *ptr_ += *right.ptr_; return *this; } - public: bool operator== ( num const& right ) const - { return *ptr_ == *right.ptr_; } - - private: int* ptr_; -}; - -// Specialization disables old-of for non-copyable `num` (no C++ type trait can -// automatically detect copy constructors). -namespace contract -{ - template< > - class copy < num > - { - public: explicit copy ( num const& n ) : num_(*n.ptr_) {} - public: num const& value ( void ) const { return num_; } - - private: num num_; - }; -} // namespace -//] - -int main ( void ) -{ - //[copy_inc_call - int i = 1, j = 2; - BOOST_TEST(inc(i, j) == 3); - - num n(1), m(2); - BOOST_TEST(inc(n, m) == num(3)); - //] - return boost::report_errors(); -} - diff --git a/example/contracts/default_subcontracting_base.cpp b/example/contracts/default_subcontracting_base.cpp deleted file mode 100644 index 1030b3a..0000000 --- a/example/contracts/default_subcontracting_base.cpp +++ /dev/null @@ -1,34 +0,0 @@ - -#include -#include - -//[default_subcontracting_base -CONTRACT_CLASS( - class (base) // Declared with contract macros. -) { - CONTRACT_CLASS_INVARIANT( std::clog << "base::inv" << std::endl ) - - CONTRACT_FUNCTION( - public virtual void (f) ( void ) - precondition( std::clog << "base::f::pre" << std::endl ) - postcondition( std::clog << "base::f::post" << std::endl ) - ) = 0; -}; - -class deriv : public base // Declared without contract macros... -{ - // ...but using `BODY` instead of `CLASS` and `FUNCTION` macros, overriding - // functions have exact same contracts as base (not real subcontracting). - public: virtual void CONTRACT_MEMBER_BODY(f) ( void ) - { - std::clog << "deriv::f::body" << std::endl; - } -}; -//] - -int main ( void ) -{ - deriv().f(); // Check `base::f` contract but execute `deriv::f` body. - return 0; -} - diff --git a/example/contracts/exception_array.cpp b/example/contracts/exception_array.cpp deleted file mode 100644 index 9bcb8c8..0000000 --- a/example/contracts/exception_array.cpp +++ /dev/null @@ -1,75 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[exception_array -CONTRACT_CLASS( - template( typename T ) - class (array) -) { - CONTRACT_CLASS_INVARIANT_TPL( size() >= 0 ) - - public: struct out_of_memory {}; - public: struct error {}; - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (array) ( size_t count ) - precondition( count >= 0 ) - postcondition( size() == count ) - // Function try-blocks are programmed within the macros only for - // constructors with member initializers otherwise they are - // programmed with the body definitions and outside the macros. - try initialize( // Try block for constructor initializers and body. - data_(new T[count]), - size_(count) - // Use `BOOST_IDENTITY_TYPE` if the exception type has unwrapped - // commas or leading symbols. - ) catch(std::bad_alloc&) ( - throw out_of_memory(); - ) catch(...) ( - throw error(); - ) - ) {} - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~array) ( void ) throw( void ) // Throw nothing. - ) { - delete[] data_; - } - - // ... -//] - - CONTRACT_FUNCTION_TPL( - public size_t (size) ( void ) const - ) { - return size_; - } - - CONTRACT_FUNCTION_TPL( - public (T&) operator([])(at) ( size_t index ) - precondition( index >= 0, index < size() ) - ) { - return data_[index]; - } - - private: T* data_; - private: size_t size_; -}; - -int main ( void ) -{ - array a(3); - BOOST_TEST(a.size() == 3); - a[0] = 1; BOOST_TEST(a[0] == 1); - a[1] = 2; BOOST_TEST(a[1] == 2); - a[2] = 3; BOOST_TEST(a[2] == 3); - return boost::report_errors(); -} - diff --git a/example/contracts/friend_counter.cpp b/example/contracts/friend_counter.cpp deleted file mode 100644 index 35009d6..0000000 --- a/example/contracts/friend_counter.cpp +++ /dev/null @@ -1,106 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[friend_counter -CONTRACT_CLASS( // Not even necessary to contract this class. - template( typename T ) requires( boost::CopyConstructible ) - class (counter) -) { - CONTRACT_CLASS_INVARIANT_TPL( value() >= 0 ); - - CONTRACT_FUNCTION_TPL( // Friend (contracted declaration and definition). - public friend (counter) operator(/)(div) ( (counter const&) left, - (T const&) right ) - precondition( right > 0 ) // Strictly positive, cannot be zero. - postcondition( - auto result = return, - result.value() * right == left.value() - ) - ) { - return counter(left.value() / right); - } - - // Friend forward declaration (contracted declaration and definition below). - public: template< typename U > - friend bool CONTRACT_FREE_BODY(operator(==)(equal)) ( // Use BODY. - counter const& left, U const& right ) ; - -// NOTE: Forward friend template instantiations give internal MSVC error. -#if defined(BOOST_MSVC) && !defined(CONTRACT_CONFIG_NO_POSTCONDITIONS) - // Friend definition (contracted declaration below). - public: friend counter CONTRACT_FREE_BODY(operator(*)(mult)) ( // Use BODY. - counter const& left, T const& right ) - { - return counter(left.value() * right); // Contract checked `right >=0` . - } -#endif - - CONTRACT_CONSTRUCTOR_TPL( // Public constructor gets next counter value. - public explicit (counter) ( void ) - initialize( value_(next_value_++) ) - ) {} - - CONTRACT_CONSTRUCTOR_TPL( // Private constructor. - private explicit (counter) ( (T const&) a_value ) - precondition( a_value >= 0 ) - postcondition( value() == a_value ) - initialize( value_(a_value) ) - ) {} - - CONTRACT_FUNCTION_TPL( - public (T) (value) ( void ) const - postcondition( auto result = return, result >= 0 ) - ) { - return value_; - } - - private: T value_; - private: static T next_value_; -}; - -template -T counter::next_value_ = T(); - -CONTRACT_FUNCTION( - template( typename U ) - bool operator(==)(equal) ( (counter const&) left, (U const&) right ) - precondition( right >= 0 ) - postcondition( - auto result = return, - result == (left.value() == right) - ) -) { - return left.value() == right; -} - -#if defined(BOOST_MSVC) && !defined(CONTRACT_CONFIG_NO_POSTCONDITIONS) -CONTRACT_FUNCTION( - (counter) operator(*)(mult) ( (counter const&) left, - (int const&) right ) - precondition( right >= 0 ) - postcondition( - auto result = return, - result.value() == left.value() * right - ) -) ; -#endif -//] - -int main ( void ) -{ - counter i0, i1, i2, i3, i4; - BOOST_TEST(i4 / 2 == 2); -#if defined(BOOST_MSVC) && !defined(CONTRACT_CONFIG_NO_POSTCONDITIONS) - BOOST_TEST(i3 * 2 == 6); -#endif - return boost::report_errors(); -} - diff --git a/example/contracts/function_template_postinc.cpp b/example/contracts/function_template_postinc.cpp deleted file mode 100644 index 85b4e02..0000000 --- a/example/contracts/function_template_postinc.cpp +++ /dev/null @@ -1,35 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[function_template_postinc -CONTRACT_FUNCTION( - template( typename T ) // Template parameter(s). - (T const) (postinc) ( (T&) value ) - precondition( value < std::numeric_limits::max() ) - postcondition( - auto result = return, - auto old_value = CONTRACT_OLDOF value, - value == old_value + 1, - result == old_value - ) -) { - return value++; -} -//] - -int main ( void ) -{ - int value = 1; - BOOST_TEST(postinc(value) == 1); - BOOST_TEST(value == 2); - return boost::report_errors(); -} - diff --git a/example/contracts/has_oldof_inc.cpp b/example/contracts/has_oldof_inc.cpp deleted file mode 100644 index 029cafb..0000000 --- a/example/contracts/has_oldof_inc.cpp +++ /dev/null @@ -1,68 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include -#include - -//[has_oldof_inc -CONTRACT_FUNCTION( - template( typename T ) - (T&) (inc) ( (T&) value, (T const&) offset ) - postcondition( - auto old_value = CONTRACT_OLDOF value, // Skip if no old-of. - auto result = return, // Never skipped. - value == old_value + offset, requires - contract::has_oldof::value and // Requires old-of. - boost::has_plus::value and - boost::has_equal_to::value, - result == value, requires - boost::has_equal_to::value - ) -) { - return value += offset; -} - -class num : boost::noncopyable // Non-copyable (for some reason...). -{ - public: explicit num ( int value ) : ptr_(new int(value)) {} - private: num ( num const& other ) : ptr_(other.ptr_) {} // Private copy. - public: ~num ( void ) { delete ptr_; } - - public: num operator+ ( num const& right ) const - { return num(*ptr_ + *right.ptr_); } - public: num& operator+= ( num const& right ) - { *ptr_ += *right.ptr_; return *this; } - public: bool operator== ( num const& right ) const - { return *ptr_ == *right.ptr_; } - - private: int* ptr_; -}; - -// Specialization disables old-of for non-copyable `num` (no C++ type trait can -// automatically detect copy constructors). -namespace contract -{ - template< > struct has_oldof < num > : boost::mpl::false_ {}; -} // namespace -//] - -int main ( void ) -{ - //[has_oldof_inc_call - int i = 1, j = 2; - BOOST_TEST(inc(i, j) == 3); - - num n(1), m(2); - BOOST_TEST(inc(n, m) == num(3)); - //] - return boost::report_errors(); -} - diff --git a/example/contracts/macro_commas_symbols_integral_map.cpp b/example/contracts/macro_commas_symbols_integral_map.cpp deleted file mode 100644 index 72ffd87..0000000 --- a/example/contracts/macro_commas_symbols_integral_map.cpp +++ /dev/null @@ -1,103 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include - -template< typename Key, typename T > -struct sizeable -{ - public: typedef typename std::map::size_type size_type; - public: static size_type const max_size = 100; - public: virtual size_type size( void ) const = 0; -}; - -//[macro_commas_symbols_integral_map -CONTRACT_CLASS( - template( - typename Key, - typename T, // Commas in following template params. - class Allocator, - default (::std::allocator >), - (typename ::std::map::key_type) default_key, - default (-1) - ) requires( (boost::Convertible) ) // Commas in concepts. - class (integral_map) - extends( public (::sizeable) ) // Commas in bases. -) { - CONTRACT_CLASS_INVARIANT_TPL( // Commas in class invariants. - (::sizeable::max_size) >= size() - ) - - public: typedef typename std::map, Allocator>:: - iterator iterator; - - CONTRACT_FUNCTION_TPL( - public template( typename OtherKey, typename OtherT ) - requires( - (::boost::Convertible), - (::boost::Convertible) - ) - (::std::pair) (insert) ( // Commas in result and params. - (::std::pair const&) other_value, - default (::std::pair(default_key, T())) - ) throw( (::std::pair) ) // Commas in exception specs. - precondition( // Leading symbols in preconditions (same for commas). - ((!full())) // LIMITATION: Two sets `((...))` (otherwise seq.). - ) - postcondition( // Commas in postconditions. - auto result = return, - (typename sizeable::size_type) - old_other_size = CONTRACT_OLDOF - (size()), - (::sizeable::max_size) >= size(), - size() == old_other_size + (result.second ? 1 : 0) - ) - ) { - // ... -//] - std::pair value(other_value.first, other_value.second); - std::pair result = map_.insert(value); - if(size() > sizeable::max_size) throw value; - return result; - } - - public: bool full ( void ) const - { return size() == sizeable::max_size; } - - public: typename sizeable::size_type size ( void ) const - { return map_.size(); } - - public: template< typename OtherKey, typename OtherT > - typename sizeable::size_type size ( void ) const - { return map_.size(); } - - public: T& operator[] ( Key const& key ) { return map_[key]; } - - private: std::map, Allocator> map_; -}; - -int main ( void ) -{ - integral_map m; - m.insert(std::make_pair(123, 'a')); - BOOST_TEST(m[char(123)] == int('a')); - m.insert(); - BOOST_TEST(m[char(-1)] == int()); - - // Test an implementation detail. - BOOST_TEST(CONTRACT_DETAIL_PP_IS_VARIADIC( (std::pair) ) == 1); - BOOST_TEST(CONTRACT_DETAIL_PP_IS_VARIADIC( (std::pair) p) == 1); - BOOST_TEST(CONTRACT_DETAIL_PP_IS_VARIADIC( false ) == 1); - BOOST_TEST(CONTRACT_DETAIL_PP_IS_VARIADIC( (!false) ) == 0); // Sequence. - - return boost::report_errors(); -} - diff --git a/example/contracts/macro_commas_symbols_integral_map_seq.cpp b/example/contracts/macro_commas_symbols_integral_map_seq.cpp deleted file mode 100644 index 8160eda..0000000 --- a/example/contracts/macro_commas_symbols_integral_map_seq.cpp +++ /dev/null @@ -1,96 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include - -template< typename Key, typename T > -struct sizeable -{ - public: typedef typename std::map::size_type size_type; - public: static size_type const max_size = 100; - public: virtual size_type size( void ) const = 0; -}; - -//[macro_commas_symbols_integral_map_seq -CONTRACT_CLASS( - template( - (typename Key) - (typename T) - (class Allocator) - (default comma(1)(::std::allocator >)) - (comma(1)(typename ::std::map::key_type) default_key) - (default (-1)) - ) requires( (comma(1)(boost::Convertible)) ) - class (integral_map) - extends( (public comma(1)(::sizeable)) ) -) { - CONTRACT_CLASS_INVARIANT_TPL( - (((::sizeable::max_size)) >= size()) - ) - - public: typedef typename std::map, Allocator>:: - iterator iterator; - - CONTRACT_FUNCTION_TPL( - public template( (typename OtherKey) (typename OtherT) ) - requires( - (comma(1)(::boost::Convertible)) - (comma(1)(::boost::Convertible)) - ) - comma(1)(::std::pair) (insert) ( - (comma(1)(::std::pair const&) other_value) - (default comma(1)(::std::pair(default_key, T()))) - ) throw( (comma(1)(::std::pair)) ) - precondition( - ((!full())) - ) - postcondition( - (auto result = return) - (comma(1)(typename sizeable::size_type) - old_other_size = CONTRACT_OLDOF - (size())) - (((::sizeable::max_size)) >= size()) - (size() == old_other_size + (result.second ? 1 : 0)) - ) - ) { - // ... -//] - std::pair value(other_value.first, other_value.second); - std::pair result = map_.insert(value); - if(size() > sizeable::max_size) throw value; - return result; - } - - public: bool full ( void ) const - { return size() == sizeable::max_size; } - - public: typename sizeable::size_type size ( void ) const - { return map_.size(); } - - public: template< typename OtherKey, typename OtherT > - typename sizeable::size_type size ( void ) const - { return map_.size(); } - - public: T& operator[] ( Key const& key ) { return map_[key]; } - - private: std::map, Allocator> map_; -}; - -int main ( void ) -{ - integral_map m; - m.insert(std::make_pair(123, 'a')); - BOOST_TEST(m[char(123)] == int('a')); - m.insert(); - BOOST_TEST(m[char(-1)] == int()); - return boost::report_errors(); -} - diff --git a/example/contracts/macro_commas_symbols_integral_map_seq_nova.cpp b/example/contracts/macro_commas_symbols_integral_map_seq_nova.cpp deleted file mode 100644 index a0c49ae..0000000 --- a/example/contracts/macro_commas_symbols_integral_map_seq_nova.cpp +++ /dev/null @@ -1,10 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include "nova.hpp" -#include "macro_commas_symbols_integral_map_seq.cpp" - diff --git a/example/contracts/member_operator_string.cpp b/example/contracts/member_operator_string.cpp deleted file mode 100644 index ef0b356..0000000 --- a/example/contracts/member_operator_string.cpp +++ /dev/null @@ -1,136 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include -#include - -//[member_operator_string -CONTRACT_CLASS( - class (string) -) { - CONTRACT_CLASS_INVARIANT( - static class( pointers >= 0, arrays >= 0 ) - ) - - public: static int pointers; - public: static int arrays; - - CONTRACT_CONSTRUCTOR( - public explicit (string) ( (char const*) c_str, default("") ) - initialize( string_(c_str) ) - ) {} - - CONTRACT_DESTRUCTOR( - public (~string) ( void ) - ) {} - - CONTRACT_FUNCTION( // Symbolic operators: `(==)(equal)`, `(())(call)`, etc. - public bool operator(==)(equal) ( (string const&) right ) const - ) { - return string_ == right.string_; - } - - CONTRACT_FUNCTION( // Implicit type conversion operator (keyword type). - public operator char const ( void ) const - ) { - return string_[0]; - } - - CONTRACT_FUNCTION( // Implicit type conversion operator (symbolic type). - public operator(char const*)(char_const_ptr) ( void ) const - ) { - return string_.c_str(); - } - - CONTRACT_FUNCTION( // Implicit type conversion operator (type with commas). - public template( typename T, class Allocator ) - operator(std::vector)(std_vector) ( void ) const - ) { - std::vector v(string_.size()); - for(size_t i = 0; i < string_.size(); ++i) v[i] = string_[i]; - return v; - } - - CONTRACT_FUNCTION( // Comma operator (use `comma` to diff. from above). - public (string&) operator comma ( (string const&) right ) - ) { - string_ += right.string_; - return *this; - } - - // All memory operators (new, delete, new[], and delete[]) must be - // explicitly `static` (because pp can't inspect new[] and delete[] that - // could be any symbolic operator like ==, +, etc). - - CONTRACT_FUNCTION( - public static (void*) operator new ( size_t size ) - ) { - void* p = malloc(size); - if(p == 0) throw std::bad_alloc(); - pointers++; - return p; - } - - CONTRACT_FUNCTION( - public static void operator delete ( (void*) pointer ) - ) { - if(pointer) { - free(pointer); - pointers--; - } - } - - CONTRACT_FUNCTION( - public static (void*) operator(new[])(new_array) ( size_t size ) - ) { - void* a = malloc(size); - if(a == 0) throw std::bad_alloc(); - arrays++; - return a; - } - - CONTRACT_FUNCTION( - public static void operator(delete[])(delete_array) ( (void*) array ) - ) { - if(array) { - free(array); - arrays--; - } - } - - private: std::string string_; -}; - -int string::pointers = 0; -int string::arrays = 0; -//] - -int main ( void ) -{ - string const xyz("xyz"); - - string s("abc"); BOOST_TEST(s == string("abc")); - BOOST_TEST((s, xyz) == string("abcxyz")); - - char x = xyz; BOOST_TEST(x == 'x'); - char const* c_xyz = xyz; BOOST_TEST(string(c_xyz) == xyz); - - std::vector > v = xyz; - BOOST_TEST(v[0] == 'x' && v[1] == 'y' && v[2] == 'z'); - - string* p = new string; BOOST_TEST(string::pointers == 1); - delete p; BOOST_TEST(string::pointers == 0); - - string* a = new string[5]; BOOST_TEST(string::arrays == 1); - delete[] a; BOOST_TEST(string::arrays == 0); - - return boost::report_errors(); -} - diff --git a/example/contracts/nested_class_bitset.cpp b/example/contracts/nested_class_bitset.cpp deleted file mode 100644 index df1ba2c..0000000 --- a/example/contracts/nested_class_bitset.cpp +++ /dev/null @@ -1,112 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include - -//[nested_class_bitset -CONTRACT_CLASS( // Enclosing class. - template( size_t N ) - class (bitset) -) { - CONTRACT_CLASS_INVARIANT_TPL( - static class( size() == N ) - ) - - CONTRACT_CLASS_TPL( // Nested class. - public class (reference) - ) { - CONTRACT_CLASS_INVARIANT_TPL( bitptr_ ) - - friend class bitset; - - CONTRACT_CLASS_TPL( // Nested (twice) class template with concepts. - private template( typename T ) - requires( boost::DefaultConstructible ) - class (bit) - ) { - CONTRACT_CLASS_INVARIANT_TPL( void ) - - CONTRACT_CONSTRUCTOR_TPL( - public (bit) ( void ) - initialize( value_() ) - ) {} - - CONTRACT_FUNCTION_TPL( - public void (from_bool) ( bool value ) - postcondition( to_bool() == value ) - ) { - value_ = value; - } - - CONTRACT_FUNCTION_TPL( - public bool (to_bool) ( void ) const - ) { - return value_; - } - - private: T value_; - }; - - CONTRACT_CONSTRUCTOR_TPL( - private (reference) ( void ) - postcondition( bitptr_->to_bool() == int() ) - initialize( - bitptr_(boost::shared_ptr >(new bit())) - ) - ) {} - - CONTRACT_DESTRUCTOR_TPL( - public (~reference) ( void ) - ) {} - - CONTRACT_FUNCTION_TPL( - public operator bool ( void ) const - ) { - return bitptr_->to_bool(); - } - - CONTRACT_FUNCTION_TPL( - public (reference&) operator(=)(assign) ( bool const bit_value ) - postcondition( auto result = return, result == *this ) - ) { - bitptr_->from_bool(bit_value); - return *this; - } - - private: boost::shared_ptr > bitptr_; - }; - - CONTRACT_FUNCTION_TPL( - public (reference) operator([])(at) ( size_t index ) - precondition( index < N ) - ) { - return bitset_[index]; - } - - CONTRACT_FUNCTION_TPL( - public static size_t (size) ( void ) - ) { - return N; - } - - private: reference bitset_[N]; -}; -//] - -int main ( void ) -{ - bitset<2> b; - b[0] = true; - BOOST_TEST(b[0]); - b[1] = false; - BOOST_TEST(not b[1]); - return boost::report_errors(); -} - diff --git a/example/contracts/no_contract_ivector.cpp b/example/contracts/no_contract_ivector.cpp deleted file mode 100644 index b01c1aa..0000000 --- a/example/contracts/no_contract_ivector.cpp +++ /dev/null @@ -1,48 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include - -//[no_contract_ivector -class ivector -{ - // invariant: empty() == (size() == 0) - // size() <= capacity() - // capacity() <= max_size() - // std::distance(begin(), end()) == int(size()) - - public: typedef std::vector::size_type size_type; - - public: explicit ivector ( size_type count ) - // precondition: count >= 0 - // postcondition: size() == count - // boost::algorithm::all_of_equal(begin(), end(), 0) - : vector_(count) - {} - - public: virtual ~ivector ( void ) {} - - public: void push_back ( int const value ) - // precondition: size() < max_size() - // postcondition: size() == oldof size() + 1 - // capacity() >= oldof capacity() - // back() == value - { - vector_.push_back(value); - } - - private: std::vector vector_; -}; -//] - -int main ( void ) -{ - ivector v(1); - v.push_back(123); - return 0; -} - diff --git a/example/contracts/no_contract_postinc.cpp b/example/contracts/no_contract_postinc.cpp deleted file mode 100644 index 2eaa89d..0000000 --- a/example/contracts/no_contract_postinc.cpp +++ /dev/null @@ -1,27 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include - -//[no_contract_postinc -int const postinc ( int& value ) - // precondition: value < std::numeric_limits::max() - // postcondition: value == oldof value + 1 - // result == oldof valule -{ - return value++; -} -//] - -int main ( void ) -{ - int value = 1; - BOOST_TEST(postinc(value) == 1); - BOOST_TEST(value == 2); - return boost::report_errors(); -} - diff --git a/example/contracts/no_pre_post_postinc.cpp b/example/contracts/no_pre_post_postinc.cpp deleted file mode 100644 index a345996..0000000 --- a/example/contracts/no_pre_post_postinc.cpp +++ /dev/null @@ -1,30 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include - -//[no_pre_post_postinc -#include - -CONTRACT_FUNCTION( // Declare free function (for programming contracts). - int const (postinc) ( (int&) value ) // Non-fundamental types in `()`. - // precondition: value < std::numeric_limits::max() - // postcondition: value == oldof value + 1 - // result == oldof value -) { - return value++; -} -//] - -int main ( void ) -{ - int value = 1; - BOOST_TEST(postinc(value) == 1); - BOOST_TEST(value == 2); - return boost::report_errors(); -} - diff --git a/example/contracts/nova.hpp b/example/contracts/nova.hpp deleted file mode 100644 index 4414741..0000000 --- a/example/contracts/nova.hpp +++ /dev/null @@ -1,21 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#ifndef NOVA_HPP_ -#define NOVA_HPP_ - -// WARNING: This file must be included first in each compilation unit. - -#include - -// Force no variadic macros but avoiding macro redefinition warnings/errors. -#ifndef BOOST_NO_VARIADIC_MACROS -# define BOOST_NO_VARIADIC_MACROS -#endif - -#endif // #include guard - diff --git a/example/contracts/params_funcptr_array_apply.cpp b/example/contracts/params_funcptr_array_apply.cpp deleted file mode 100644 index 7db456d..0000000 --- a/example/contracts/params_funcptr_array_apply.cpp +++ /dev/null @@ -1,50 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[params_funcptr_array_apply -// Contracts cannot directly use array type syntax, use via `typedef` instead. -typedef int array_2x3[2][3]; -typedef int (*func_ptr) ( int ); - -CONTRACT_FUNCTION( - void (apply) ( (func_ptr) f, (array_2x3) m ) - // precondition: f != NULL - // m != NULL -) { - for ( size_t i = 0; i < 2; ++i) - for ( size_t j = 0; j < 3; ++j) - m[i][j] = f(m[i][j]); -} - -int offset ( int i ) { return i + 10; } -//] - -int main ( void ) -{ - //[params_funcptr_array_apply_call - int x[2][3] = { - {1, 2, 3}, - {4, 5, 6} - }; - apply(offset, x); - //] - - BOOST_TEST(x[0][0] == 11); - BOOST_TEST(x[0][1] == 12); - BOOST_TEST(x[0][2] == 13); - - BOOST_TEST(x[1][0] == 14); - BOOST_TEST(x[1][1] == 15); - BOOST_TEST(x[1][2] == 16); - - return boost::report_errors(); -} - diff --git a/example/contracts/params_postinc.cpp b/example/contracts/params_postinc.cpp deleted file mode 100644 index 4c97e9d..0000000 --- a/example/contracts/params_postinc.cpp +++ /dev/null @@ -1,37 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[params_postinc -CONTRACT_FUNCTION( // Overload, storage classifiers, and default parameters. - long const (postinc) ( (long&) value, register unsigned offset, default 1 ) - // precondition: value < std::numeric_limits::max() - // postcondition: value == oldof value + offset - // result == oldof value -) { - long result = value; - if(offset > 0) { - value += 1; - postinc(value, offset - 1); // Recursive calls. - } - return result; -} -//] - -int main ( void ) -{ - //[params_postinc_call - long value = 1; - BOOST_TEST(postinc(value) == 1); // Increment of 1 (it is 1). - BOOST_TEST(postinc(value, 4) == 2); // Increment of 4 (it is 2). - BOOST_TEST(value == 6); // Incremented of 4 (it was 2). - //] - return boost::report_errors(); -} - diff --git a/example/contracts/post_also_postinc.cpp b/example/contracts/post_also_postinc.cpp deleted file mode 100644 index 3c25e0a..0000000 --- a/example/contracts/post_also_postinc.cpp +++ /dev/null @@ -1,34 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[post_also_postinc -CONTRACT_FUNCTION( - int const (postinc) ( (int&) value ) - precondition( value < std::numeric_limits::max() ) - postcondition( // Postconditions. - auto result = return, // Result value. - auto old_value = CONTRACT_OLDOF value, // Old value(s). - value == old_value + 1, // Assertion(s)... - result == old_value - ) -) { - return value++; -} -//] - -int main ( void ) -{ - int value = 1; - BOOST_TEST(postinc(value) == 1); - BOOST_TEST(value == 2); - return boost::report_errors(); -} - diff --git a/example/contracts/pre_only_postinc.cpp b/example/contracts/pre_only_postinc.cpp deleted file mode 100644 index 131ae50..0000000 --- a/example/contracts/pre_only_postinc.cpp +++ /dev/null @@ -1,30 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[pre_only_postinc -CONTRACT_FUNCTION( - int const (postinc) ( (int&) value ) - precondition( value < std::numeric_limits::max() ) // Precondition. - // postcondition: value == oldof value + 1 - // result == oldof value -) { - return value++; -} -//] - -int main ( void ) -{ - int value = 1; - BOOST_TEST(postinc(value) == 1); - BOOST_TEST(value == 2); - return boost::report_errors(); -} - diff --git a/example/contracts/push_back.cpp b/example/contracts/push_back.cpp deleted file mode 100644 index bab4efc..0000000 --- a/example/contracts/push_back.cpp +++ /dev/null @@ -1,56 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include - -//[push_back -#include // This library. -#include -#include "pushable.hpp" // Some base class. - -BOOST_CONTRACT_CLASS( - template( typename T ) - class (vector) extends( public pushable ) // Subcontracting. - invariant( - empty() == (size() == 0) // More class invariants here... - ) -) { -public: - typedef typename std::vector::size_type size_type; - typedef typename std::vector::const_reference const_reference; - - BOOST_CONTRACT_FUNCTION_TPL( - void (push_back) ( (T const&) value ) - 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)... - bool empty ( ) const { return vector_.empty(); } - size_type size ( ) const { return vector_.size(); } - size_type max_size ( ) const { return vector_.max_size(); } - const_reference back ( ) const { return vector_.back(); } - -private: - std::vector vector_; -}; -//] - -int main ( ) { - vector v; - v.push_back(123); - BOOST_TEST(v.size() == 1); - return boost::report_errors(); -} - diff --git a/example/contracts/push_back_lines.cpp b/example/contracts/push_back_lines.cpp deleted file mode 100644 index e1bcaa1..0000000 --- a/example/contracts/push_back_lines.cpp +++ /dev/null @@ -1,47 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[push_back_lines - 1 - 2 - 3 - 4 - 5 - 6 - 7 - 8 - 9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -//] - diff --git a/example/contracts/push_back_npaper.cpp b/example/contracts/push_back_npaper.cpp deleted file mode 100644 index 1c38998..0000000 --- a/example/contracts/push_back_npaper.cpp +++ /dev/null @@ -1,47 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[push_back_npaper -// Extra spaces, newlines, etc used to align text with this library code. -#include -#include -#include "pushable.hpp" // Some base class. - - -template< typename T > requires CopyConstructible // Concepts. -class vector : public pushable // Subcontracting. -{ - invariant { - empty() == (size() == 0); // More class invariants here... - } - - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::const_reference const_reference; - - - public: void push_back ( T const& value ) override - precondition { - size() < max_size(); // More preconditions here... - } - postcondition { - // Old-of values use `oldof` operator. - size() == oldof size() + 1; // More postconditions here... - } - { - vector_.push_back(value); // Original function body. - } - - // Rest of class here (with possibly 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 vector_; -}; -//] - diff --git a/example/contracts/pushable.hpp b/example/contracts/pushable.hpp deleted file mode 100644 index e6f243b..0000000 --- a/example/contracts/pushable.hpp +++ /dev/null @@ -1,40 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#ifndef PUSHABLE_HPP_ -#define PUSHABLE_HPP_ - -#include -#include -#include - -//[pushable -CONTRACT_CLASS( - template( typename T ) - class (pushable) -) { - // Subcontracting: In `and` with derived class invariants. - CONTRACT_CLASS_INVARIANT_TPL( void ) - - public: typedef typename std::vector::const_reference const_reference; - - CONTRACT_FUNCTION_TPL( - public virtual void (push_back) ( (T const&) value ) new - // Subcontracting: In `or` with overriding function preconditions. - precondition( false ) // Force check to overriding preconditions. - // Subcontracting: In `and` with overriding function postconditions. - postcondition( - back() == value, requires boost::has_equal_to::value - ) - ) = 0; // Contract for pure virtual function. - - public: virtual const_reference back ( void ) const = 0; -}; -//] - -#endif // #include guard - diff --git a/example/contracts/pushable_seq.hpp b/example/contracts/pushable_seq.hpp deleted file mode 100644 index 75d0ae6..0000000 --- a/example/contracts/pushable_seq.hpp +++ /dev/null @@ -1,40 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#ifndef PUSHABLE_HPP_ -#define PUSHABLE_HPP_ - -#include -#include -#include - -//[pushable_seq -CONTRACT_CLASS( - template( (typename T) ) - class (pushable) -) { - // Subcontracting: In `and` with derived class invariants. - CONTRACT_CLASS_INVARIANT_TPL( (void) ) - - public: typedef typename std::vector::const_reference const_reference; - - CONTRACT_FUNCTION_TPL( - public virtual void (push_back) ( ((T const&) value) ) new - // Subcontracting: In `or` with overriding function preconditions. - precondition( (false) ) // Force check to overriding preconditions. - // Subcontracting: In `and` with overriding function postconditions. - postcondition( - (back() == value)(requires boost::has_equal_to::value) - ) - ) = 0; // Contract for pure virtual function. - - public: virtual const_reference back ( void ) const = 0; -}; -//] - -#endif // #include guard - diff --git a/example/contracts/select_assertion_factorial.cpp b/example/contracts/select_assertion_factorial.cpp deleted file mode 100644 index 734dcbb..0000000 --- a/example/contracts/select_assertion_factorial.cpp +++ /dev/null @@ -1,37 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[select_assertion_factorial -CONTRACT_FUNCTION( - int (factorial) ( int n ) - precondition( n >= 0 ) - postcondition( - auto result = return, - result >= 1, - if(n == 0 or n == 1) ( // Select assertion, if-then statement. - result == 1 - ) else ( // Select assertion, else statement (optional). - // Assertions disabled within assertion so recursion OK. - result == n * factorial(n - 1) - ) - ) -) { - if(n == 0 or n == 1) return 1; - else return n * factorial(n - 1); -} -//] - -int main ( void ) -{ - BOOST_TEST(factorial(4) == 24); - return boost::report_errors(); -} - - diff --git a/example/contracts/static_assertion_memcopy.cpp b/example/contracts/static_assertion_memcopy.cpp deleted file mode 100644 index 1fb9fe1..0000000 --- a/example/contracts/static_assertion_memcopy.cpp +++ /dev/null @@ -1,43 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include - -//[static_assertion_memcopy -CONTRACT_FUNCTION( - template( typename To, typename From ) - (To*) (memcopy) ( (To*) to, (From*) from ) - precondition( // Static assertions. - static_assert(sizeof(To) >= sizeof(From), "destination too small"), - // Wrapping parenthesis for asserted condition with commas. - static_assert((boost::is_convertible::value), - "incompatible types"), - to, // pointer not null - from // pointer not null - ) -) ; -//] - -template< typename To, typename From > -To* CONTRACT_FREE_BODY(memcopy)( To* to, From* from ) -{ - memcpy(to, from, sizeof(From)); - return to; -} - -int main ( void ) -{ - int x = 0, y = 123; - memcopy(&x, &y); - BOOST_TEST(x == 123); - BOOST_TEST(y == 123); - return boost::report_errors(); -} - diff --git a/example/contracts/static_contract_instance_counter.cpp b/example/contracts/static_contract_instance_counter.cpp deleted file mode 100644 index 49289eb..0000000 --- a/example/contracts/static_contract_instance_counter.cpp +++ /dev/null @@ -1,77 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[static_contract_instance_counter -CONTRACT_CLASS( - template( typename T ) - class (instance_counter) -) { - CONTRACT_CLASS_INVARIANT_TPL( - object(), // Non-static class invariants. - static class( // Static class invariants. - count() >= 0 - // ... - ) - ) - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (instance_counter) ( (T*) the_object ) - precondition( the_object ) - postcondition( - auto old_count = CONTRACT_OLDOF count(), - count() == old_count + 1, - object() == the_object - ) - initialize( object_(the_object) ) - ) { - count_++; - } - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~instance_counter) ( void ) - // FUTURE: Destructors could have static postconditions. - // postcondition: count() = oldof count() - 1 - ) { - delete object_; - count_--; - } - - CONTRACT_FUNCTION_TPL( - public (T const* const) (object) ( void ) const - ) { - return object_; - } - - CONTRACT_FUNCTION_TPL( // Contract static member function. - public static int (count) ( void ) - // No preconditions nor postconditions for this example but when - // present no object can be accessed by assertions (i.e., `static`). - ) { - return count_; - } - - private: static int count_; - private: T* object_; -}; - -template< typename T > -int instance_counter::count_ = 0; -//] - -int main ( void ) -{ - instance_counter i(new int(123)), j(new int(456)); - BOOST_TEST(i.count() == 2); - BOOST_TEST(j.count() == 2); - BOOST_TEST(*(i.object()) == 123); - BOOST_TEST(*(j.object()) == 456); - return boost::report_errors(); -} - diff --git a/example/contracts/subcontract_identifiers.cpp b/example/contracts/subcontract_identifiers.cpp deleted file mode 100644 index 8447495..0000000 --- a/example/contracts/subcontract_identifiers.cpp +++ /dev/null @@ -1,115 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include -#include - -//[subcontract_identifiers_unique -CONTRACT_CLASS( - class (unique_identifiers) -) { - CONTRACT_CLASS_INVARIANT( size() >= 0 ) - - CONTRACT_CONSTRUCTOR( - public (unique_identifiers) ( void ) - postcondition( size() == 0 ) - ) {} - - CONTRACT_DESTRUCTOR( - public virtual (~unique_identifiers) ( void ) - ) {} - - CONTRACT_FUNCTION( - public virtual void (add) ( int id ) - precondition( - // Id not already present. - std::find(begin(), end(), id) == end() - ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - auto old_found = CONTRACT_OLDOF - std::find(begin(), end(), id) != end(), - // If id was not already present, it was added now... - old_found ? true : std::find(begin(), end(), id) != end(), - // ...and size was increased of 1. - old_found ? true : size() == old_size + 1 - ) - ) { - identifiers_.push_back(id); - } - - // ... -//] - - public: typedef std::vector::const_iterator const_iterator; - - // Should contract these members too... - public: int size ( void ) const { return identifiers_.size(); } - public: const_iterator begin ( void ) const { return identifiers_.begin(); } - public: const_iterator end ( void ) const { return identifiers_.end(); } - - protected: std::vector identifiers_; -}; - -//[subcontract_identifiers_duplicate -CONTRACT_CLASS( - class (duplicate_identifiers) - extends( public unique_identifiers ) // Automatically subcontract. -) { - CONTRACT_CLASS_INVARIANT( - size() >= 1 // Strengthened inherited class invariants (in `and`). - ) - - CONTRACT_CONSTRUCTOR( - public (duplicate_identifiers) ( int id ) - postcondition( size() == 1 ) - ) { - // As usual, constructor should not call virtual member `add`. - identifiers_.push_back(id); - } - - CONTRACT_DESTRUCTOR( - public virtual (~duplicate_identifiers) ( void ) - ) {} - - CONTRACT_FUNCTION( - public virtual void (add) ( int id ) - precondition( // Wakened inherited preconditions (in `or`). - // OK even if id is already present. - std::find(begin(), end(), id) != end() - ) - postcondition( // Strengthened inherited postconditions (in `and`). - auto old_size = CONTRACT_OLDOF size(), - auto old_found = CONTRACT_OLDOF - std::find(begin(), end(), id) != end(), - // Inherited postconditions not checked because of - // select assertions, plus size unchanged if already present. - old_found ? size() == old_size : true - ) - ) { - if(std::find(begin(), end(), id) == end()) { // Not already present. - // Unfortunately, must invoke base function via `BODY` macro. - unique_identifiers::CONTRACT_MEMBER_BODY(add)(id); - } - } -}; -//] - -int main ( void ) -{ - //[subcontract_identifiers_duplicate_add - duplicate_identifiers ids(123); - ids.add(123); - //] - BOOST_TEST(ids.size() == 1); // Not 2 because `add(123)` has no effect. - ids.add(456); - BOOST_TEST(ids.size() == 2); - return boost::report_errors(); -} - diff --git a/example/contracts/subcontract_pre_natural_failure.cpp b/example/contracts/subcontract_pre_natural_failure.cpp deleted file mode 100644 index a0f5834..0000000 --- a/example/contracts/subcontract_pre_natural_failure.cpp +++ /dev/null @@ -1,69 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include -#include - -//[subcontract_pre_natural_failure -CONTRACT_CLASS( - class (integer) -) { - CONTRACT_CLASS_INVARIANT( void ) - - CONTRACT_FUNCTION( - public virtual void (set) ( int value ) - // No preconditions so this and all overrides can always be called. - postcondition( get() == value ) - ) { - value_ = value; - } - - CONTRACT_FUNCTION( - public virtual int (get) ( void ) const - ) { - return value_; - } - - private: int value_; -}; - -CONTRACT_CLASS( - class (natural) extends( public integer ) // Subcontract. -) { - CONTRACT_CLASS_INVARIANT( get() >= 0 ) - - CONTRACT_FUNCTION( - public virtual void (set) ( int value ) - precondition( value >= 0 ) // NOTE: Will not fail because of base. - ) { - integer::CONTRACT_MEMBER_BODY(set)(value); - } -}; -//] - -void throwing_handler ( contract::from const& context ) { throw; } - -int main ( void ) -{ - contract::set_class_invariant_broken(&throwing_handler); - bool pass = false; - try { - //[subcontract_pre_natural_failure_call - natural n; - n.set(-123); // Error: Fails call invariants instead of preconditions. - //] - } catch(contract::broken& ex) { - if(std::string(ex.assertion_code()) == std::string("get() >= 0")) - pass = true; - } -#ifndef CONTRACT_CONFIG_NO_CLASS_INVARIANTS - BOOST_TEST(pass); -#endif - return boost::report_errors(); -} - diff --git a/example/contracts/template_params.cpp b/example/contracts/template_params.cpp deleted file mode 100644 index 2de5ef4..0000000 --- a/example/contracts/template_params.cpp +++ /dev/null @@ -1,64 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include - -template< - typename X - , template< typename S, typename T = S > class Y - , class Z = int - , Z V = 0 -> struct x {}; - -//[template_params_class -CONTRACT_CLASS( // Class template parameters. - template( - typename A // Type template parameter. - , int B // Value template parameter. - , class C, default A // Optional type template parameter. - , (A) D, default B // Optional value template parameter. - , template( // Template template parameter: Outer template - typename X // uses `()` but rest uses usual syntax. - , template< typename S, typename T = S > class Y - , class Z = int - , Z V = 0 - ) class E, default x // Optional template template parameter. - ) - struct (a) -) { - // ... -//] - CONTRACT_CLASS_INVARIANT_TPL( void ) -}; - -//[template_params_function -CONTRACT_FUNCTION( // Function template parameters. - template( // As usual, no default template parameters allowed in functions. - typename A // Type template parameter. - , int B // Value template parameter. - , class C // Type template parameter. - , (A) D // Value template parameter. - , template( // Template template parameter: Outer template - typename X // uses `()` but rest uses usual syntax. - , template< typename S, typename T = S > class Y - , class Z = int - , Z V = 0 - ) class E - ) - void (f) ( void ) -) { - // ... -//] -} - -int main ( void ) -{ - a aa; - f(); - return 0; -}; - diff --git a/example/contracts/template_specializations_vector.cpp b/example/contracts/template_specializations_vector.cpp deleted file mode 100644 index 01a3a81..0000000 --- a/example/contracts/template_specializations_vector.cpp +++ /dev/null @@ -1,128 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include "pushable.hpp" -#include -#include - -//[template_specializations_vector -CONTRACT_CLASS( // Not even necessary to contract this template. - template( typename T, class Allocator, default std::allocator ) - class (vector) extends( public pushable ) -) { - // ... -//] - CONTRACT_CLASS_INVARIANT_TPL( empty() == (size() == 0) ) - - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::const_reference - const_reference; - - CONTRACT_FUNCTION_TPL( - public void (push_back) ( (T const&) value ) - precondition( size() < max_size() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - size() == old_size + 1 - ) - ) { - std::cout << "T, Allocator" << std::endl; - vector_.push_back(value); - } - - 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 vector_; -}; - -//[template_specializations_vector_bool -CONTRACT_CLASS( // Template specialization (no template parameter). - template( void ) - class (vector) ( bool ) extends( public pushable ) -) { - // ... -//] - CONTRACT_CLASS_INVARIANT( empty() == (size() == 0) ) - - public: typedef std::vector::size_type size_type; - public: typedef std::vector::const_reference - const_reference; - - CONTRACT_FUNCTION( - public void (push_back) ( (bool const&) value ) - precondition( size() < max_size() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - size() == old_size + 1 - ) - ) { - std::cout << "bool" << std::endl; - vector_.push_back(value); - } - - 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 vector_; -}; - -//[template_specializations_vector_bool_allocator -CONTRACT_CLASS( // Template specialization (one template parameter). - template( class Allocator ) - class (vector) ( bool, Allocator ) extends( public pushable ) -) { - // ... -//] - CONTRACT_CLASS_INVARIANT_TPL( empty() == (size() == 0) ) - - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::const_reference - const_reference; - - CONTRACT_FUNCTION_TPL( - public void (push_back) ( (bool const&) value ) - precondition( size() < max_size() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - size() == old_size + 1 - ) - ) { - std::cout << "bool, Allocator" << std::endl; - vector_.push_back(value); - } - - 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 vector_; -}; - -int main ( void ) -{ - vector v; - v.push_back(123); - std::cout << v.size() << std::endl; - - vector b; - b.push_back(true); - std::cout << b.size() << std::endl; - - vector > bc; - bc.push_back(true); - std::cout << bc.size() << std::endl; - - return 0; -} - - diff --git a/example/contracts/typed_counter.cpp b/example/contracts/typed_counter.cpp deleted file mode 100644 index 8bde0e0..0000000 --- a/example/contracts/typed_counter.cpp +++ /dev/null @@ -1,41 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[typed_counter -CONTRACT_CLASS( - class (counter) -) { - CONTRACT_CLASS_INVARIANT( void ) - - public: static unsigned value; - - CONTRACT_FUNCTION( - public static int (next) ( void ) - postcondition( // Explicit types so no Boost.Typeof. - auto result = return, - unsigned const old_value = CONTRACT_OLDOF value, - const( unsigned value, unsigned const old_value ) - value == old_value + 1, - result == int(value) - ) - ) { - return ++value; - } -}; - -unsigned counter::value = 0; -//] - -int main ( void ) -{ - BOOST_TEST(counter::next() == 1); - return boost::report_errors(); -} - diff --git a/example/contracts/volatile_contract_shared_instance.cpp b/example/contracts/volatile_contract_shared_instance.cpp deleted file mode 100644 index 632bd65..0000000 --- a/example/contracts/volatile_contract_shared_instance.cpp +++ /dev/null @@ -1,63 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -#include -#include - -//[volatile_contract_shared_instance -CONTRACT_CLASS( - template( typename T ) - class (shared_instance) -) { - CONTRACT_CLASS_INVARIANT_TPL( - queries() >= 0, // Non-volatile class invariants. - volatile class( // Volatile class invariants. - object() - // ... - ) - ) - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (shared_instance) ( (T*) the_object ) - precondition( the_object ) - postcondition( object() == the_object ) - initialize( object_(the_object), queries_(0) ) - ) {} - - CONTRACT_DESTRUCTOR_TPL( - public virtual (~shared_instance) ( void ) - ) { - delete object_; - } - - CONTRACT_FUNCTION_TPL( // Contracts for volatile member function. - public (T const volatile* const) (object) ( void ) const volatile - // No preconditions nor postconditions for this example but when - // present object is `const volatile` within assertions. - ) { - queries_++; - return object_; - } - - CONTRACT_FUNCTION_TPL( - public int (queries) ( void ) const - ) { - return queries_; - } - - private: T volatile* object_; - private: mutable int queries_; -}; -//] - -int main ( void ) -{ - shared_instance volatile i(new int(123)); - BOOST_TEST(*(i.object()) == 123); - return boost::report_errors(); -} - diff --git a/example/meyer97/gcd.cpp b/example/meyer97/gcd.cpp deleted file mode 100644 index 6ad5a0c..0000000 --- a/example/meyer97/gcd.cpp +++ /dev/null @@ -1,42 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[meyer97_gcd -// File: gcd.cpp -#include -#include -#include - -CONTRACT_FUNCTION( // Great common divisor of given positive integers. - int (gcd) ( int a, int b ) - precondition( - a > 0, b > 0 - ) -) { - int x = a, y = b; - - CONTRACT_LOOP( while(x != y) ) { // Loop contracted with a variant. - // Block invariant assert loop invariant. - CONTRACT_BLOCK_INVARIANT( const( x ) x > 0, const( y ) y > 0 ) - // Loop variant is non-negative and monotonically decreasing. - CONTRACT_LOOP_VARIANT( const( x, y ) std::max(x, y) ) - - // `x` and `y` have the same GCD as `a` and `b`. - - if(x > y) x = x - y; else y = y - x; - } - return x; -} - -int main ( void ) -{ - BOOST_TEST(gcd(12, 18) == 6); - BOOST_TEST(gcd(4, 14) == 2); - return boost::report_errors(); -} -//] - diff --git a/example/meyer97/gcd.e b/example/meyer97/gcd.e deleted file mode 100644 index 53f3c79..0000000 --- a/example/meyer97/gcd.e +++ /dev/null @@ -1,42 +0,0 @@ - --- Copyright (C) 2008-2012 Lorenzo Caminiti --- Use, modification, and distribution is subject to the --- Boost Software License, Version 1.0 (see accompanying file --- LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt). --- Documentation at http://contractpp.sourceforge.net. - -//[meyer97_gcd_e --- File: gcd.e --- Extra spaces, newlines, etc used to align text with this library code. - - - --- Greatest common divisor of a and b. -gcd ( a, b : INTEGER ) : INTEGER is - require - a > 0; b > 0 - local - x, y : INTEGER - do - from - x := a; y := b - invariant - x > 0; y > 0 - variant - x.max(y) - until - x = y - loop - if x > y then x := x - y else y := y - x end - end - Result := x - end - - - - - - - -//] - diff --git a/example/meyer97/maxarray.cpp b/example/meyer97/maxarray.cpp deleted file mode 100644 index f1e43bb..0000000 --- a/example/meyer97/maxarray.cpp +++ /dev/null @@ -1,44 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[meyer97_maxarray -// File: maxarray.cpp -#include -#include -#include - -CONTRACT_FUNCTION( - int (maxarray) ( (int const* const) array, (size_t const&) size ) - precondition( - array, // array allocated - size >= 1 // size in range - ) -) { - int maxnow = array[0]; - CONTRACT_LOOP( for(size_t i = 0; i < (size - 1); ++i) ) { - // Nested loop (with variant) used to assert enclosing loop invariants. - CONTRACT_LOOP( for(size_t j = 0; j < i; ++j) ) { - CONTRACT_LOOP_VARIANT( const( i, j ) i - j ) - CONTRACT_BLOCK_INVARIANT( const( maxnow, array, j ) - maxnow >= array[j] ) - } - // -2 because starts from 0 (not 1) and already done element at 0. - CONTRACT_LOOP_VARIANT( const( size, i ) size - i - 2 ) - - maxnow = std::max(maxnow, array[i]); - } - return maxnow; -} - -int main ( void ) -{ - int a[] = {1, 5, 3}; - BOOST_TEST(maxarray(a, 3) == 5); - return boost::report_errors(); -} -//] - diff --git a/example/meyer97/stack3.cpp b/example/meyer97/stack3.cpp deleted file mode 100644 index 59d3ee6..0000000 --- a/example/meyer97/stack3.cpp +++ /dev/null @@ -1,164 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[meyer97_stack3 -// File: stack3.cpp -#include "stack4.hpp" -#include -#include - -CONTRACT_CLASS( // Dispenser LIFO and max capacity using error codes. - template( typename T ) - class (stack3) -) { - CONTRACT_CLASS_INVARIANT_TPL( void ) // no class invariant - - public: enum Error { // Error codes. - NO_ERROR = 0, - OVERFLOW_ERROR, - UNDERFLOW_ERROR, - SIZE_ERROR - }; - - // Initialization. - - // Create stack for max of n elements, if n < 0 set error (no precondition). - CONTRACT_CONSTRUCTOR_TPL( - public (stack3) ( (const int&) n, (const T&) none, default T() ) - postcondition( - bool(n < 0) == (error() == SIZE_ERROR), // error if impossible - bool(n >= 0) == !error(), // no error if possible - if(bool(!error())) ( capacity() == n ) // created if no error - ) - initialize( none_(none), representation_(0), error_(NO_ERROR) ) - ) { - if(n >= 0) representation_ = stack4(n); - else error_ = SIZE_ERROR; - } - - CONTRACT_DESTRUCTOR_TPL( // Destroy stack. - public virtual (~stack3) ( void ) - ) {} - - // Access. - - CONTRACT_FUNCTION_TPL( // Max number of stack elements. - public int (capacity) ( void ) const - ) { - return representation_.capacity(); - } - - CONTRACT_FUNCTION_TPL( // Number of stack elements. - public int (count) ( void ) const - ) { - return representation_.count(); - } - - // Top element if present, otherwise set error (no precondition). - CONTRACT_FUNCTION_TPL( - public (const T&) (item) ( void ) const - postcondition( - empty() == (error() == UNDERFLOW_ERROR), // error if impossible - bool(!empty() == !error()) // no error if possible - ) - ) { - if(!empty()) { - error_ = NO_ERROR; - return representation_.item(); - } else { - error_ = UNDERFLOW_ERROR; - return none_; - } - } - - // Status report. - - CONTRACT_FUNCTION_TPL( // Error indicator set by various operations. - public (Error) (error) ( void ) const - ) { - return error_; - } - - CONTRACT_FUNCTION_TPL( // Is stack empty? - public bool (empty) ( void ) const - ) { - return representation_.empty(); - } - - CONTRACT_FUNCTION_TPL( // Is stack full? - public bool (full) ( void ) const - ) { - return representation_.full(); - } - - // Element change. - - // Add x to top if capacity left, otherwise set error (no precondition). - CONTRACT_FUNCTION_TPL( - public void (put) ( (const T&) x ) - postcondition( - auto old_full = CONTRACT_OLDOF full(), - auto old_count = CONTRACT_OLDOF count(), - old_full == (error() == OVERFLOW_ERROR), // error if impossible - not old_full == not error(), // no error if possible - if(not error()) ( - not empty(), // not empty if no error - item() == x, // added to top is no error - count() == old_count + 1 // one more item if no error - ) - ) - ) { - if(full()) { - error_ = OVERFLOW_ERROR; - } else { - representation_.put(x); - error_ = NO_ERROR; - } - } - - // Remove top item if possible, otherwise set error to (no precondition). - CONTRACT_FUNCTION_TPL( - public void (remove) ( void ) - postcondition( - auto old_empty = CONTRACT_OLDOF empty(), - auto old_count = CONTRACT_OLDOF count(), - old_empty == (error() == UNDERFLOW_ERROR), // if impossible - not old_empty == not error(), // no error if possible - if(not error()) ( - not full(), // not full is no error - count() == old_count - 1 // one fewer item if no error - ) - ) - ) { - if(empty()) { - error_ = UNDERFLOW_ERROR; - } else { - representation_.remove(); - error_ = NO_ERROR; - } - } - - private: const T none_; - private: stack4 representation_; - private: mutable Error error_; // Mutable for logic constantness. -}; - -int main ( void ) -{ - stack3 s(3); - BOOST_TEST(s.capacity() == 3); - BOOST_TEST(s.count() == 0); - BOOST_TEST(s.empty()); - BOOST_TEST(not s.full()); - s.put(123); - BOOST_TEST(s.item() == 123); - s.remove(); - BOOST_TEST(s.empty()); - return boost::report_errors(); -} -//] - diff --git a/example/meyer97/stack4.e b/example/meyer97/stack4.e deleted file mode 100644 index 0ad23f7..0000000 --- a/example/meyer97/stack4.e +++ /dev/null @@ -1,211 +0,0 @@ - --- Copyright (C) 2008-2012 Lorenzo Caminiti --- Use, modification, and distribution is subject to the --- Boost Software License, Version 1.0 (see accompanying file --- LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt). --- Documentation at http://contractpp.sourceforge.net. - -//[meyer97_stack4_e --- File: stack4.e --- Extra spaces, newlines, etc used to align text with this library code. - - - - - - -indexing - destription: "Dispenser with LIFO access policy and a fixed max capacity." -class interface STACK4[G] creation make - -invariant - count_non_negative: count >= 0 - count_bounded: count <= capacity - empty_if_no_elements: empty = (count = 0) - - -feature -- Initialization. - - -- Allocate stack for a maximum of n elements. - make ( n : INTEGER ) is - require - non_negative_capacity: n >= 0 - - ensure - capacity_set: capacity = n - - end - - - - - - - - - - - - - - - - - - - - - - - -feature -- Access. - - -- Max number of stack elements. - capacity : INTEGER - - - -- Number of stack elements. - count : INTEGER - - - -- Top element - item : G is - require - not_empty: not empty -- i.e., count > 0 - - end - -feature -- Status report. - - -- Is stack empty? - empty : BOOLEAN is - ensure - - empty_definition: result = (count = 0) - - end - - -- Is stack full? - full : BOOLEAN is - ensure - - full_definition: result = (count = capacity) - - end - -feature -- Element change. - - -- Add x on top. - put ( x : G ) is - require - not_full: not full - - ensure - - not_empty: not empty - added_to_top: item = x - one_more_item: count = old count + 1 - - end - - -- Remove top element. - remove is - require - not_empty: not empty -- i.e., count > 0 - - ensure - - not_full: not full - one_fewer_item: count = old count - 1 - - end - - - - -end -- class interface STACK4 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -//] - diff --git a/example/meyer97/stack4.hpp b/example/meyer97/stack4.hpp deleted file mode 100644 index af0e022..0000000 --- a/example/meyer97/stack4.hpp +++ /dev/null @@ -1,212 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[meyer97_stack4_header -// File: stack4.hpp -#ifndef STACK4_HPP_ -#define STACK4_HPP_ - -#include - -// Specification. - -CONTRACT_CLASS( // Dispenser with LIFO access policy and a fixed max capacity. - template( typename T ) - class (stack4) -) { - CONTRACT_CLASS_INVARIANT_TPL( - count() >= 0, // count non negative - count() <= capacity(), // count bounded - empty() == (count() == 0) // empty if no elements - ) - - // Initialization. - - CONTRACT_CONSTRUCTOR_TPL( // Allocate stack for a maximum of n elements. - public explicit (stack4) ( (const int&) n ) - precondition( - n >= 0 // non negative capacity - ) - postcondition( - capacity() == n // capacity set - ) - ) ; // Deferred body definition (see bottom). - - CONTRACT_CONSTRUCTOR_TPL( // Deep copy. - public (stack4) ( (const stack4&) right ) - postcondition( - capacity() == right.capacity(), - count() == right.count() - // all items equal right's items one by one - ) - ) ; - - CONTRACT_FUNCTION_TPL( // Deep assignment. - public (stack4&) operator(=)(assign) ( (const stack4&) right ) - postcondition( - capacity() == right.capacity(), - count() == right.count() - // all items equal right's items one by one - ) - ) ; - - CONTRACT_DESTRUCTOR_TPL( // Destroy this stack. - public virtual (~stack4) ( void ) - ) ; - - // Access. - - CONTRACT_FUNCTION_TPL( // Max number of stack elements. - public int (capacity) ( void ) const - ) ; - - CONTRACT_FUNCTION_TPL( // Number of stack elements. - public int (count) ( void ) const - ) ; - - CONTRACT_FUNCTION_TPL( // Top element. - public (const T&) (item) ( void ) const - precondition( - not empty() // not empty (i.e., count > 0) - ) - ) ; - - // Status report. - - CONTRACT_FUNCTION_TPL( // Is stack empty? - public bool (empty) ( void ) const - postcondition( - auto result = return, - result == (count() == 0) // empty definition - ) - ) ; - - CONTRACT_FUNCTION_TPL( // Is stack full? - public bool (full) ( void ) const - postcondition( - auto result = return, - result == (count() == capacity()) // full definition - ) - ) ; - - // Element change. - - CONTRACT_FUNCTION_TPL( // Add x on top. - public void (put) ( (const T&) x ) - precondition( - not full() // not full - ) - postcondition( - auto old_count = CONTRACT_OLDOF count(), - not empty(), // not empty - item() == x, // added to top - count() == old_count + 1 // one more item - ) - ) ; - - CONTRACT_FUNCTION_TPL( // Remove top item. - public void (remove) ( void ) - precondition( - not empty() // not empty (i.e., count > 0) - ) - postcondition( - auto old_count = CONTRACT_OLDOF count(), - not full(), // not full - count() == old_count - 1 // one fewer item - ) - ) ; - - private: int capacity_; - private: int count_; - private: T* representation_; // Using C-style array. -}; - -// Implementation. - -template< typename T > -CONTRACT_CONSTRUCTOR_BODY(stack4, stack4) ( const int& n ) -{ - capacity_ = n; - count_ = 0; - representation_ = new T[n]; -} - -template< typename T > -CONTRACT_CONSTRUCTOR_BODY(stack4, stack4) ( const stack4& right ) -{ - capacity_ = right.capacity_; - count_ = right.count_; - representation_ = new T[right.capacity_]; - for(int i = 0; i < right.count_; ++i) - representation_[i] = right.representation_[i]; -} - -template< typename T > -stack4& stack4::CONTRACT_MEMBER_BODY(operator(=)(assign)) ( - const stack4& right ) -{ - delete[] representation_; - capacity_ = right.capacity_; - count_ = right.count_; - representation_ = new T[right.capacity_]; - for(int i = 0; i < right.count_; ++i) - representation_[i] = right.representation_[i]; - return *this; -} - -template< typename T > -CONTRACT_DESTRUCTOR_BODY(stack4, ~stack4) ( void ) -{ - delete[] representation_; -} - -template< typename T > -int stack4::CONTRACT_MEMBER_BODY(capacity) ( void ) const -{ - return capacity_; -} - -template< typename T > -int stack4::CONTRACT_MEMBER_BODY(count) ( void ) const -{ - return count_; -} - -template< typename T > -const T& stack4::CONTRACT_MEMBER_BODY(item) ( void ) const -{ - return representation_[count() - 1]; -} - -template< typename T > -bool stack4::CONTRACT_MEMBER_BODY(empty) ( void ) const -{ - return count() == 0; -} - -template< typename T > -bool stack4::CONTRACT_MEMBER_BODY(full) ( void ) const -{ - return count() == capacity(); -} - -template< typename T > -void stack4::CONTRACT_MEMBER_BODY(put) ( const T& x ) -{ - representation_[count_++] = x; -} - -template< typename T > -void stack4::CONTRACT_MEMBER_BODY(remove) ( void ) -{ - --count_; -} - -#endif // #include guard -//] - - diff --git a/example/meyer97/stack4_main.cpp b/example/meyer97/stack4_main.cpp deleted file mode 100644 index 3b2b0ac..0000000 --- a/example/meyer97/stack4_main.cpp +++ /dev/null @@ -1,27 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[meyer97_stack4_main -// File: stack4_main.cpp -#include "stack4.hpp" -#include - -int main ( void ) -{ - stack4 s(3); - BOOST_TEST(s.capacity() == 3); - BOOST_TEST(s.count() == 0); - s.put(123); - BOOST_TEST(not s.empty()); - BOOST_TEST(not s.full()); - BOOST_TEST(s.item() == 123); - s.remove(); - BOOST_TEST(s.empty()); - return boost::report_errors(); -} -//] - diff --git a/example/mitchell02/counter/counter.hpp b/example/mitchell02/counter/counter.hpp deleted file mode 100644 index 55e3b7c..0000000 --- a/example/mitchell02/counter/counter.hpp +++ /dev/null @@ -1,59 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_counter_header -// File: counter/counter.hpp -#ifndef COUNTER_HPP_ -#define COUNTER_HPP_ - -#include "../observer/subject.hpp" -#include - -CONTRACT_CLASS( // Positive integer counter. - class (counter) extends( public subject ) -) { - CONTRACT_CLASS_INVARIANT( void ) // no invariants - - // Creation. - - CONTRACT_CONSTRUCTOR( // Construct counter with specified value. - public explicit (counter) ( int const a_value, default 10 ) - postcondition( value() == a_value ) // value set - initialize( value_(a_value) ) - ) {} - - CONTRACT_DESTRUCTOR( // Destroy counter. - public virtual (~counter) ( void ) - ) {} - - // Queries. - - CONTRACT_FUNCTION( // Current counter value. - public int (value) ( void ) const - ) { - return value_; - } - - // Commands. - - CONTRACT_FUNCTION( // Decrement counter value. - public void (decrement) ( void ) - postcondition( - auto old_value = CONTRACT_OLDOF value(), - value() == old_value - 1 // decremented - ) - ) { - --value_; - notify(); // Notifies all attached observers. - } - - private: int value_; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/counter/decrement_button.hpp b/example/mitchell02/counter/decrement_button.hpp deleted file mode 100644 index e4cd073..0000000 --- a/example/mitchell02/counter/decrement_button.hpp +++ /dev/null @@ -1,76 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_decrement_button_header -// File: counter/decrement_button.hpp -#ifndef DECREMENT_BUTTON_HPP_ -#define DECREMENT_BUTTON_HPP_ - -#include "push_button.hpp" -#include "counter.hpp" -#include "../observer/observer.hpp" -#include -#include - -CONTRACT_CLASS( // Button that decrements counter. - class (decrement_button) final // Contract for final class. - extends( public push_button, protected observer, boost::noncopyable ) -) { - CONTRACT_CLASS_INVARIANT( void ) // no invariant - - // Creation. - - CONTRACT_CONSTRUCTOR( // Create button associated with given counter. - public explicit (decrement_button) ( (counter&) the_counter ) - postcondition( - // enabled iff positive value - enabled() == (the_counter.value() > 0) - ) - initialize( counter_ref_(the_counter) ) - ) { - counter_ref_.attach(this); - } - - CONTRACT_DESTRUCTOR( // Destroy button. - public (~decrement_button) ( void ) - ) {} - - // Commands. - - CONTRACT_FUNCTION( - public void (on_bn_clicked) ( void ) override - postcondition( - old_value = CONTRACT_OLDOF counter_ref_.value(), - counter_ref_.value() == old_value - 1 // counter decremented - ) - ) { - counter_ref_.decrement(); - } - - CONTRACT_FUNCTION( - private bool (up_to_date_with_subject) ( void ) const override - ) { - return true; // For simplicity, always up-to-date. - } - - CONTRACT_FUNCTION( - private void (update) ( void ) override - postcondition( - // enabled if positive value - enabled() == (counter_ref_.value() > 0) - ) - ) { - if(counter_ref_.value() == 0) disable(); - else enable(); - } - - private: counter& counter_ref_; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/counter/push_button.hpp b/example/mitchell02/counter/push_button.hpp deleted file mode 100644 index b3e9265..0000000 --- a/example/mitchell02/counter/push_button.hpp +++ /dev/null @@ -1,66 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_push_button_header -// File: counter/push_button.hpp -#ifndef PUSH_BUTTON_HPP_ -#define PUSH_BUTTON_HPP_ - -#include - -CONTRACT_CLASS( // Basic button. - class (push_button) -) { - CONTRACT_CLASS_INVARIANT( void ) // no invariant - - // Creation. - - CONTRACT_CONSTRUCTOR( // Create an enabled button. - public (push_button) ( void ) - postcondition( enabled() ) // enabled - initialize( enabled_(true) ) - ) {} - - CONTRACT_DESTRUCTOR( // Destroy button. - public virtual (~push_button) ( void ) - ) {} - - // Queries. - - CONTRACT_FUNCTION( // If button enabled. - public bool (enabled) ( void ) const - ) { - return enabled_; - } - - // Commands. - - CONTRACT_FUNCTION( // Enable this button. - public void (enable) ( void ) - postcondition( enabled() ) // enabled - ) { - enabled_ = true; - } - - CONTRACT_FUNCTION( // Disable this button. - public void (disable) ( void ) - postcondition( not enabled() ) // disabled - ) { - enabled_ = false; - } - - CONTRACT_FUNCTION( // Invoked externally when this button is clicked. - public virtual void (on_bn_clicked) ( void ) new - precondition( enabled() ) // enabled - ) = 0; // Contract for pure virtual function. - - private: bool enabled_; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/counter_main.cpp b/example/mitchell02/counter_main.cpp deleted file mode 100644 index 1742ba2..0000000 --- a/example/mitchell02/counter_main.cpp +++ /dev/null @@ -1,64 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_counter_main -// File: counter_main.cpp -#include "counter/counter.hpp" -#include "counter/decrement_button.hpp" -#include "observer/observer.hpp" -#include - -int counter_check; - -CONTRACT_CLASS( // Show current value of associated counter. - class (view_of_counter) extends( private observer ) -) { - CONTRACT_CLASS_INVARIANT( void ) // no invariant - - // Creation. - - CONTRACT_CONSTRUCTOR( // Create viewer associated with given counter. - public explicit (view_of_counter) ( (counter&) the_counter ) - initialize( counter_ref_(the_counter) ) - ) { - counter_ref_.attach(this); - BOOST_TEST(counter_ref_.value() == counter_check); - } - - CONTRACT_DESTRUCTOR( // Destroy viewer. - public virtual (~view_of_counter) ( void ) - ) {} - - CONTRACT_FUNCTION( - private bool (up_to_date_with_subject) ( void ) const override final - ) { - return true; // For simplicity, always up-to-date. - } - - CONTRACT_FUNCTION( - private void (update) ( void ) override final // Contract final func. - ) { - BOOST_TEST(counter_ref_.value() == counter_check); - } - - private: counter& counter_ref_; -}; - -int main ( void ) -{ - counter count(counter_check = 1); - view_of_counter view(count); - decrement_button decrement(count); - BOOST_TEST(decrement.enabled()); - - counter_check--; - decrement.on_bn_clicked(); - BOOST_TEST(not decrement.enabled()); - return boost::report_errors(); -} -//] - diff --git a/example/mitchell02/courier.cpp b/example/mitchell02/courier.cpp deleted file mode 100644 index d61ced4..0000000 --- a/example/mitchell02/courier.cpp +++ /dev/null @@ -1,49 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_courier -// File: courier.cpp -#include "courier.hpp" - -// Courier. - -double courier::min_insurance_dollar = 10.0e+6; - -CONTRACT_CONSTRUCTOR_BODY(courier, courier) ( - double const an_insurance_cover_dollar ) -{ - insurance_cover_dollar_ = an_insurance_cover_dollar; -} - -CONTRACT_DESTRUCTOR_BODY(courier, ~courier) ( void ) {} - -double courier::CONTRACT_MEMBER_BODY(insurance_cover_dollar) ( void ) const - { return insurance_cover_dollar_; } - -void courier::CONTRACT_MEMBER_BODY(deliver) ( package& the_package, - std::string const destination ) -{ - the_package.location = destination; - // Delivery takes 2.5 hours. - the_package.delivered_hour = the_package.accepted_hour + 2.5; -} - -// Different courier. - -double different_courier::different_insurance_dollar = 20.0e+6; - -CONTRACT_DESTRUCTOR_BODY(different_courier, ~different_courier) ( void ) {} - -void different_courier::CONTRACT_MEMBER_BODY(deliver) ( package& the_package, - std::string const destination ) -{ - the_package.location = destination; - // Delivery takes only 0.5 hours. - the_package.delivered_hour = the_package.accepted_hour + 0.5; -} -//] - diff --git a/example/mitchell02/courier.hpp b/example/mitchell02/courier.hpp deleted file mode 100644 index f138cb8..0000000 --- a/example/mitchell02/courier.hpp +++ /dev/null @@ -1,133 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_courier_header -// File: courier.hpp -#ifndef COURIER_HPP_ -#define COURIER_HPP_ - -#include -#include - -struct package // Basic package information. -{ - public: double weight_kg; // Weight in kilograms. - public: std::string location; // Current location. - public: double accepted_hour; // Hour when it was accepted for delivery. - public: double delivered_hour; // Hour when it was delivered. - - public: explicit package ( - double const a_weight_kg, - std::string const a_location = "", - double const an_accepted_hour = 0.0, - double const a_delivered_hour = 0.0 - ) - : weight_kg(a_weight_kg), - location(a_location), - accepted_hour(an_accepted_hour), - delivered_hour(a_delivered_hour) - {} -}; - -CONTRACT_CLASS( // Basic courier for package delivery. - class (courier) -) { - CONTRACT_CLASS_INVARIANT( - insurance_cover_dollar() >= min_insurance_dollar, // above min insur. - static class( // Static class invariants. - min_insurance_dollar > 0.0 // positive min insurance - ) - ) - - public: static double min_insurance_dollar; - - // Creation. - - CONTRACT_CONSTRUCTOR( // Create courier with specified insurance value. - public explicit (courier) ( - double const an_insurance_cover_dollar, - default min_insurance_dollar - ) - precondition( an_insurance_cover_dollar > 0.0 ) // positive insur. - ) ; // Deferred body definition. - - CONTRACT_DESTRUCTOR( // Destroy courier. - public virtual (~courier) ( void ) - ) ; - - // Queries. - - CONTRACT_FUNCTION( // Return insurance cover. - public double (insurance_cover_dollar) ( void ) const - ) ; - - // Commands. - - CONTRACT_FUNCTION( // Deliver package to destination. - public virtual void (deliver) ( (package&) the_package, - (std::string const) destination ) - precondition( - the_package.weight_kg < 5.0 // within max wight - ) - postcondition( - double(the_package.delivered_hour - the_package.accepted_hour) - <= 3.0, // within max delivery time - the_package.location == destination // delivered at destination - ) - ) ; - - private: double insurance_cover_dollar_; -}; - -CONTRACT_CLASS( // Different courier for package delivery. - class (different_courier) extends( public courier ) -) { - CONTRACT_CLASS_INVARIANT( - insurance_cover_dollar() >= different_insurance_dollar, - static class( - different_insurance_dollar >= courier::min_insurance_dollar - ) - ) - - public: static double different_insurance_dollar; - - // Creation. - - CONTRACT_CONSTRUCTOR( // Create currier with specified insurance value. - public explicit (different_courier) ( - double const insurance_cover_dollar, - default different_insurance_dollar - ) - precondition( insurance_cover_dollar > 0.0 ) - initialize( courier(insurance_cover_dollar) ) - ) {} // Cannot separated body definition because has member initializers. - - CONTRACT_DESTRUCTOR( // Destroy courier. - public virtual (~different_courier) ( void ) - ) ; - - // Commands. - - CONTRACT_FUNCTION( - public virtual void (deliver) ( (package&) the_package, - (std::string const) destination ) override final - precondition( - // Weaker precondition on weight (it can weight more). - the_package.weight_kg <= 8.0 - ) - postcondition( - // Stronger postcondition on delivery time (faster delivery). - double(the_package.delivered_hour - the_package.accepted_hour) - <= 2.0 - // Inherits "delivered at destination" postcondition. - ) - ) ; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/courier_main.cpp b/example/mitchell02/courier_main.cpp deleted file mode 100644 index d4a84e9..0000000 --- a/example/mitchell02/courier_main.cpp +++ /dev/null @@ -1,23 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_courier_main -// File: courier_main.cpp -#include "courier.hpp" - -int main ( void ) -{ - courier c; - different_courier dc; - package cups(3.6, "store"); - package desk(7.2, "store"); - c.deliver(cups, "home"); - dc.deliver(desk, "office"); - return 0; -} -//] - diff --git a/example/mitchell02/customer_manager.cpp b/example/mitchell02/customer_manager.cpp deleted file mode 100644 index e96277c..0000000 --- a/example/mitchell02/customer_manager.cpp +++ /dev/null @@ -1,45 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_customer_manager -// File: customer_manager.cpp -#include "customer_manager.hpp" -#include - -CONTRACT_CONSTRUCTOR_BODY(customer_manager, customer_manager) ( void ) {} - -CONTRACT_DESTRUCTOR_BODY(customer_manager, ~customer_manager) ( void ) {} - -int customer_manager::CONTRACT_MEMBER_BODY(count) ( void ) const - { return customers_.size(); } - -bool customer_manager::CONTRACT_MEMBER_BODY(id_active) ( - basic_customer_details::identifier const& id) const -{ - return customers_.find(id) != customers_.end(); -} - -std::string const& customer_manager::CONTRACT_MEMBER_BODY(name_for) ( - basic_customer_details::identifier const& id) const -{ - // Find != end because of `id_active()` pre so no defensive programming. - return customers_.find(id)->second.name; -} - -void customer_manager::CONTRACT_MEMBER_BODY(add) ( - basic_customer_details const& details ) - { customers_.insert(std::make_pair(details.id, customer(details))); } - -void customer_manager::CONTRACT_MEMBER_BODY(set_name) ( - basic_customer_details::identifier const& id, - std::string const& name ) -{ - // Find != end because of `id_active()` pre so no defensive programming. - customers_.find(id)->second.name = name; -} -//] - diff --git a/example/mitchell02/customer_manager.hpp b/example/mitchell02/customer_manager.hpp deleted file mode 100644 index cd865a7..0000000 --- a/example/mitchell02/customer_manager.hpp +++ /dev/null @@ -1,109 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_customer_manager_header -// File: customer_manager.hpp -#ifndef CUSTOMER_MANAGER_HPP_ -#define CUSTOMER_MANAGER_HPP_ - -#include -#include -#include - -class basic_customer_details // Basic customer information. -{ - friend class customer_manager; - - public: typedef std::string identifier; - - public: explicit basic_customer_details ( identifier const& an_id ) - : id(an_id), name(), address(), birthday() - {} - - protected: identifier id; // Customer identifier. - protected: std::string name; // Customer name. - protected: std::string address; // Customer address. - protected: std::string birthday; // Customer date of birth. -}; - -CONTRACT_CLASS( // Manage customers. - class (customer_manager) -) { - CONTRACT_CLASS_INVARIANT( count() >= 0 ) // non-negative count - - // Creation. - - CONTRACT_CONSTRUCTOR( - public (customer_manager) ( void ) - // LIMITATION: Cannot use member initializes because deferring - // body definition. - ) ; // Deferred body definition. - - CONTRACT_DESTRUCTOR( - public virtual (~customer_manager) ( void ) - ) ; - - // Basic queries. - - CONTRACT_FUNCTION( - public int (count) ( void ) const - // postcondition: non-negative count asserted by class invariants - ) ; - - CONTRACT_FUNCTION( // There is a customer with given identifier. - public bool (id_active) ( - (basic_customer_details::identifier const&) id ) const - ) ; - - // Derived queries. - - CONTRACT_FUNCTION( // Name of customer with given identifier. - public (std::string const&) (name_for) ( - (basic_customer_details::identifier const&) id ) const - precondition( id_active(id) ) // id active - ) ; - - // Commands. - - CONTRACT_FUNCTION( // Add given customer. - public void (add) ( (basic_customer_details const&) details ) - precondition( not id_active(details.id) ) // id not active - postcondition( - auto old_count = CONTRACT_OLDOF count(), - count() == old_count + 1, // count increased - id_active(details.id) // id active - ) - ) ; - - CONTRACT_FUNCTION( // Set name of customer with given identifier. - public void (set_name) ( - (basic_customer_details::identifier const&) id, - (std::string const&) name - ) - precondition( id_active(id) ) // id active - postcondition( name_for(id) == name ) // name set - ) ; - - private: class agent {}; // Customer agent. - - private: struct customer : basic_customer_details // Basic customer. - { - public: agent managing_agent; // Customer agent. - public: std::string last_contact; // Customer last contacted. - - public: explicit customer ( basic_customer_details const& details ) - : basic_customer_details(details), managing_agent(), - last_contact() - {} - }; - - private: std::map customers_; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/customer_manager_main.cpp b/example/mitchell02/customer_manager_main.cpp deleted file mode 100644 index 64d8b3d..0000000 --- a/example/mitchell02/customer_manager_main.cpp +++ /dev/null @@ -1,26 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_customer_manager_main -// File: customer_manager_main.cpp -#include "customer_manager.hpp" -#include - -int main ( void ) -{ - customer_manager mgr; - basic_customer_details d("id1"); - - mgr.add(d); - mgr.set_name("id1", "abc"); - BOOST_TEST(mgr.name_for("id1") == "abc"); - BOOST_TEST(mgr.count() == 1); - BOOST_TEST(mgr.id_active("id1")); - return boost::report_errors(); -} -//] - diff --git a/example/mitchell02/dictionary.cpp b/example/mitchell02/dictionary.cpp deleted file mode 100644 index bf990a2..0000000 --- a/example/mitchell02/dictionary.cpp +++ /dev/null @@ -1,98 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_dictionary -// File: dictionary.cpp -#include -#include -#include -#include - -CONTRACT_CLASS( // Simple dictionary. - template( typename Key, typename Value ) - class (dictionary) -) { - CONTRACT_CLASS_INVARIANT_TPL( count() >= 0 ) // non-negative count - - // Creation. - - CONTRACT_CONSTRUCTOR_TPL( // Create empty dictionary. - public (dictionary) ( void ) - postcondition( count() == 0 ) // empty - ) {} - - CONTRACT_DESTRUCTOR_TPL( // Destroy dictionary. - public virtual (~dictionary) ( void ) - ) {} - - // Basic queries. - - CONTRACT_FUNCTION_TPL( // Number of key entires. - public int (count) ( void ) const - // postcondition: non-negative count asserted by class invariants - ) { - return items_.size(); - } - - CONTRACT_FUNCTION_TPL( // Has entry for key? - public bool (has) ( (Key const&) key ) const - postcondition( - auto result = return, - if(count() == 0) ( not result ) // empty has no key - ) - ) { - return items_.find(key) != items_.end(); - } - - CONTRACT_FUNCTION_TPL( // Value for given key. - public (Value const&) (value_for) ( (Key const&) key ) const - precondition( has(key) ) // has key - ) { - return items_.find(key)->second; - } - - // Commands. - - CONTRACT_FUNCTION_TPL( // Put value for given key. - public void (put) ( (Key const&) key, (Value const&) value ) - postcondition( - auto old_count = CONTRACT_OLDOF count(), - count() == old_count + 1, // count increased - has(key), // has key - value_for(key) == value // value for key set - ) - ) { - items_.insert(std::make_pair(key, value)); - } - - CONTRACT_FUNCTION_TPL( // Remove value for given key. - public void (remove) ( (Key const&) key ) - precondition( has(key) ) // has key - postcondition( - auto old_count = CONTRACT_OLDOF count(), - count() == old_count - 1, // count decreased - not has(key) // does not have key - ) - ) { - items_.erase(key); - } - - private: std::map items_; -}; - -int main ( void ) -{ - dictionary ages; - BOOST_TEST(not ages.has("john")); - ages.put("john", 23); - BOOST_TEST(ages.value_for("john") == 23); - ages.remove("john"); - BOOST_TEST(ages.count() == 0); - return boost::report_errors(); -} -//] - diff --git a/example/mitchell02/name_list.cpp b/example/mitchell02/name_list.cpp deleted file mode 100644 index 837d3f7..0000000 --- a/example/mitchell02/name_list.cpp +++ /dev/null @@ -1,40 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_name_list -// File: name_list.cpp -#include "name_list.hpp" -#include - -// name_list - -CONTRACT_CONSTRUCTOR_BODY(name_list, name_list) ( void ) {} - -CONTRACT_DESTRUCTOR_BODY(name_list, ~name_list) ( void ) {} - -int name_list::CONTRACT_MEMBER_BODY(count) ( void ) const - { return names_.size(); } - -bool name_list::CONTRACT_MEMBER_BODY(has) ( std::string const& name ) const - { return names_.end() != std::find(names_.begin(), names_.end(), name); } - -void name_list::CONTRACT_MEMBER_BODY(put) ( std::string const& name ) - { names_.push_back(name); } - -// relaxed_name_list - -CONTRACT_CONSTRUCTOR_BODY(relaxed_name_list, relaxed_name_list) ( void ) {} - -CONTRACT_DESTRUCTOR_BODY(relaxed_name_list, ~relaxed_name_list) ( void ) {} - -void relaxed_name_list::CONTRACT_MEMBER_BODY(put) ( std::string const& name ) -{ - // Must use `BODY` to call base functions (to avoid infinite recursion). - if(!has(name)) name_list::CONTRACT_MEMBER_BODY(put)(name); -} -//] - diff --git a/example/mitchell02/name_list.hpp b/example/mitchell02/name_list.hpp deleted file mode 100644 index 5a6e7c2..0000000 --- a/example/mitchell02/name_list.hpp +++ /dev/null @@ -1,99 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_name_list_header -// File: name_list.hpp -#ifndef NAME_LIST_HPP_ -#define NAME_LIST_HPP_ - -#include -#include -#include - -CONTRACT_CLASS( // List of names. - class (name_list) -) { - CONTRACT_CLASS_INVARIANT( count() >= 0 ) // non-negative count - - CONTRACT_CONSTRUCTOR( // Create an empty list. - public (name_list) ( void ) - postcondition( count() == 0 ) // empty list - ) ; // Deferred body definition. - - CONTRACT_DESTRUCTOR( // Destroy list. - public virtual (~name_list) ( void ) - ) ; - - CONTRACT_FUNCTION( // Number of names in list. - public int (count) ( void ) const - // postcondition: non-negative count already in class invariants - ) ; - - CONTRACT_FUNCTION( // Is name in list? - public bool (has) ( (std::string const&) name ) const - postcondition( - auto result = return, - if(count() == 0) ( not result ) // does not have is empty - ) - ) ; - - CONTRACT_FUNCTION( // Add name to list. - public virtual void (put) ( (std::string const&) name ) - precondition( - not has(name) // not already in list - ) - postcondition( - auto old_has_name = CONTRACT_OLDOF has(name), - auto old_count = CONTRACT_OLDOF count(), - // Following if-guard allows to relax subcontracts. - if(not old_has_name) ( - has(name), // name on list - count() == old_count + 1 // number of names increased - ) - ) - ) ; - - private: std::list names_; -}; - -CONTRACT_CLASS( // List of names that allows for duplicates. - class (relaxed_name_list) extends( public name_list ) // Subcontracting. -) { - CONTRACT_CLASS_INVARIANT( void ) // no subcontracted invariants - - // Creation. - - CONTRACT_CONSTRUCTOR( // Create an empty list. - public (relaxed_name_list) ( void ) - postcondition( count() == 0 ) - ) ; - - CONTRACT_DESTRUCTOR( // Destroy list. - public virtual (~relaxed_name_list) ( void ) - ) ; - - // Commands. - - CONTRACT_FUNCTION( // Add name to list. - public void (put) ( (std::string const&) name ) - precondition( // Relax inherited precondition. - has(name) // already in list - ) - postcondition( - auto old_has_name = CONTRACT_OLDOF has(name), - auto old_count = CONTRACT_OLDOF count(), - // Inherited postconditions not checked because of its if-guard. - if(old_has_name) ( - count() == old_count // unchanged if name already in list - ) - ) - ) ; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/name_list_main.cpp b/example/mitchell02/name_list_main.cpp deleted file mode 100644 index b0a14e5..0000000 --- a/example/mitchell02/name_list_main.cpp +++ /dev/null @@ -1,27 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_name_list_main -// File: name_list_main.cpp -#include "name_list.hpp" -#include - -int main ( void ) -{ - relaxed_name_list rl; - rl.put("abc"); - BOOST_TEST(rl.has("abc")); - rl.put("abc"); // Note: Can call `put("abc")` this gain. - - name_list nl; - nl.put("abc"); - BOOST_TEST(nl.has("abc")); - // Note: Cannot call `put("abc")` again. - return boost::report_errors(); -} -//] - diff --git a/example/mitchell02/observer/observer.hpp b/example/mitchell02/observer/observer.hpp deleted file mode 100644 index 634fd05..0000000 --- a/example/mitchell02/observer/observer.hpp +++ /dev/null @@ -1,46 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_observer_header -// File: observer/observer.hpp -#ifndef OBSERVER_HPP_ -#define OBSERVER_HPP_ - -#include - -CONTRACT_CLASS( // Observer. - class (observer) -) { - CONTRACT_CLASS_INVARIANT( void ) // no invariant - - friend class subject; - - // Creation. - - CONTRACT_CONSTRUCTOR( // Create observer. - public (observer) ( void ) - ) {} - - CONTRACT_DESTRUCTOR( // Destroy observer. - public virtual (~observer) ( void ) - ) {} - - // Commands. - - CONTRACT_FUNCTION( // If up to date with its subject. - protected virtual bool (up_to_date_with_subject) ( void ) const new - ) = 0; - - CONTRACT_FUNCTION( // Update and inform its subject. - protected virtual void (update) ( void ) new - postcondition( up_to_date_with_subject() ) // up-to-date - ) = 0; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/observer/subject.hpp b/example/mitchell02/observer/subject.hpp deleted file mode 100644 index 0222610..0000000 --- a/example/mitchell02/observer/subject.hpp +++ /dev/null @@ -1,151 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_subject_header -// File: observer/subject.hpp -#ifndef SUBJECT_HPP_ -#define SUBJECT_HPP_ - -#include "observer.hpp" -#include -#include -#include - -// Assertion requirements used to model assertion computational complexity. -#define O_1 0 // O(1) constant (default) -#define O_N 1 // O(n) linear -#define COMPLEXITY_MAX O_1 - -CONTRACT_CLASS( // Subject for observer design pattern. - class (subject) -) { - CONTRACT_CLASS_INVARIANT( - all_observers_valid(observers()), // observes valid - requires O_N <= COMPLEXITY_MAX - ) - - // Creation. - - CONTRACT_CONSTRUCTOR( // Construct subject with no observer. - public (subject) ( void ) - ) {} - - CONTRACT_DESTRUCTOR( // Destroy subject. - public virtual (~subject) ( void ) - ) {} - - // Queries. - - CONTRACT_FUNCTION( // If given observer is attached. - public bool (attached) ( (observer const* const) obs ) const - precondition( obs ) // not null - ) { - return std::find(observers_.begin(), observers_.end(), obs) != - observers_.end(); - } - - // Commands. - - CONTRACT_FUNCTION( // Remember given object as an observer. - public void (attach) ( (observer* const) obs ) - precondition( - obs, // not null - not attached(obs) // not already attached - ) - postcondition( - auto old_observers = CONTRACT_OLDOF observers(), - attached(obs), // attached - other_observers_unchanged(old_observers, observers(), obs), - // others not changed (frame rule) - requires O_N <= COMPLEXITY_MAX - ) - ) { - observers_.push_back(obs); - } - - // Queries. - - CONTRACT_FUNCTION( // All observers attached to this subject. - protected (std::list) (observers) ( void ) const - ) { - // Create list of pointers to const observers. - std::list obs; - for(std::list::const_iterator - i = observers_.begin(); i != observers_.end(); ++i) { - obs.push_back(*i); - } - return obs; - } - - // Commands. - - CONTRACT_FUNCTION( // Update all attached observers. - protected void (notify) ( void ) - postcondition( all_observers_updated(observers()) ) // all updated - ) { - for(std::list::iterator - i = observers_.begin(); i != observers_.end(); ++i) { - // Class invariant ensures no null pointers in observers but - // class invariants not checked for non-public members so check. - CONTRACT_BLOCK_INVARIANT( const( i ) 0 != *i ) // pointer not null - (*i)->update(); - } - } - - // Contract helpers. - - CONTRACT_FUNCTION( - private static bool (all_observers_valid) ( - (std::list const&) observers ) - ) { - for(std::list::const_iterator - i = observers.begin(); i != observers.end(); ++i) { - if(!(*i)) return false; - } - return true; - } - - CONTRACT_FUNCTION( - private bool (other_observers_unchanged) ( - (std::list const&) old, - (std::list const&) now, - (observer const*) obs - ) const - precondition( obs ) // not null - ) { - std::list remaining = now; - std::remove(remaining.begin(), remaining.end(), obs); - - std::list::const_iterator - remaining_it = remaining.begin(); - std::list::const_iterator old_it = old.begin(); - while(remaining.end() != remaining_it && old.end() != old_it) { - if(*remaining_it != *old_it) return false; - ++remaining_it; - ++old_it; - } - return true; - } - - CONTRACT_FUNCTION( - private bool (all_observers_updated) ( - (std::list const&) observers ) const - ) { - for(std::list::const_iterator - i = observers.begin(); i != observers.end(); ++i) { - if(!(*i)) return false; - if(!(*i)->up_to_date_with_subject()) return false; - } - return true; - } - - private: std::list observers_; -}; - -#endif // #include guard -//] - diff --git a/example/mitchell02/observer_main.cpp b/example/mitchell02/observer_main.cpp deleted file mode 100644 index 024b482..0000000 --- a/example/mitchell02/observer_main.cpp +++ /dev/null @@ -1,74 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_observer_main -// File: observer_main.cpp -#include "observer/observer.hpp" -#include "observer/subject.hpp" -#include -#include - -int state_check; // For unit testing. - -class concrete_subject : public subject // Implement an actual subject. -{ - public: typedef int state; // Some state being observed. - - public: concrete_subject ( void ) : state_() {} - - public: void set_state (state const& the_state) { - state_ = the_state; - BOOST_TEST(state_ == state_check); - notify(); // Notify observers. - } - - public: state get_state ( void ) const { return state_; } - - private: state state_; -}; - -CONTRACT_CLASS( // Implement of actual observer. - class (concrete_observer) extends( public observer ) -) { - CONTRACT_CLASS_INVARIANT( void ) - - CONTRACT_CONSTRUCTOR( // Create concrete observer. - public explicit (concrete_observer) ( - (concrete_subject const&) the_subject ) - initialize( subject_(the_subject), observed_state_() ) - ) {} - - // Implement base virtual functions. - - CONTRACT_FUNCTION( - private bool (up_to_date_with_subject) ( void ) const override final - ) { - return true; // For simplicity, always up-to-date. - } - - CONTRACT_FUNCTION( - private void (update) ( void ) override final - ) { - observed_state_ = subject_.get_state(); - BOOST_TEST(observed_state_ == state_check); - } - - private: concrete_subject const& subject_; - private: concrete_subject::state observed_state_; -}; - -int main ( void ) -{ - concrete_subject sbj; - concrete_observer ob(sbj); - sbj.attach(&ob); - sbj.set_state(state_check = 123); - sbj.set_state(state_check = 456); - return boost::report_errors(); -} -//] - diff --git a/example/mitchell02/simple_queue.cpp b/example/mitchell02/simple_queue.cpp deleted file mode 100644 index 67bddee..0000000 --- a/example/mitchell02/simple_queue.cpp +++ /dev/null @@ -1,170 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_simple_queue -// File: simple_queue.cpp -#include -#include -#include - -// Assertion requirements used to model assertion computational complexity. -#define O_1 0 // O(1) constant (default) -#define O_N 1 // O(n) linear -#define COMPLEXITY_MAX O_1 - -CONTRACT_CLASS( - template( typename T ) - class (simple_queue) -) { - CONTRACT_CLASS_INVARIANT( count() >= 0 ) // non-negative count - - // Creation. - - CONTRACT_CONSTRUCTOR_TPL( // Create empty queue. - public explicit (simple_queue) ( int const the_capacity ) - precondition( the_capacity > 0 ) // positive capacity - postcondition( - capacity() == the_capacity, // capacity set - is_empty() // empty - ) - ) { - items_.reserve(the_capacity); - } - - CONTRACT_DESTRUCTOR_TPL( // Destroy queue. - public virtual (~simple_queue) ( void ) - ) {} - - // Basic queries. - - CONTRACT_FUNCTION_TPL( // Items in the queue (in their order). - public (std::vector const&) (items) ( void ) const - ) { - return items_; - } - - CONTRACT_FUNCTION_TPL( // Max number of items queue can hold. - public int (capacity) ( void ) const - ) { - return items_.capacity(); - } - - // Derived queries. - - CONTRACT_FUNCTION_TPL( // Number of items. - public int (count) ( void ) const - postcondition( - auto result = return, - result == int(items().size()) // return items count - ) - ) { - return items_.size(); - } - - CONTRACT_FUNCTION_TPL( // Item at head. - public (T const&) (head) ( void ) const - precondition( not is_empty() ) - postcondition( - auto result = return, - result == items().at(0) // return item on top - ) - ) { - return items_.at(0); - } - - CONTRACT_FUNCTION_TPL( // If queue contains no item. - public bool (is_empty) ( void ) const - postcondition( - auto result = return, - result == (count() == 0) // consistent with count - ) - ) { - return items_.size() == 0; - } - - CONTRACT_FUNCTION_TPL( // If queue has no room for another item. - public bool (is_full) ( void ) const - postcondition( - auto result = return, - // consistent with size and capacity - result == (capacity() == int(items().size())) - ) - ) { - return items_.size() == items_.capacity(); - } - - // Commands. - - CONTRACT_FUNCTION_TPL( // Remove head item and shift all other items. - public void (remove) ( void ) - precondition( not is_empty() ) - postcondition( - auto old_count = CONTRACT_OLDOF count(), - auto old_items = CONTRACT_OLDOF items(), - count() == old_count - 1, // count decreased - // Expensive assertion to check so marked with its complexity. - all_equal(items(), old_items, 1 /* shifted */), - requires O_N <= COMPLEXITY_MAX - ) - ) { - items_.erase(items_.begin()); - } - - CONTRACT_FUNCTION_TPL( // Add item to tail. - public void (put) ( (T const&) item ) - precondition( count() < capacity() ) - postcondition( - auto old_count = CONTRACT_OLDOF count(), - auto old_items = CONTRACT_OLDOF items(), - count() == old_count + 1, // count increased - items().at(count() - 1) == item, // second last item - if(count() >= 2) ( - // Computationally expensive assertion to check. - all_equal(items(), old_items), - requires O_N <= COMPLEXITY_MAX - ) - ) - ) { - items_.push_back(item); - } - - CONTRACT_FUNCTION_TPL( // Contract helper. - private static bool (all_equal) ( - (std::vector const&) left, - (std::vector const&) right, - size_t offset, default 0 - ) - precondition( - right.size() == left.size() + offset // correct offset - ) - ) { - for(size_t i = offset; i < right.size(); ++i) - if(left.at(i - offset) != right.at(i)) return false; - return true; - } - - private: std::vector items_; -}; - -int main ( void ) -{ - simple_queue q(10); - q.put(123); - q.put(456); - std::vector const& items = q.items(); - BOOST_TEST(items[0] == 123); - BOOST_TEST(items[1] == 456); - BOOST_TEST(q.capacity() == 10); - BOOST_TEST(q.head() == 123); - BOOST_TEST(not q.is_empty()); - BOOST_TEST(not q.is_full()); - q.remove(); - BOOST_TEST(q.count() == 1); - return boost::report_errors(); -} -//] - diff --git a/example/mitchell02/stack.cpp b/example/mitchell02/stack.cpp deleted file mode 100644 index 82e20b8..0000000 --- a/example/mitchell02/stack.cpp +++ /dev/null @@ -1,110 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[mitchell02_stack -// File: stack.cpp -#include -#include -#include - -CONTRACT_CLASS( // Simple stack. - template( typename T ) - class (stack) -) { - CONTRACT_CLASS_INVARIANT_TPL( count() >= 0 ) // non-negative count - - // Creation. - - CONTRACT_CONSTRUCTOR_TPL( // Create empty stack. - public (stack) ( void ) - postcondition( count() == 0 ) // empty - ) {} - - CONTRACT_DESTRUCTOR_TPL( // Destroy stack. - public virtual (~stack) ( void ) - ) {} - - // Basic queries. - - CONTRACT_FUNCTION_TPL( // Number of items. - public int (count) ( void ) const - ) { - return items_.size(); - } - - CONTRACT_FUNCTION_TPL( // Item at index in [1, count()] (as in Eiffel). - public (T const&) (item_at) ( int const index ) const - precondition( - index > 0, // positive index - index <= count() // index within count - ) - ) { - return items_.at(index - 1); - } - - // Derived queries. - - CONTRACT_FUNCTION_TPL( // If no items. - public bool (is_empty) ( void ) const - postcondition( - auto result = return, - result == (count() == 0) // consistent with count - ) - ) { - return count() == 0; - } - - CONTRACT_FUNCTION_TPL( // Top item. - public (T const&) (item) ( void ) const - precondition( count() > 0 ) // not empty - postcondition( - auto result = return, - result == item_at(count()) // item on top - ) - ) { - return item_at(count()); - } - - // Commands. - - CONTRACT_FUNCTION_TPL( // Push item to the top. - public void (put) ( (T const&) new_item ) - postcondition( - auto old_count = CONTRACT_OLDOF count(), - count() == old_count + 1, // count increased - item() == new_item // item set - ) - ) { - items_.push_back(new_item); - } - - CONTRACT_FUNCTION_TPL( // Pop top item. - public void (remove) ( void ) - precondition( count() > 0 ) // not empty - postcondition( - auto old_count = CONTRACT_OLDOF count(), - count() == old_count - 1 // count decreased - ) - ) { - items_.resize(items_.size() - 1); - } - - private: std::vector items_; -}; - -int main ( void ) -{ - stack s; - BOOST_TEST(s.count() == 0); - s.put(123); - BOOST_TEST(s.item_at(1) == 123); - s.remove(); - BOOST_TEST(s.is_empty()); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/block_invariant.cpp b/example/n1962/block_invariant.cpp deleted file mode 100644 index 4e5ee67..0000000 --- a/example/n1962/block_invariant.cpp +++ /dev/null @@ -1,25 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_block_invariant -// File: block_invariant.cpp -#include -#include -#include - -int main ( void ) -{ - int i = 0; - for(i = 0; i < 100; ++i) - { - CONTRACT_BLOCK_INVARIANT( const( i ) i >= 0 ) - } - BOOST_TEST(i == 100); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/circle.cpp b/example/n1962/circle.cpp deleted file mode 100644 index ee50f2e..0000000 --- a/example/n1962/circle.cpp +++ /dev/null @@ -1,57 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_circle -// File: circle.cpp -#include -#include - -CONTRACT_CLASS( - class (shape) -) { - CONTRACT_CLASS_INVARIANT( void ) // Must always specify class invariants. - - CONTRACT_DESTRUCTOR( - public virtual (~shape) ( void ) - ) {} - - CONTRACT_FUNCTION( - public virtual int (compute_area) ( void ) const - // No base preconditions so all derived preconditions true. - postcondition( auto result = return, result > 0 ) - ) = 0; // Contract for pure virtual function. -}; - -CONTRACT_CLASS( - class (circle) extends( public shape ) // Subcontract from base `shape`. -) { - CONTRACT_CLASS_INVARIANT( void ) // In AND with base class invariants. - - public: int radius() const { return 2; } - - CONTRACT_FUNCTION( // Also using `override` specifier (optional). - public virtual int (compute_area) ( void ) const override - // Eventual preconditions in OR with base function preconditions. - postcondition( // In AND with base function postconditions. - auto result = return, - result == pi * radius() * radius() - ) - ) { - return pi * radius() * radius(); - } - - private: static const int pi = 3; // Truncated from 3.14... -}; - -int main ( void ) -{ - circle c; - BOOST_TEST(c.compute_area() == 12); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/equal.hpp b/example/n1962/equal.hpp deleted file mode 100644 index 3472948..0000000 --- a/example/n1962/equal.hpp +++ /dev/null @@ -1,29 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_equal_header -// File: equal.hpp -#ifndef EQUAL_HPP_ -#define EQUAL_HPP_ - -#include "equal_not.hpp" -#include - -CONTRACT_FUNCTION_TPL( - template( typename T ) - bool operator(==)(equal) ( (T const&) left, (T const&) right ) - postcondition( - auto result = return, - result == !(left != right) - ) -) { - return left.value == right.value; -} - -#endif // #include guard -//] - diff --git a/example/n1962/equal_main.cpp b/example/n1962/equal_main.cpp deleted file mode 100644 index 83ed3d9..0000000 --- a/example/n1962/equal_main.cpp +++ /dev/null @@ -1,26 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_equal_main -// File: equal_main.cpp -#include "equal.hpp" -#include "equal_not.hpp" -#include - -struct number { int value; }; - -int main ( void ) -{ - number n; - n.value = 123; - - BOOST_TEST((n == n) == true); - BOOST_TEST((n != n) == false); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/equal_not.hpp b/example/n1962/equal_not.hpp deleted file mode 100644 index 564e645..0000000 --- a/example/n1962/equal_not.hpp +++ /dev/null @@ -1,29 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_equal_not_header -// File: equal_not.hpp -#ifndef EQUAL_NOT_HPP_ -#define EQUAL_NOT_HPP_ - -#include "equal.hpp" -#include - -CONTRACT_FUNCTION_TPL( - template( typename T ) - bool operator(!=)(not_equal) ( (T const&) left, (T const&) right ) - postcondition( - auto result = return, - result == !(left == right) - ) -) { - return left.value != right.value; -} - -#endif // #include guard -//] - diff --git a/example/n1962/factorial.cpp b/example/n1962/factorial.cpp deleted file mode 100644 index 0ba99de..0000000 --- a/example/n1962/factorial.cpp +++ /dev/null @@ -1,56 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_factorial -// File: factorial.cpp -#include -#include - -// Assertion requirements used to model assertion computational complexity. -#define O_1 0 // O(1) constant (default). -#define O_N 1 // O(n) linear. -#define O_NN 2 // O(n * n) quadratic. -#define O_NX 3 // O(n^x) polynomial. -#define O_FACTN 4 // O(n!) factorial. -#define O_EXPN 5 // O(e^n) exponential. -#define O_ALL 10 -#define COMPLEXITY_MAX O_ALL - -CONTRACT_FUNCTION( - int (factorial) ( int n ) - precondition( - n >= 0, // Non-negative natural number. - n <= 12 // Max function input. - ) - postcondition( - auto result = return, - result >= 1, - if(n < 2) ( // Select assertion. - result == 1 - ) else ( - // Assertions automatically disabled within other assertions. - // Therefore, this postcondition can recursively call the - // function without causing infinite recursion. - result == n * factorial(n - 1), - // This assertion introduces significant run-time - // overhead (same as the function body) so assertion - // requirements are used to selectively disable it. - requires O_FACTN <= COMPLEXITY_MAX - ) - ) -) { - if(n < 2) return 1; - else return n * factorial(n - 1); -} - -int main ( void ) -{ - BOOST_TEST(factorial(4) == 24); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/sqrt.cpp b/example/n1962/sqrt.cpp deleted file mode 100644 index 05df517..0000000 --- a/example/n1962/sqrt.cpp +++ /dev/null @@ -1,31 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_sqrt -// File: sqrt.cpp -#include -#include -#include - -CONTRACT_FUNCTION( // Default value for `precision` parameter. - double (mysqrt) ( double x, double precision, default(1e-6) ) - precondition( x >= 0.0 ) - postcondition( - auto root = return, // Result value named `root`. - fabs(root * root - x) <= precision // Equal within precision. - ) -) { - return sqrt(x); -} - -int main ( void ) -{ - BOOST_TEST(fabs(mysqrt(4.0) - 2.0) <= 1e-6); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/sqrt.d b/example/n1962/sqrt.d deleted file mode 100644 index 0dba6d5..0000000 --- a/example/n1962/sqrt.d +++ /dev/null @@ -1,31 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Use, modification, and distribution is subject to the -// Boost Software License, Version 1.0 (see accompanying file -// LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt). -// Documentation at http://contractpp.sourceforge.net. - -//[n1962_sqrt_d -// File: sqrt.d -// Extra spaces, newlines, etc used to align text with this library code. - - - - -real mysqrt ( real x ) // No default parameters in D. - in { assert(x >= 0); } - out(root) { - - assert(std.math.fabs(root * root - x) <= 1e6); - } -body { - return std.math.sqrt(x); -} - - - - - - -//] - diff --git a/example/n1962/sum.cpp b/example/n1962/sum.cpp deleted file mode 100644 index 476ca62..0000000 --- a/example/n1962/sum.cpp +++ /dev/null @@ -1,18 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_sum -// File: sum.cpp -#include "sum.hpp" - -int CONTRACT_FREE_BODY(sum) ( int count, int* array ) { - int total = 0; - for(int i = 0; i < count; ++i) total += array[i]; - return total; -} -//] - diff --git a/example/n1962/sum.hpp b/example/n1962/sum.hpp deleted file mode 100644 index d0dd36e..0000000 --- a/example/n1962/sum.hpp +++ /dev/null @@ -1,22 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_sum_header -// File: sum.hpp -#ifndef SUM_HPP_ -#define SUM_HPP_ - -#include - -CONTRACT_FUNCTION( - int (sum)( int count, (int*) array ) - precondition( count % 4 == 0 ) -) ; // Separate body definition from function declaration (see ".cpp" file). - -#endif // #include guard -//] - diff --git a/example/n1962/sum_main.cpp b/example/n1962/sum_main.cpp deleted file mode 100644 index 6a8ae90..0000000 --- a/example/n1962/sum_main.cpp +++ /dev/null @@ -1,20 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_sum_main -// File: sum_main.cpp -#include "sum.hpp" -#include - -int main ( void ) -{ - int a[8] = {1, 1, 1, 1, 1, 1, 1, 1}; - BOOST_TEST(sum(8, a) == 8); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/vector.cpp b/example/n1962/vector.cpp deleted file mode 100644 index 87b1f76..0000000 --- a/example/n1962/vector.cpp +++ /dev/null @@ -1,39 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_vector_main -// File: vector.cpp -#include "vector.hpp" -#include - -int main ( void ) -{ - // Run a few of the operations (could test more of them...). - vector v(3); - BOOST_TEST(v.size() == 3); - BOOST_TEST(boost::algorithm::all_of_equal(v, '\0')); - const vector& cv = v; // A reference so no copy. - - vector w(v); - BOOST_TEST(w == v); - - vector::iterator b = v.begin(); - BOOST_TEST(*b == '\0'); - - vector::const_iterator cb = cv.begin(); - BOOST_TEST(*cb == '\0'); - - v.insert(b, 2, 'a'); - BOOST_TEST(v[0] == 'a'); - BOOST_TEST(v[1] == 'a'); - - v.push_back('b'); - BOOST_TEST(v.back() == 'b'); - return boost::report_errors(); -} -//] - diff --git a/example/n1962/vector.hpp b/example/n1962/vector.hpp deleted file mode 100644 index e29b0b4..0000000 --- a/example/n1962/vector.hpp +++ /dev/null @@ -1,499 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_vector -// File: vector.hpp -#include -#include -#include -#include -#include -#include -#include - -CONTRACT_CLASS( // Vector wrapper with contracts. - template( class T, class Allocator, default std::allocator ) - class (vector) // No base classes so no subcontracting for this example. -) { - CONTRACT_CLASS_INVARIANT_TPL( // At very beginning of the class declaration. - empty() == (size() == 0), - std::distance(begin(), end()) == int(size()), - std::distance(rbegin(), rend()) == int(size()), - size() <= capacity(), - capacity() <= max_size() - ) // No static or volatile class invariants for this example. - - public: typedef typename std::vector::allocator_type - allocator_type; - public: typedef typename std::vector::pointer pointer; - public: typedef typename std::vector::const_pointer - const_pointer; - public: typedef typename std::vector::reference reference; - public: typedef typename std::vector::const_reference - const_reference; - public: typedef typename std::vector::value_type value_type; - public: typedef typename std::vector::iterator iterator; - public: typedef typename std::vector::const_iterator - const_iterator; - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::difference_type - difference_type; - public: typedef typename std::vector::reverse_iterator - reverse_iterator; - public: typedef typename std::vector::const_reverse_iterator - const_reverse_iterator; - - CONTRACT_CONSTRUCTOR_TPL( - public (vector) ( void ) // Always specify access level `public`, etc. - postcondition( not empty() ) - initialize( vector_() ) // Member initializers. - ) {} - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (vector) ( (const Allocator&) allocator ) - postcondition( - empty(), - allocator == get_allocator() - ) - initialize( vector_(allocator) ) - ) {} - - CONTRACT_CONSTRUCTOR_TPL( - public explicit (vector) ( (size_type) count ) - postcondition( - size() == count, - boost::algorithm::all_of_equal(begin(), end(), T()), - requires boost::has_equal_to::value // Requirements. - ) - initialize( vector_(count) ) - ) {} - - CONTRACT_CONSTRUCTOR_TPL( - public (vector) ( (size_type) count, (const T&) value ) - postcondition( - size() == count, - boost::algorithm::all_of_equal(begin(), end(), value), - requires boost::has_equal_to::value - ) - initialize( vector_(count, value) ) - ) {} - - CONTRACT_CONSTRUCTOR_TPL( - public (vector) ( (size_type) count, (const T&) value, - (const Allocator&) allocator ) - postcondition( - size() == count, - boost::algorithm::all_of_equal(begin(), end(), value), - requires boost::has_equal_to::value, - allocator == get_allocator() - ) - initialize( vector_(count, value, allocator) ) - ) {} - - CONTRACT_CONSTRUCTOR_TPL( // Contract with concepts. - public template( class Iterator ) - requires( boost::InputIterator ) - (vector) ( (Iterator) first, (Iterator) last ) - postcondition( std::distance(first, last) == int(size()) ) - initialize( vector_(first, last) ) - ) {} - - CONTRACT_CONSTRUCTOR_TPL( - public template( class Iterator ) - requires( boost::InputIterator ) - (vector) ( (Iterator) first, (Iterator) last, - (const Allocator&) allocator ) - postcondition( - std::distance(first, last) == int(size()), - allocator == get_allocator() - ) - initialize( vector_(first, last, allocator) ) - ) {} - - CONTRACT_CONSTRUCTOR_TPL( - public (vector) ( (const vector&) right ) - postcondition( - right == *this, requires boost::has_equal_to::value - ) - initialize( vector_(right.vector_) ) - ) {} - - CONTRACT_FUNCTION_TPL( // Operator symbol and (arbitrary) name `copy`. - public (vector&) operator(=)(copy) ( (const vector&) right ) - postcondition( - auto result = return, // Return value. - result == *this, requires boost::has_equal_to::value, - result == right, requires boost::has_equal_to::value - ) - ) { - return vector_ = right.vector_; - } - - CONTRACT_DESTRUCTOR_TPL( // Destruct contract (check class invariant). - public virtual (~vector) ( void ) - ) {} - - CONTRACT_FUNCTION_TPL( - // Wrapping parenthesis optional for keyword types `void`, `bool`, etc. - public void (reserve) ( (size_type) count ) - precondition( count < max_size() ) - postcondition( capacity() >= count ) - ) { - vector_.reserve(count); - } - - CONTRACT_FUNCTION_TPL( - public (size_type) (capacity) ( void ) const // Constant member. - postcondition( auto result = return, result >= size() ) - ) { - return vector_.capacity(); - } - - CONTRACT_FUNCTION_TPL( - public (iterator) (begin) ( void ) - postcondition( - auto result = return, - if(empty()) ( // Select assertions `if(...) ( ...)`. - result == end() - ) // Omitted optional `else( ... )`. - ) - ) { - return vector_.begin(); - } - - CONTRACT_FUNCTION_TPL( // Contract overloaded function (see above). - public (const_iterator) (begin) ( void ) const - postcondition( - auto result = return, - if(empty()) ( result == end() ) - ) - ) { - return vector_.begin(); - } - - CONTRACT_FUNCTION_TPL( // Contract with no pre/post checks class invariants. - public (iterator) (end) ( void ) - ) { - return vector_.end(); - } - - CONTRACT_FUNCTION_TPL( - public (const_iterator) (end) ( void ) const - ) { - return vector_.end(); - } - - CONTRACT_FUNCTION_TPL( - public (reverse_iterator) (rbegin) ( void ) - postcondition( - auto result = return, - if(empty()) ( result == rend() ) - ) - ) { - return vector_.rbegin(); - } - - CONTRACT_FUNCTION_TPL( - public (const_reverse_iterator) (rbegin) ( void ) const - postcondition( - auto result = return, - if(empty()) ( result == rend() ) - ) - ) { - return vector_.rbegin(); - } - - CONTRACT_FUNCTION_TPL( - public (reverse_iterator) (rend) ( void ) - ) { - return vector_.rend(); - } - - CONTRACT_FUNCTION_TPL( - public (const_reverse_iterator) (rend) ( void ) const - ) { - return vector_.rend(); - } - - CONTRACT_FUNCTION_TPL( - public void (resize) ( (size_type) count ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), // Old value (at entry). - size() == count, - if(count > old_size) ( - boost::algorithm::all_of_equal(begin() + old_size, end(), - T()), requires boost::has_equal_to::value - ) - ) - ) { - vector_.resize(count); - } - - CONTRACT_FUNCTION_TPL( - public void (resize) ( (size_type) count, (T) value ) - postcondition( - (size_type) old_size = CONTRACT_OLDOF size(), // With old type. - size() == count, - count > old_size ? // Ternary operator. - boost::algorithm::all_of_equal(begin() + old_size, end(), - value) - : - true - , requires boost::has_equal_to::value - ) - ) { - vector_.resize(count, value); - } - - CONTRACT_FUNCTION_TPL( - public (size_type) (size) ( void ) const - postcondition( auto result = return, result <= capacity() ) - ) { - return vector_.size(); - } - - CONTRACT_FUNCTION_TPL( - public (size_type) (max_size) ( void ) const - postcondition( auto result = return, result >= capacity() ) - ) { - return vector_.max_size(); - } - - CONTRACT_FUNCTION_TPL( - public bool (empty) ( void ) const - postcondition( - auto result = return, - result == (size() == 0) - ) - ) { - return vector_.empty(); - } - - CONTRACT_FUNCTION_TPL( - public (Allocator) (get_allocator) ( void ) const - ) { - return vector_.get_allocator(); - } - - CONTRACT_FUNCTION_TPL( - public (reference) (at) ( (size_type) index ) - precondition( index < size() ) - ) { - return vector_.at(index); - } - - CONTRACT_FUNCTION_TPL( - public (const_reference) (at) ( (size_type) index ) const - precondition( index < size() ) - ) { - return vector_.at(index); - } - - CONTRACT_FUNCTION_TPL( - public (reference) operator([])(at) ( (size_type) index ) - precondition( index < size() ) - ) { - return vector_[index]; - } - - CONTRACT_FUNCTION_TPL( - public (const_reference) operator([])(at) ( (size_type) index ) const - precondition( index < size() ) - ) { - return vector_[index]; - } - - CONTRACT_FUNCTION_TPL( - public (reference) (front) ( void ) - precondition( not empty() ) // `not` instead of symbol `!`. - ) { - return vector_.front(); - } - - CONTRACT_FUNCTION_TPL( - public (const_reference) (front) ( void ) const - precondition( bool(!empty()) ) // Or, `bool` to wrap symbol `!`. - ) { - return vector_.front(); - } - - CONTRACT_FUNCTION_TPL( - public (reference) (back) ( void ) - precondition( not empty() ) - ) { - return vector_.back(); - } - - CONTRACT_FUNCTION_TPL( - public (const_reference) (back) ( void ) const - precondition( not empty() ) - ) { - return vector_.back(); - } - - CONTRACT_FUNCTION_TPL( - public void (push_back) ( (const T&) value ) - precondition( size() < max_size() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - auto old_capacity = CONTRACT_OLDOF capacity(), - back() == value, requires boost::has_equal_to::value, - size() == old_size + 1, - capacity() >= old_capacity - ) - ) { - vector_.push_back(value); - } - - CONTRACT_FUNCTION_TPL( - public void (pop_back) ( void ) - precondition( not empty() ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - size() == old_size - 1 - ) - ) { - vector_.pop_back(); - } - - CONTRACT_FUNCTION_TPL( - public template( class Iterator ) - requires( boost::InputIterator ) - void (assign) ( (Iterator) first, (Iterator) last ) - // precondition: [begin(), end()) does not contain [first, last) - postcondition( std::distance(first, last) == int(size()) ) - ) { - vector_.assign(first, last); - } - - CONTRACT_FUNCTION_TPL( - public void (assign) ( (size_type) count, (const T&) value ) - precondition( count <= max_size() ) - postcondition( - boost::algorithm::all_of_equal(begin(), end(), value), - requires boost::has_equal_to::value - ) - ) { - vector_.assign(count, value); - } - - CONTRACT_FUNCTION_TPL( - public (iterator) (insert) ( (iterator) where, (const T&) value ) - precondition( size() < max_size() ) - postcondition( - auto result = return, - auto old_size = CONTRACT_OLDOF size(), - value == *result, requires boost::has_equal_to::value, - size() == old_size + 1 - // if(capacity() > oldof capacity()) - // [begin(), end()) is invalid - // else - // [where, end()) is invalid - ) - ) { - return vector_.insert(where, value); - } - - CONTRACT_FUNCTION_TPL( - public void (insert) ( (iterator) where, (size_type) count, - (const T&) value ) - precondition( size() + count < max_size() ) - postcondition( - using boost::prior, - auto old_size = CONTRACT_OLDOF size(), - auto old_capacity = CONTRACT_OLDOF capacity(), - auto old_where = CONTRACT_OLDOF where, - size() == old_size + count, - capacity() >= old_capacity, - if(capacity() == old_capacity) ( - boost::algorithm::all_of_equal(prior(old_where), - prior(old_where) + count, value), - requires boost::has_equal_to::value - // [where, end()) is invalid - ) // else [begin(), end()) is invalid - ) - ) { - vector_.insert(where, count, value); - } - - CONTRACT_FUNCTION_TPL( - public template( class Iterator ) - requires( boost::InputIterator ) - void (insert) ( (iterator) where, (Iterator) first, (Iterator) last ) - precondition( - // [first, last) is not contained in [begin(), end()) - size() + std::distance(first, last) < max_size() - ) - postcondition( - auto old_size = CONTRACT_OLDOF size(), - auto old_capacity = CONTRACT_OLDOF capacity(), - size() == old_size + std::distance(first, last), - capacity() >= old_capacity - ) - ) { - vector_.insert(where, first, last); - } - - CONTRACT_FUNCTION_TPL( - public (iterator) (erase) ( (iterator) where ) - precondition( - not empty(), - where != end() - ) - postcondition( - auto result = return, - auto old_size = CONTRACT_OLDOF size(), - size() == old_size - 1, - if(empty()) ( result == end() ) - // [where, end()) is invalid - ) - ) { - return vector_.erase(where); - } - - CONTRACT_FUNCTION_TPL( - public (iterator) (erase) ( (iterator) first, (iterator) last ) - precondition( size() >= std::distance(first, last) ) - postcondition( - auto result = return, - auto old_size = CONTRACT_OLDOF size(), - size() == old_size - std::distance(first, last), - if(empty()) ( result == end() ) - // [first, last) is invalid - ) - ) { - return vector_.erase(first, last); - } - - CONTRACT_FUNCTION_TPL( - public void (clear) ( void ) - postcondition( empty() ) - ) { - vector_.clear(); - } - - CONTRACT_FUNCTION_TPL( - public void (swap) ( (vector&) right ) - postcondition( - auto old_self = CONTRACT_OLDOF *this, - auto old_right = CONTRACT_OLDOF right, - right == old_self, requires boost::has_equal_to::value, - old_right == *this, requires boost::has_equal_to::value - ) - ) { - vector_.swap(right); - } - - friend bool operator== ( vector const& left, vector const& right ) - { - return left.vector_ == right.vector_; - } - - private: std::vector vector_; -}; -//] - diff --git a/example/n1962/vector_npaper.hpp b/example/n1962/vector_npaper.hpp deleted file mode 100644 index 287df85..0000000 --- a/example/n1962/vector_npaper.hpp +++ /dev/null @@ -1,499 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n1962_vector_npaper -// File: vector_npaper.cpp -// Extra spaces, newlines, etc used to align text with this library code. - -#include -#include -#include -#include -#include - - -template< class T, class Allocator = std::allocator > -class vector -{ - invariant { - empty() == (size() == 0); - std::distance(begin(), end()) == int(size()); - std::distance(rbegin(), rend()) == int(size()); - size() <= capacity(); - capacity() <= max_size(); - } - - public: typedef typename std::vector::allocator_type - allocator_type; - public: typedef typename std::vector::pointer pointer; - public: typedef typename std::vector::const_pointer - const_pointer; - public: typedef typename std::vector::reference reference; - public: typedef typename std::vector::const_reference - const_reference; - public: typedef typename std::vector::value_type value_type; - public: typedef typename std::vector::iterator iterator; - public: typedef typename std::vector::const_iterator - const_iterator; - public: typedef typename std::vector::size_type size_type; - public: typedef typename std::vector::difference_type - difference_type; - public: typedef typename std::vector::reverse_iterator - reverse_iterator; - public: typedef typename std::vector::const_reverse_iterator - const_reverse_iterator; - - - public: vector ( void ) - postcondition { not empty(); } - : vector_() - {} - - - public: explicit vector ( const Allocator& alllocator ) - postcondition { - empty(); - allocator == get_allocator(); - } - : vector_(allocator) - {} - - - public: explicit vector ( size_type count ) - postcondition { - size() == count; - boost::algorithm::all_of_equal(begin(), end(), T()); - // Assertion requirements not supported by [N1962]. - } - : vector_(count) - {} - - - public: vector ( size_type count, const T& value ) - postcondition { - size() == count; - boost::algorithm::all_of_equal(begin(), end(), value); - - } - : vector_(count, value) - {} - - - public: vector ( size_type count, const T& value, - const Allocator& allocator ) - postcondition { - size() == count; - boost::algorithm::all_of_equal(begin(), end(), value); - - allocator == get_allocator(); - } - : vector_(count, value, allocator) - {} - - - public: template< class Iterator > - requires std::InputIterator - vector ( Iterator first, Iterator last ) - postcondition { std::distance(first, last) == int(size()); } - : vector_(first, last) - {} - - - public: template< class Iterator > - requires std::InputIterator - vector ( Iterator first, Iterator last, - const Allocator& allocator ) - postcondition { - std::distance(first, last) == int(size()); - allocator == get_allocator(); - } - : vector_(first, last, allocator) - {} - - - public: vector ( const vector& right ) - postcondition { - right == *this; - } - : vector_(right.vector_) - {} - - - public: vector& operator= ( const vector& right ) - postcondition(result) { - - right == *this; - result == *this; - } - { - return vect_ = right.vect_; - } - - - public: virtual ~vector ( void ) - {} - - - - public: void reserve ( size_type count ) - precondition { count < max_size(); } - postcondition { capacity() >= count; } - { - vector_.reserve(count); - } - - - public: size_type capacity ( void ) const - postcondition(result) { result >= size(); } - { - return vector_.capacity(); - } - - - public: iterator begin ( void ) - postcondition { - - if(empty()) { - result == end(); - } - } - { - return vector_.begin(); - } - - - public: const_iterator begin ( void ) const - postcondition(result) { - - if(empty()) { result == end(); } - } - { - return vector_.begin(); - } - - - public: iterator end ( void ) - { - return vector_.end(); - } - - - public: const_iterator end ( void ) const - { - return vector_.end(); - } - - - public: reverse_iterator rbegin ( void ) - postcondition(result) { - - if(empty()) { result == rend(); } - } - { - return vector_.rbegin(); - } - - - public: const_reverse_iterator rbegin ( void ) const - postcondition(result) { - - if(empty()) { result == rend(); } - } - { - return vector_.rbegin(); - } - - - public: reverse_iterator rend ( void ) - { - return vector_.rend(); - } - - - public: const_reverse_iterator rend ( void ) const - { - return vector_.rend(); - } - - - public: void resize ( size_type count ) - postcondition { - - size() == count; - if(count > oldof size()) { - boost::algorithm::all_of_equal(begin() + oldof size(), end(), - T()); - } - } - { - vectcor_.resize(count); - } - - - public: void resize ( size_type count, T value ) - postcondition { - - size() == count; - count > oldof size() ? - boost::algorithm::all_of_equal(begin() + oldof size(), end(), - value) - : - true - ; - } - { - vector_.resize(count, value); - } - - - public: size_type size ( void ) const - postcondition(result) { result <= capacity(); } - { - return vector_.size(); - } - - - public: size_type max_size ( void ) const - postcondition(result) { result >= capacity(); } - { - return vector_.max_size(); - } - - - public: bool empty ( void ) const - postcondition(result) { - - result == (size() == 0); - } - { - return vector_.empty(); - } - - - public: Alloctor get_allocator ( void ) const - { - return vector_.get_allocator(); - } - - - public: reference at ( size_type index ) - precondition { index < size(); } - { - return vectcor_.at(index); - } - - - public: const_reference at ( size_type index ) const - precondition { index < size(); } - { - return vector_.at(index); - } - - - public: reference operator[] ( size_type index ) - precondition { index < size(); } - { - return vector_[index]; - } - - - public: const_reference operator[] ( size_type index ) const - precondition { index < size(); } - { - return vectcor_[index]; - } - - - public: reference front ( void ) - precondition { not empty(); } - { - return vectcor_.front(); - } - - - public: const_reference front ( void ) const - precondition { bool(!empty()); } - { - return vector_.front(); - } - - - public: reference back ( void ) - precondition { not empty(); } - { - return vector_.back(); - } - - - public: const_reference back ( void ) const - precondition { not empty(); } - { - return vector_.back(); - } - - - public void push_back ( const T& value ) - precondition { size() < max_size() } - postcondition { - - - static if(boost::has_equal_to::value) { back() == value; } - size() == oldof size() + 1; - capacity() >= oldof capacity() - } - { - vector_.push_back(value); - } - - - public: void pop_back ( void ) - precondition { not empty(); } - postcondition { - - size() == oldof size() - 1; - } - { - vector_.pop_back(); - } - - - public: template< class Iterator > - requires std::InputIterator - void assign ( Iterator first, Iterator last ) - // precondition: [begin(), end()) does not contain [first, last) - postcondition { std::distance(first, last) == int(size()); } - { - vector_.assign(first, last); - } - - - public: void assign ( size_type count, const T& vallue ) - precondition { count <= max_size(); } - postcondition { - boost::algorithm::all_of_equal(begin(), end(), value); - - } - { - vector_.assign(count, value); - } - - - public: iterator insert ( iterator where, const T& value ) - precondition { size() < max_size(); } - postcondition(result) { - - - value == *result; - size() == oldof size() + 1; - // if(capacity() > oldof capacity()) - // [begin(), end()) is invalid - // else - // [where, end()) is invalid - } - { - return vector_.insert(where, value); - } - - - public: void insert ( iterator where, size_type count, - const T& value ) - precondition { size() + count < max_size(); } - postcondition { - - - - - size() == oldof size() + count; - capacity() >= oldof capacity(); - if(capacity() == oldof capacity()) { - boost::algorithm::all_of_equal(boost::prior(oldof where), - boost::prior(oldof where) + count, value); - - // [where, end()) is invalid - } // else [begin(), end()) is invalid - } - { - vector_.insert(where, count, value); - } - - - public: template< class Iterator > - requires std::InputIterator - void insert ( iterator where, Iterator first, Iterator last ) - precondition { - // [first, last) is not contained in [begin(), end()) - size() + std::distance(first, last) < max_size(); - } - postcondition { - - - size() == oldof size() + std::distance(first, last); - capacity() >= oldof capacity(); - } - { - vector_.insert(where, first, last); - } - - - public: iterator erase ( iterator where ) - precondition { - not empty(); - where != end(); - } - postcondition(result) { - - - size() == oldod size() - 1; - if(empty()) { result == end(); } - // [where, end()) is invalid - } - { - return vector_.erase(where); - } - - - public: iterator erase ( iterator first, iterator last ) - precondition { size() >= std::distance(first, lasst); } - postcondition(result) { - - - size() == oldof size() - std::distance(first, last); - if(empty()) { result == end(); } - // [first, last) is invalid - } - { - return vector_.erase(first, last); - } - - - public: void clear ( void ) - postcondition( empty() ) - { - vector_.clear(); - } - - - public: void swap ( vector& right ) - postcondition { - - - right == oldof *this; - oldof right == *this; - } - { - vector_.swap(right); - } - - friend bool operator== ( vector const& left, vector const& right ) - { - return left.vector_ == right.vector_; - } - - private: std::vector vector_; -}; -//] - diff --git a/example/n2081/add.cpp b/example/n2081/add.cpp deleted file mode 100644 index 0be71cf..0000000 --- a/example/n2081/add.cpp +++ /dev/null @@ -1,20 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_add -// File: add.cpp -#include "add.hpp" -#include - -int main ( void ) -{ - int x = 10, y = 20; - BOOST_TEST(add(x, y) == 30); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/add.hpp b/example/n2081/add.hpp deleted file mode 100644 index f994eaf..0000000 --- a/example/n2081/add.hpp +++ /dev/null @@ -1,45 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_add_header -// File: add.hpp -#ifndef ADD_HPP -#define ADD_HPP - -#include -#include -#include - -template< typename T > -struct Addable // User-defined concept. -{ - BOOST_CONCEPT_USAGE(Addable) - { - return_type(x + y); // Check addition `T operator+(T x, T y)`. - } - -private: - void return_type ( T const& ) {} // Used to check addition returns type `T`. - - T const& x; - T const& y; -}; - -CONTRACT_FUNCTION( - template( typename T ) requires( Addable ) - (T) (add) ( (T const&) x, (T const&) y ) - postcondition( - auto result = return, - result == x + y, requires boost::has_equal_to::value - ) -) { - return x + y; -} - -#endif // #include guard -//] - diff --git a/example/n2081/add_error.cpp b/example/n2081/add_error.cpp deleted file mode 100644 index 02953e9..0000000 --- a/example/n2081/add_error.cpp +++ /dev/null @@ -1,25 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_add_error -// File: add_error.cpp -#include "add.hpp" - -struct num -{ - int value; - num ( int v = 0 ) : value(v) {}; -}; - -int main ( void ) -{ - num n(10), m(20); - add(n, m); // Error: Correctly fails `add` concept requirements. - return 0; -} -//] - diff --git a/example/n2081/advance.cpp b/example/n2081/advance.cpp deleted file mode 100644 index 628085c..0000000 --- a/example/n2081/advance.cpp +++ /dev/null @@ -1,98 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_advance -// File: advance.cpp -#include -#include -#include -#include -#include -#include - -namespace aux { // Tag dispatch helpers (in a private namespace). - -template< typename InputIterator, typename Distance > -void myadvance_dispatch ( InputIterator& i, Distance n, - std::input_iterator_tag ) -{ - CONTRACT_LOOP( while(n--) ) { - CONTRACT_LOOP_VARIANT_TPL( const( n ) n ) - ++i; - } -} - -template< typename BidirectionalIterator, typename Distance > -void myadvance_dispatch ( BidirectionalIterator& i, Distance n, - std::bidirectional_iterator_tag ) -{ - if(n >= 0) { - CONTRACT_LOOP( while(n--) ) { - CONTRACT_LOOP_VARIANT_TPL( const( n ) n ) - ++i; - } - } else { -#ifndef CONTRACT_CONFIG_NO_LOOP_VARIANTS - // Avoid unused variable warning when loop invariants are disabled. - Distance n_max = n; -#endif - CONTRACT_LOOP( while(n++) ) { - CONTRACT_LOOP_VARIANT_TPL( const( n_max, n ) n_max - n ) - --i; - } - } -} - -template< typename RandomAccessIterator, typename Distance > -void myadvance_dispatch ( RandomAccessIterator& i, Distance n, - std::random_access_iterator_tag ) -{ - i += n; -} - -} // namespace aux - -// Contract helper meta-function. -template< typename T > struct is_input_iterator : boost::mpl::false_ {}; -template< > struct is_input_iterator : - boost::mpl::true_ {}; - -CONTRACT_FUNCTION( - template( typename InputIterator, typename Distance ) - void (myadvance) ( (InputIterator&) i, (Distance) n ) - precondition( - // range [i, i + n] is non-singular. - if(is_input_iterator:: - iterator_category>::value) ( - n > 0 // if input iterator, n positive - ) - ) - postcondition( - auto old_i = CONTRACT_OLDOF i, - std::distance(old_i, i) == n // iterator advanced of n - ) -) { - aux::myadvance_dispatch(i, n, typename - std::iterator_traits:: iterator_category()); -} - -int main ( void ) -{ - std::vector v(10); - v[2] = 123; v[3] = -123; - std::vector::iterator r = v.begin(); // Random iterator. - myadvance(r, 3); - BOOST_TEST(*r == -123); - - std::list l(v.begin(), v.end()); - std::list::iterator b = l.begin(); // Bidirectional and not random. - myadvance(b, 2); - BOOST_TEST(*b == 123); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/apply.cpp b/example/n2081/apply.cpp deleted file mode 100644 index 9934c58..0000000 --- a/example/n2081/apply.cpp +++ /dev/null @@ -1,70 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_apply -// File: apply.cpp -#include -#include -#include -#include - -// Use assertion requirements to model assertion computational complexity. -#define O_1 0 // constant computational complexity O(1) -#define O_BODY 10 // same computation complexity of the body -#define COMPLEXITY_MAX O_1 // only check assertions with complexity within O(1) - -CONTRACT_FUNCTION( // Invoke unary functors. - template( typename Result, typename Argument0, typename Function ) - requires( (boost::UnaryFunction) ) - (Result) (apply) ( (Function) function, (Argument0) argument0, - (Result&) result ) - postcondition( - auto return_value = return, - result == function(argument0), - requires O_BODY <= COMPLEXITY_MAX && - boost::has_equal_to::value, - return_value == result, - requires boost::has_equal_to::value - ) -) { - return result = function(argument0); -} - -CONTRACT_FUNCTION( // Overload to invoke binary functors. - template( typename Result, typename Argument0, typename Argument1, - typename Function ) - requires( (boost::BinaryFunction) ) - (Result) (apply) ( (Function) function, (Argument0) argument0, - (Argument1) argument1, (Result&) result ) - postcondition( - auto return_value = return, - result == function(argument0, argument1), - requires O_BODY <= COMPLEXITY_MAX && - boost::has_equal_to::value, - return_value == result, - requires boost::has_equal_to::value - ) -) { - return result = function(argument0, argument1); -} - -int complement ( int x ) { return -x; } -int add ( int x, int y ) { return x + y; } - -int main ( void ) -{ - int r = 0; - apply(complement, 1, r); - BOOST_TEST(r == -1); - - apply(add, 1, 2, r); - BOOST_TEST(r == 3); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/convert.cpp b/example/n2081/convert.cpp deleted file mode 100644 index 33bb7b1..0000000 --- a/example/n2081/convert.cpp +++ /dev/null @@ -1,19 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_convert -// File: convert.cpp -#include "convert.hpp" -#include - -int main ( void ) -{ - BOOST_TEST(convert('\0') == 0); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/convert.hpp b/example/n2081/convert.hpp deleted file mode 100644 index d55a31a..0000000 --- a/example/n2081/convert.hpp +++ /dev/null @@ -1,26 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_convert_header -// File: convert.hpp -#ifndef CONVERT_HPP_ -#define CONVERT_HPP_ - -#include -#include - -CONTRACT_FUNCTION( - template( typename To, typename From ) - requires( (boost::Convertible) ) - (To) (convert) ( (From const&) from ) -) { - return from; -} - -#endif // #include guard -//] - diff --git a/example/n2081/convert_error.cpp b/example/n2081/convert_error.cpp deleted file mode 100644 index 9e581d2..0000000 --- a/example/n2081/convert_error.cpp +++ /dev/null @@ -1,18 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_convert_error -// File: convert_error.cpp -#include "convert.hpp" - -int main ( void ) -{ - convert(10); // Error: Correctly cannot convert type. - return 0; -} -//] - diff --git a/example/n2081/count.cpp b/example/n2081/count.cpp deleted file mode 100644 index 7db1c4e..0000000 --- a/example/n2081/count.cpp +++ /dev/null @@ -1,48 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_count -// File: count.cpp -#include -#include -#include -#include - -CONTRACT_FUNCTION( - template( typename Iterator ) - requires( - boost::InputIterator, - boost::EqualityComparable, - boost::EqualityComparable< - typename boost::InputIterator::value_type> - ) - (typename boost::InputIterator::difference_type) (mycount) ( - (Iterator) first, (Iterator) last, - (typename boost::InputIterator::value_type const&) value ) - // precondition: range [first, last) is valid - postcondition( auto result = return, result >= 0 ) -) { - typename boost::InputIterator::difference_type result = 0; - CONTRACT_LOOP( while(first != last) ) { // OK: Iterator has `==`. - CONTRACT_LOOP_VARIANT_TPL( - const( first, last ) std::distance(first, last) ) - if(*first == value) // OK: Value is equality comparable. - ++result; - ++first; // OK: Iterator is input iterator. - } - return result; // OK: Input iterator difference is copy constructible. -} - -int main ( void ) -{ - std::vector v(3); - v[0] = -1; v[1] = 0; v[2] = -1; - BOOST_TEST(mycount(v.begin(), v.end(), -1) == 2); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/deref.cpp b/example/n2081/deref.cpp deleted file mode 100644 index 5f24d2b..0000000 --- a/example/n2081/deref.cpp +++ /dev/null @@ -1,43 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_deref -// File: deref.cpp -#include -#include -#include -#include -#include - -CONTRACT_FUNCTION( - template( typename Iterator ) - requires( - boost::InputIterator, - boost::CopyConstructible< - typename boost::InputIterator::value_type> - ) - (typename boost::InputIterator::value_type) (deref) ( - (Iterator) iterator ) - // precondition: iterator is non-singular - postcondition( - auto result = return, - result == *iterator, requires boost::has_equal_to< - typename boost::InputIterator::value_type>::value - ) -) { - return *iterator; -} - -int main ( void ) -{ - std::vector v(1); - v[0] = 123; - BOOST_TEST(deref(v.begin()) == 123); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/equal.cpp b/example/n2081/equal.cpp deleted file mode 100644 index 9b10312..0000000 --- a/example/n2081/equal.cpp +++ /dev/null @@ -1,20 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_equal -// File: equal.cpp -#include "equal.hpp" -#include - -int main ( void) -{ - BOOST_TEST(equal(1, 1) == true); - BOOST_TEST(equal(1, 2) == false); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/equal.hpp b/example/n2081/equal.hpp deleted file mode 100644 index 68066e4..0000000 --- a/example/n2081/equal.hpp +++ /dev/null @@ -1,27 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_equal_header -// File: equal.hpp -#ifndef EQUAL_HPP_ -#define EQUAL_HPP_ - -#include -#include - -CONTRACT_FUNCTION( - template( typename T ) - requires( boost::EqualityComparable ) - bool (equal) ( (T const&) left, (T const&) right ) - postcondition( auto result = return, result == (left == right) ) -) { - return left == right; -} - -#endif // #include guard -//] - diff --git a/example/n2081/equal_error.cpp b/example/n2081/equal_error.cpp deleted file mode 100644 index 15ecc2e..0000000 --- a/example/n2081/equal_error.cpp +++ /dev/null @@ -1,24 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_equal_error -// File: equal_error.cpp -#include "equal.hpp" - -struct num -{ - int value; - explicit num ( int v = 0 ) : value(v) {} -}; - -int main ( void ) -{ - equal(num(1), num(1)); // Compiler error. - return 0; -} -//] - diff --git a/example/n2081/find.cpp b/example/n2081/find.cpp deleted file mode 100644 index 110201d..0000000 --- a/example/n2081/find.cpp +++ /dev/null @@ -1,22 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_find -// File: find.cpp -#include "find.hpp" -#include -#include - -int main ( void ) -{ - std::vector ints(3); - ints[0] = 1; ints[1] = 2; ints[2] = 3; - BOOST_TEST(*myfind(ints.begin(), ints.end(), 2) == 2); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/find.hpp b/example/n2081/find.hpp deleted file mode 100644 index a805367..0000000 --- a/example/n2081/find.hpp +++ /dev/null @@ -1,43 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_find_header -// File: find.hpp -#ifndef FIND_HPP_ -#define FIND_HPP_ - -#include -#include - -CONTRACT_FUNCTION( - template( typename Iterator ) - requires( - boost::InputIterator, - boost::EqualityComparable< // Equality needed to find value. - typename boost::InputIterator::value_type> - ) - (Iterator) (myfind) ( (Iterator) first, (Iterator) last, - (typename boost::InputIterator::value_type const&) value ) - // precondition: range [first, last) is valid - postcondition( - auto result = return, - if(result != last) ( - value == *result // if result not last, value found - ) - ) -) { - CONTRACT_LOOP( while(first != last && *first != value) ) { - CONTRACT_LOOP_VARIANT_TPL( - const( first, last ) std::distance(first, last) ) - ++first; - } - return first; -} - -#endif // #include guard -//] - diff --git a/example/n2081/find_error.cpp b/example/n2081/find_error.cpp deleted file mode 100644 index 93f8bbb..0000000 --- a/example/n2081/find_error.cpp +++ /dev/null @@ -1,28 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_find_error -// File: find_error.cpp -#include "find.hpp" -#include - -struct num -{ - int value; - explicit num ( int v = 0 ) : value(v) {} -}; - -int main ( void ) -{ - std::vector nums(3); - nums[0] = num(1); nums[1] = num(2); nums[2] = num(3); - // Error: Correctly, num does not meet concept requirements. - myfind(nums.begin(), nums.end(), num(2)); - return 0; -} -//] - diff --git a/example/n2081/for_each.cpp b/example/n2081/for_each.cpp deleted file mode 100644 index 9dfd5a4..0000000 --- a/example/n2081/for_each.cpp +++ /dev/null @@ -1,52 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_for_each -// File: for_each.cpp -#include -#include -#include -#include -#include - -CONTRACT_FUNCTION( - template( typename Iterator, typename Function ) - requires( - boost::InputIterator, - (boost::UnaryFunction::value_type>) - ) - (Function) (my_for_each) ( (Iterator) first, (Iterator) last, - (Function) function ) - // precondition: range [first, last) is valid - postcondition( - auto result = return, - result == function, requires boost::has_equal_to::value - ) -) { - CONTRACT_LOOP( while(first < last) ) { // OK: Iterator is InputIterator. - CONTRACT_LOOP_VARIANT_TPL( - const( first, last ) std::distance(first, last) ) - function(*first); // OK: Function is UnaryFunction. - ++first; // OK: Iterator is InputIterator. - } - return function; -} - -int total = 0; -void add ( int i ) { total += i; } - -int main ( void ) -{ - std::vector v(3); - v[0] = 1; v[1] = 2; v[2] = 3; - my_for_each(v.begin(), v.end(), add); - BOOST_TEST(total == 6); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/less_eq.cpp b/example/n2081/less_eq.cpp deleted file mode 100644 index 5bd31d9..0000000 --- a/example/n2081/less_eq.cpp +++ /dev/null @@ -1,36 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_less_eq -// File: less_eq.cpp -#include -#include -#include - -CONTRACT_FUNCTION( - template( typename T ) - requires( - boost::EqualityComparable, - boost::LessThanComparable - ) - bool (less_eq) ( (T) left, (T) right ) - postcondition( - auto result = return, - result == (left < right || left == right) - ) -) { - return left < right || left == right; -} - -int main ( void ) -{ - BOOST_TEST(less_eq(1, 2) == true); - BOOST_TEST(less_eq(2, 1) == false); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/min.cpp b/example/n2081/min.cpp deleted file mode 100644 index 417cea9..0000000 --- a/example/n2081/min.cpp +++ /dev/null @@ -1,20 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_min -// File: min.cpp -#include "min.hpp" -#include - -int main ( void ) -{ - BOOST_TEST(min(1, 2) == 1); - BOOST_TEST(min(-1, -2) == -2); - return boost::report_errors(); -} -//] - diff --git a/example/n2081/min.hpp b/example/n2081/min.hpp deleted file mode 100644 index 7f1e675..0000000 --- a/example/n2081/min.hpp +++ /dev/null @@ -1,31 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_min_header -// File: min.hpp -#ifndef MIN_HPP_ -#define MIN_HPP_ - -#include -#include -#include - -CONTRACT_FUNCTION( - template( typename T ) requires( boost::LessThanComparable ) - (T const&) (min) ( (T const&) x, (T const&) y ) - postcondition( - auto result = return, - x < y ? result == x : result == y, - requires boost::has_equal_to::value - ) -) { - return x < y ? x : y; // OK: T is less than comparable `<`. -} - -#endif // #include guard -//] - diff --git a/example/n2081/min_error.cpp b/example/n2081/min_error.cpp deleted file mode 100644 index 8fe73f2..0000000 --- a/example/n2081/min_error.cpp +++ /dev/null @@ -1,24 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_min_error -// File: min_error.cpp -#include "min.hpp" - -struct num -{ - int value; - explicit num ( int v = 0 ) : value(v) {} -}; - -int main ( void ) -{ - min(num(1), num(2)); // Compiler error: Fail concept requirements. - return 0; -} -//] - diff --git a/example/n2081/transform.cpp b/example/n2081/transform.cpp deleted file mode 100644 index f2be053..0000000 --- a/example/n2081/transform.cpp +++ /dev/null @@ -1,68 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[n2081_transform -// File: transform.cpp - -#define CONTRACT_CONFIG_FUNCTION_ARITY_MAX 5 // Support for 5 parameters. -#include - -#include -#include -#include -#include -#include - -CONTRACT_FUNCTION( - template( - typename Iterator1, - typename Iterator2, - typename ResultIterator, - typename Function - ) - requires( - boost::InputIterator, - boost::InputIterator, - (boost::OutputIterator::value_type>), - (boost::BinaryFunction::value_type, - typename boost::InputIterator::value_type, - typename boost::InputIterator::value_type>) - ) - (ResultIterator) (mytransform) ( - (Iterator1) first1, - (Iterator1) last1, - (Iterator2) first2, - (ResultIterator) result, - (Function) function - ) - // precondition: [first1, last1) is valid - // precondition: [first2, first2 + (last1 - first1)) is valid - // precondition: result is not an iterator within [first1 + 1, last1) - // or [first2 + 1, first2 + (last1 - first1)) - // precondition: [result, result + (last1 - first1)) is valid -) { - return std::transform(first1, last1, first2, result, function); -} - -int main ( void ) -{ - std::vector v(3); - v[0] = 1; v[1] = 2; v[2] = 3; - std::vector w(3); - w[0] = 10; w[1] = 20; w[2] = 30; - - mytransform(v.begin(), v.end(), w.begin(), v.begin(), std::plus()); - - BOOST_TEST(v[0] == 11); - BOOST_TEST(v[1] == 22); - BOOST_TEST(v[2] == 33); - return boost::report_errors(); -} -//] - diff --git a/example/stroustrup97/string.cpp b/example/stroustrup97/string.cpp deleted file mode 100644 index f5b109c..0000000 --- a/example/stroustrup97/string.cpp +++ /dev/null @@ -1,33 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[stroustrup97_string -// File: string.cpp -#include "string.hpp" - -CONTRACT_CONSTRUCTOR_BODY(string, string) ( const char* chars ) - { init(chars); } - -CONTRACT_CONSTRUCTOR_BODY(string, string) ( const string& other ) - { init(other.chars_); } - -CONTRACT_DESTRUCTOR_BODY(string, ~string) ( void ) - { delete[] chars_; } - -char& string::CONTRACT_MEMBER_BODY(operator([])(at)) ( int index ) - { return chars_[index]; } - -int string::CONTRACT_MEMBER_BODY(size) ( void ) const { return size_; } - -void string::CONTRACT_MEMBER_BODY(init) ( const char* chars ) { - size_ = strlen(chars); - chars_ = new char[size_ + 1]; - for(int i = 0; i < size_; ++i) chars_[i] = chars[i]; - chars_[size_] = '\0'; -} -//] - diff --git a/example/stroustrup97/string.hpp b/example/stroustrup97/string.hpp deleted file mode 100644 index 0c089b1..0000000 --- a/example/stroustrup97/string.hpp +++ /dev/null @@ -1,81 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[stroustrup97_string_header -// File: string.hpp -#ifndef STRING_HPP_ -#define STRING_HPP_ - -#include -#include - -// Adapted from an example presented in [Stroustrup1997] to illustrate -// importance of class invariants. Simple preconditions were added where it -// made sense. This should be compiled with postconditions checking turned off -// (define the `CONTRACT_CONFIG_NO_POSTCONDITIONS` macro) because -// postconditions are deliberately not used. -// See [Stroustrup1997] for a discussion on the importance of class invariants, -// and on pros and cons of using pre and post conditions. -CONTRACT_CLASS( - class (string) -) { - CONTRACT_CLASS_INVARIANT( - // It would be better to assert conditions separately so to generate - // more informative error in case they fail. - chars_ ? true : throw invariant_error(), - size_ >= 0 ? true : throw invariant_error(), - too_large >= size_ ? true : throw invariant_error(), - chars_[size_] == '\0' ? true : throw invariant_error() - ) - - // Broken contracts throw user defined exceptions. - public: class range_error {}; - public: class invariant_error {}; - public: class null_error {}; - public: class too_large_error {}; - - public: enum { too_large = 16000 }; // Length limit. - - CONTRACT_CONSTRUCTOR( - public (string) ( (const char*) chars ) - precondition( - chars ? true : throw null_error(), - strlen(chars) <= too_large ? true : throw too_large_error() - ) - ) ; // Deferred body definition. - - CONTRACT_CONSTRUCTOR( - public (string) ( (const string&) other ) - ) ; - - CONTRACT_DESTRUCTOR( - public (~string) ( void ) - ) ; - - CONTRACT_FUNCTION( - public (char&) operator([])(at) ( int index ) - precondition( - index >= 0 ? true : throw range_error(), - size_ > index ? true : throw range_error() - ) - ) ; - - CONTRACT_FUNCTION( - public int (size) ( void ) const - ) ; - - CONTRACT_FUNCTION( // Not public so it does not check class invariants. - private void (init) ( (const char*) q ) - ) ; - - private: int size_; - private: char* chars_; -}; - -#endif // #include guard -//] - diff --git a/example/stroustrup97/string_main.cpp b/example/stroustrup97/string_main.cpp deleted file mode 100644 index b340f2b..0000000 --- a/example/stroustrup97/string_main.cpp +++ /dev/null @@ -1,47 +0,0 @@ - -// Copyright (C) 2008-2012 Lorenzo Caminiti -// Distributed under the Boost Software License, Version 1.0 -// (see accompanying file LICENSE_1_0.txt or a copy at -// http://www.boost.org/LICENSE_1_0.txt) -// Home at http://sourceforge.net/projects/contractpp - -//[stroustrup97_string_main -// File: string_main.cpp -#include "string.hpp" -#include - -// Handler that re-throws contract broken exceptions instead of terminating. -void throwing_handler ( contract::from const& context ) -{ - if(context == contract::FROM_DESTRUCTOR) { - // Destructor cannot throw for STL exception safety (ignore error). - std::clog << "Ignored destructor contract failure" << std::endl; - } else { - // Failure handlers always called with active an exception. - throw; // Re-throw active exception thrown by precondition. - } -} - -int main ( void ) -{ - // Setup all contract failure handlers to throw (instead of terminate). - contract::set_precondition_broken(&throwing_handler); - contract::set_postcondition_broken(&throwing_handler); - contract::set_class_invariant_broken(&throwing_handler); - contract::set_block_invariant_broken(&throwing_handler); - contract::set_loop_variant_broken(&throwing_handler); - - string s("abc"); - BOOST_TEST(s[0] == 'a'); - -#ifndef CONTRACT_CONFIG_NO_PRECONDITIONS - bool pass = false; - try { s[3]; } // Out of range. - catch(string::range_error) { pass = true; } - BOOST_TEST(pass); -#endif - - return boost::report_errors(); -} -//] - diff --git a/tool/boost_setup/cygwin-boost-env.sh b/tool/boost_setup/cygwin-boost-env.sh deleted file mode 100644 index 3811c5b..0000000 --- a/tool/boost_setup/cygwin-boost-env.sh +++ /dev/null @@ -1,15 +0,0 @@ - -# Copyright (C) 2009-2011 Lorenzo Caminiti -# Use, modification, and distribution is subject to the Boost Software -# License, Version 1.0 (see accompanying file LICENSE_1_0.txt or a -# copy at http://www.boost.org/LICENSE_1_0.txt). - -#export BOOST_ROOT="$HOME/Desktop/code/boost/trunk.cyg" -export BOOST_ROOT="$HOME/Desktop/code/boost_1_50_0.cyg" -export PATH="$BOOST_ROOT:$PATH" - -echo "HOME=$HOME" -echo "BOOST_ROOT=$BOOST_ROOT" -echo -echo "Make sure \"$HOME/user-config.jam\" exists and it is correct" - diff --git a/tool/boost_setup/cygwin-user-config.jam b/tool/boost_setup/cygwin-user-config.jam deleted file mode 100644 index 311beb2..0000000 --- a/tool/boost_setup/cygwin-user-config.jam +++ /dev/null @@ -1,10 +0,0 @@ - -# Copyright (C) 2009-2011 Lorenzo Caminiti -# Use, modification, and distribution is subject to the Boost Software -# License, Version 1.0 (see accompanying file LICENSE_1_0.txt or a -# copy at http://www.boost.org/LICENSE_1_0.txt). - -# Toolset. -using gcc ; -using python ; - diff --git a/tool/boost_setup/linux-boost-env.sh b/tool/boost_setup/linux-boost-env.sh deleted file mode 100644 index 95dd4de..0000000 --- a/tool/boost_setup/linux-boost-env.sh +++ /dev/null @@ -1,15 +0,0 @@ - -# Copyright (C) 2008-2012 Lorenzo Caminiti -# Distributed under the Boost Software License, Version 1.0 -# (see accompanying file LICENSE_1_0.txt or a copy at -# http://www.boost.org/LICENSE_1_0.txt) -# Home at http://sourceforge.net/projects/contractpp - -export BOOST_ROOT="$HOME/Desktop/code/boost/trunk.linux" -export PATH="$BOOST_ROOT:$PATH" - -echo "HOME=$HOME" -echo "BOOST_ROOT=$BOOST_ROOT" -echo -echo "Make sure \"$HOME/user-config.jam\" exists and it is correct" - diff --git a/tool/boost_setup/linux-user-config.jam b/tool/boost_setup/linux-user-config.jam deleted file mode 100644 index 6c8ef93..0000000 --- a/tool/boost_setup/linux-user-config.jam +++ /dev/null @@ -1,19 +0,0 @@ - -# Copyright (C) 2008-2012 Lorenzo Caminiti -# Distributed under the Boost Software License, Version 1.0 -# (see accompanying file LICENSE_1_0.txt or a copy at -# http://www.boost.org/LICENSE_1_0.txt) -# Home at http://sourceforge.net/projects/contractpp - -using gcc ; -using python ; - -# Documentation tools. -using quickbook ; -using xsltproc ; -using boostbook - : "/usr/share/xml/docbook/stylesheet/nwalsh" - : "/usr/share/xml/docbook/schema/dtd/4.2" - ; -using doxygen ; - diff --git a/tool/boost_setup/windows-boost-env.bat b/tool/boost_setup/windows-boost-env.bat deleted file mode 100644 index 6239d6e..0000000 --- a/tool/boost_setup/windows-boost-env.bat +++ /dev/null @@ -1,17 +0,0 @@ - -REM Copyright (C) 2009-2011 Lorenzo Caminiti -REM Use, modification, and distribution is subject to the Boost Software -REM License, Version 1.0 (see accompanying file LICENSE_1_0.txt or a -REM copy at http://www.boost.org/LICENSE_1_0.txt). - -@ECHO OFF - -set BOOST_ROOT=%HOMEDRIVE%%HOMEPATH%\Desktop\code\boost_1_50_0.win -set PATH="C:\PROGRA~2\boost\xml\bin";%BOOST_ROOT%;%PATH% - -ECHO HOME=%HOMEDRIVE%%HOMEPATH% -ECHO BOOST_ROOT=%BOOST_ROOT% -ECHO BOOST_BUILD_PATH=%BOOST_BUILD_PATH% -ECHO. -ECHO Make sure "%HOMEDRIVE%%HOMEPATH%\user-config.jam" exists and it is correct - diff --git a/tool/boost_setup/windows-user-config.jam b/tool/boost_setup/windows-user-config.jam deleted file mode 100644 index 84c0838..0000000 --- a/tool/boost_setup/windows-user-config.jam +++ /dev/null @@ -1,24 +0,0 @@ - -# Copyright (C) 2009-2011 Lorenzo Caminiti -# Use, modification, and distribution is subject to the Boost Software -# License, Version 1.0 (see accompanying file LICENSE_1_0.txt or a -# copy at http://www.boost.org/LICENSE_1_0.txt). - -# Toolset. -using msvc ; -using python ; - -# Documentation tools -using quickbook : "C:/PROGRA~2/boost/xml/bin/quickbook.exe" : ; -using xsltproc : "C:/PROGRA~2/boost/xml/bin/xsltproc.exe" ; -using boostbook - : "C:/PROGRA~2/boost/xml/docbook-xsl" - : "C:/PROGRA~2/boost/xml/docbook-xml" - ; -using doxygen : "C:/PROGRA~2/doxygen/bin/doxygen.exe" ; -# For PDF documentation. -using fop - : "C:/PROGRA~1/RenderX/XEP/xep.bat" - : "C:/PROGRA~1/Java/jre6/bin" - ; - diff --git a/tool/copyright_header.py b/tool/copyright_header.py deleted file mode 100644 index b7b7fd9..0000000 --- a/tool/copyright_header.py +++ /dev/null @@ -1,121 +0,0 @@ - -# Copyright (C) 2008-2012 Lorenzo Caminiti -# Distributed under the Boost Software License, Version 1.0 -# (see accompanying file LICENSE_1_0.txt or a copy at -# http://www.boost.org/LICENSE_1_0.txt) -# Home at http://sourceforge.net/projects/contractpp - -import sys -import os; -import re; -import getopt; -import sh; - -def parse_args(): - COMMENT_FOR_FILE = { # Comment line start and end characters. - '.cpp': ['// ', ''], - '.hpp': ['// ', ''], - '.qbk': ['[/ ', ' ]'], - '.jam': ['# ', ''], - '.v2': ['# ', ''], - '.py': ['# ', ''], - '.sh': ['# ', ''], - '.bat': ['REM ', ''], - } - START_WORD_DFLT = 'Copyright' # Default header starting word. - HEADER_FILE_DFLT = "../COPYRIGHT.txt" # Default header text file. - - try: - (opts, args) = getopt.getopt(sys.argv[1:], '', []) - if len(args) == 0: - raise getopt.GetoptError('Missing DIR argument') - elif len(args) == 1: - dir = args[0] - header_file = HEADER_FILE_DFLT - start_word = START_WORD_DFLT - elif len(args) == 2: - dir = args[0] - header_file = args[1] - start_word = START_WORD_DFLT - elif len(args) == 3: - dir = args[0] - header_file = args[1] - start_word = args[2] - else: - raise getopt.GetoptError('Too many arguments') - except getopt.GetoptError, err: - print "Error: ", err - print """ -Usage: python %s DIR [HEADER_FILE] [START_WORD] -Replace text starting with the work START_WORD at file's header with the test -from HEADER_FILE. - -All files in DIR with the following extensions are recursively processed: - %s - -Defaults: - HEADER_FILE %s - START_WORD %s -""" % (os.path.split(sys.argv[0])[1], COMMENT_FOR_FILE.keys(), - HEADER_FILE_DFLT, START_WORD_DFLT) - exit(1) - return (dir, header_file, start_word, COMMENT_FOR_FILE) - -class header: - def __init__(self, header_file): - f = open(header_file, 'rU') - self.__lines = [] - for ln in f.xreadlines(): self.__lines.append(ln.rstrip('\n')) - f.close(); - - def text(self, line_start = '// ', line_end = ''): - s = '' - for ln in self.__lines: s = s + line_start + ln + line_end + '\n' - return s - -class replace_header: - def __init__(self, header_file, start_word, comment_for_file): - self.__header = header(header_file) - self.__start_word = start_word - self.__comment_for_file = comment_for_file - - def __call__(self, ln, inheader, file_path, line_num): - if line_num <= 1: sh.info('Updating "' + file_path + '"...') - (ret_ln, ret_inheader) = ('', None) - - (file_root, file_ext) = os.path.splitext(file_path) - comment_start = self.__comment_for_file[file_ext][0] - comment_end = self.__comment_for_file[file_ext][1] - new_header = '\n' + self.__header.text(comment_start, - comment_end) + '\n' - header_start_re = '^' + re.escape(comment_start + - self.__start_word) + '.*$' - header_continue_re = '^' + re.escape(comment_start) + '.*$' - - if inheader is None: # At very top of file. - if re.match('^ *$', ln): # Skip empty lines at top. - (ret_ln, ret_inheader) = ('', None) - elif re.match(header_start_re, ln): # Old header starts. - (ret_ln, ret_inheader) = ('', True) - else: # Old header ends -- replace it. - (ret_ln, ret_inheader) = (new_header + ln, False) - elif inheader: - if re.match(header_continue_re, ln): # In old header -- skip it. - (ret_ln, ret_inheader) = ('', True) - elif re.match('^ *$', ln): # Skip empty lines after old header. - (ret_ln, ret_inheader) = ('', True) - else: # Old header ends -- replace it. - (ret_ln, ret_inheader) = (new_header + ln, False) - else: # Not in nor entering header. - (ret_ln, ret_inheader) = (ln, False) - return (ret_ln, ret_inheader) - -(dir, header_file, start_word, comment_for_file) = parse_args() -replacer = replace_header(header_file, start_word, comment_for_file) -name_re = '' -for file_ext in comment_for_file.keys(): - if name_re != '': name_re = name_re + '|' - name_re = name_re + '(.*' + re.escape(file_ext) + '$)' - -sh.replace(dir, name_re, replacer) - diff --git a/tool/release_instructions.txt b/tool/release_instructions.txt deleted file mode 100644 index c269cbc..0000000 --- a/tool/release_instructions.txt +++ /dev/null @@ -1,54 +0,0 @@ - -RELEASE INSTRUCTIONS -==================== - -How to release this library version X.Y.Z from SVN trunk to SourceForge (SF). - -1. PREPARE TO RELEASE - -* Make sure all examples and test compiles. -* Make sure that documentation, release version, and release notes are up-to-date. -* Make sure that "trunk/index.html" redirects to "releases/contractpp_X_Y_Z/doc/html/index.html". - -Commit everything (code, documentation, etc) to SVN trunk. - -2. RELEASE BRANCH - -Create a SVN branch for the release X.Y.Z for example from trunk, make sure all code is correctly checked into trunk, then: - - $ svn cp https://contractpp.svn.sourceforge.net/svnroot/contractpp/trunk https://contractpp.svn.sourceforge.net/svnroot/contractpp/releases/contractpp_X_Y_Z - -3. ZIP FILE - -Create a "contractpp_X_Y_Z.zip" file from the release branch (this ZIP file -should not go in SVN, just uploaded it on SF as explained in the next step): - - $ zip contractpp/release/contractpp_X_Y_Z contractpp_X_Y_Z.zip - -4. UPLOAD ZIP FILE TO SF - -Log in to SF website and go to Contract++ page, click Files, then "releases", and then Add File to upload "contract_X_Y_Z.zip". -Click the information icon ("I" icon on the right-hand-side of the file) and select the newly added file as the "Default Download" for all platform then click Save (the file should now show as the "latest version" on the top of the page and SF will link it to the "Download" from the library documentation). - -5. UPLOAD DOCUMENTATION INDEX.HTML - -Using FileZilla connect to the location below and drag-and-drop releases/contract_X_Y_Z/index.html to the project-web/contractpp/htdocs/ localtion: - - Host web.sourceforge.net - Protocol SFTP - Port 22 - Username ... - Password ... - Upload to /home/project-web/contractpp/htdocs - -The LICENSE_1_0.txt and COPYRIGHT.txt files should be copied to this location also (but they might already be there). - -6. FINAL CHECKS - -* Go to the project web http://contractpp.sourceforge.net and check that the latest documentation shows up. -* Click on "Download" for the documentation and check that contractpp_X_Y_Z.zip is downloaded (correct version). - -7. UPDATE INFORMATION ON SF (IF NEEDED) - -Update the information on SF if needed: library release status (pre-alpha, beta, etc), library logo on SF, name, description, feature list, screenshots, etc. - diff --git a/tool/sh.py b/tool/sh.py deleted file mode 100644 index 4ed2c18..0000000 --- a/tool/sh.py +++ /dev/null @@ -1,118 +0,0 @@ - -# Copyright (C) 2008-2012 Lorenzo Caminiti -# Distributed under the Boost Software License, Version 1.0 -# (see accompanying file LICENSE_1_0.txt or a copy at -# http://www.boost.org/LICENSE_1_0.txt) -# Home at http://sourceforge.net/projects/contractpp - -import sys -import os -import shutil -import re -import tempfile -import time - -silent = False - -def info(msg, newline = True): - if not silent: - if newline: print msg - else: sys.stdout.write(msg) - -def err(msg): - print "Error:", msg - -def run(cmd): - if os.system(cmd) != 0: - err('Unable to execute command "' + cmd + '"') - exit() - -def quit_if_exist_is(path, exist, err_msg = ""): - if os.access(path, os.F_OK) == exist: - if err_msg == "": - if not exist: err('File path "' + path + '" not found') - else: err('File path "' + path + '" already exists') - else: err(err_msg) - exit() - -def cp(src, dst): - info("Copying: " + src + " -> " + dst) - quit_if_exist_is(src, False) - if os.path.isdir(src): - quit_if_exist_is(dst, True) # `copytree()` requires dst not exist. - shutil.copytree(src, dst) - else: - shutil.copy2(src, dst) - -def mkdir(dir): - if not os.access(dir, os.F_OK): os.makedirs(dir) - -def read(msg = '', default = ''): - if msg != '': info(msg, False) - s = raw_input() - if s == '': s = default - return s - -def rm(path, interactive = True): - if os.access(path, os.F_OK): - if interactive: user_in = '' - else: user_in = 'y' - while user_in != 'y' and user_in != 'n': - user_in = read( - 'Warning: If "y", existing file(s) will be lost!\n' + - 'Override existing path "' + path + '"? (y/n) ') - if user_in == 'y': - if os.path.isdir(path): shutil.rmtree(path) - else: os.remove(path) - else: - err('Unable to override existing path "' + path + - '" -- manually remove it first') - exit() - -def find(dir, name_re, exec_func = None): - found = [] - for root, dirs, files in os.walk(dir): - for dir in dirs: - path = os.path.join(root, dir) - if re.match(name_re, path): - if not exec_func is None: exec_func(path) - found.append(path) - for file in files: - path = os.path.join(root, file) - if re.match(name_re, path): - if not exec_func is None: exec_func(path) - found.append(path) - return found - -# Can be passed as `replace_func` to `replace()` for simple text replace. -class replace_text: - def __init__(self, find_re, repl_txt): - self.__find_re = find_re - self.__repl_txt = repl_txt - def __call__(self, ln, unused, file_name, line_num): - return (re.sub(self.__find_re, self.__repl_txt, ln), unused) - -def replace(dir, name_re, replace_func, data = None): - class _replace_func: - def __init__(self, func, data): - self.__func = func - self.__data = data - def __call__(self, ifile_name): - ifile = open(ifile_name, 'rU') - ofile_name = ifile_name + str(time.time()) # Time for temp file. - ofile = open(ofile_name, 'w') - func = self.__func - data = self.__data # Copy data so self's data not changed. - ln_num = 0 - for ln in ifile.xreadlines(): - ln_num = ln_num + 1 - (repl_ln, repl_data) = func(ln, data, ifile_name, ln_num) - data = repl_data # Update data within this file replacement. - ofile.write(repl_ln) - ifile.close() - ofile.close() - os.remove(ifile.name) - os.rename(ofile.name, ifile.name) - f = _replace_func(replace_func, data) - find(dir, name_re, f) - diff --git a/wave.cfg b/wave.cfg index e657ea4..e53bf38 100644 --- a/wave.cfg +++ b/wave.cfg @@ -1,11 +1,18 @@ # NOTE: Some of the paths in this file may need to be changed for your system. +-NBOOST_TEST + -D_WIN32 --Sinclude +-S"C:\git\boost-contract\include" -S"C:\git\modular-boost.win" -S"C:\Program Files (x86)\Microsoft Visual Studio 10.0\VC\include" --variadics +--timer + +-opp.cpp +-tpp.dbg +#-cpp.cnt