[Boost-commit] svn:boost r50551 - in sandbox/itl/libs: itl/doc validate/example/labat_single

Subject: [Boost-commit] svn:boost r50551 - in sandbox/itl/libs: itl/doc validate/example/labat_single
From: afojgo_at_[hidden]
Date: 2009-01-12 05:45:09

Author: jofaber
Date: 2009-01-12 05:45:08 EST (Mon, 12 Jan 2009)
New Revision: 50551
URL: http://svn.boost.org/trac/boost/changeset/50551

Log:
Added documentation. Semantics: Concept Induction. Stable {msvc-9.0, partly congcc-4.3-a7}  

Text files modified: 
   sandbox/itl/libs/itl/doc/semantics.qbk                          |   126 +++++++++++++++++++++++++++------------ 
   sandbox/itl/libs/validate/example/labat_single/labat_single.cpp |     8 +-                                      
   2 files changed, 90 insertions(+), 44 deletions(-)

Modified: sandbox/itl/libs/itl/doc/semantics.qbk
==============================================================================
--- sandbox/itl/libs/itl/doc/semantics.qbk	(original)
+++ sandbox/itl/libs/itl/doc/semantics.qbk	2009-01-12 05:45:08 EST (Mon, 12 Jan 2009)
@@ -14,8 +14,8 @@
 instantiation of the variables contained in the law. The following
 pseudocode gives a shorthand notation of such a law.
 ``
-Commutativity<typename T>
-T a, b: a + b == b + a;
+Commutativity<T,+>:
+T a, b; a + b == b + a;
 ``
 This can of course be coded as a proper c++ class template which has 
 been done for the validation of the *itl*. For sake of simplicity 
@@ -141,9 +141,9 @@
 `neutron<S>::value()` which is the empty set `T()`
 these laws hold:
 ``
-Associativity<S,+,== >: S a,b,c: a+(b+c) == (a+b)+c
-Neutrality<S,+,== >   : S a:       a+S() == a
-Commutativity<S,+,== >: S a,b:       a+b == b+a
+Associativity<S,+,== >: S a,b,c; a+(b+c) == (a+b)+c
+Neutrality<S,+,== >   : S a;       a+S() == a
+Commutativity<S,+,== >: S a,b;       a+b == b+a
 ``
 
 [h5 Laws on set intersection]
@@ -152,8 +152,8 @@
 `operator *, *=, &, &=` these laws were validated:
 
 ``
-Associativity<S,*,== >: S a,b,c: a*(b*c) == (a*b)*c
-Commutativity<S,*,== >: S a,b:       a*b == b*a
+Associativity<S,*,== >: S a,b,c; a*(b*c) == (a*b)*c
+Commutativity<S,*,== >: S a,b;       a*b == b*a
 ``
 
 Neutrality has *not* been validated to avoid 
@@ -167,8 +167,8 @@
 is non symmetrical.
 
 ``
-RightNeutrality<S,-,== > : S a:   a-S() == a
-SelfRemovability<S,-,== >: S a:   a - a == S()
+RightNeutrality<S,-,== > : S a;   a-S() == a
+SelfRemovability<S,-,== >: S a;   a - a == S()
 ``
 
 Summarized in the next table are laws that use `+`, `*` and `-`
@@ -197,10 +197,10 @@
 Therefore they are denoted using a /variable/ equality `=v=` below.
 
 ``
-     Distributivity<S,+,*,=v= > : S a,b,c: a + (b * c) =v= (a + b) * (a + c)
-     Distributivity<S,*,+,=v= > : S a,b,c: a * (b + c) =v= (a * b) + (a * c)
-RightDistributivity<S,+,-,=v= > : S a,b,c: (a + b) - c =v= (a - c) + (b - c)
-RightDistributivity<S,*,-,=v= > : S a,b,c: (a * b) - c =v= (a - c) * (b - c)
+     Distributivity<S,+,*,=v= > : S a,b,c; a + (b * c) =v= (a + b) * (a + c)
+     Distributivity<S,*,+,=v= > : S a,b,c; a * (b + c) =v= (a * b) + (a * c)
+RightDistributivity<S,+,-,=v= > : S a,b,c; (a + b) - c =v= (a - c) + (b - c)
+RightDistributivity<S,*,-,=v= > : S a,b,c; (a * b) - c =v= (a - c) * (b - c)
 ``
 
 The next table shows the relationship between 
@@ -254,8 +254,8 @@
 below is an adaption for the binary set difference `-`, which is 
 also called ['*relative complement*].
 ``
-DeMorgan<S,+,*,=v= > : S a,b,c: a - (b + c) =v= (a - b) * (a - c)
-DeMorgan<S,*,+,=v= > : S a,b,c: a - (b * c) =v= (a - b) + (a - c)
+DeMorgan<S,+,*,=v= > : S a,b,c; a - (b + c) =v= (a - b) * (a - c)
+DeMorgan<S,*,+,=v= > : S a,b,c; a - (b * c) =v= (a - b) + (a - c)
 ``
 
 ``
@@ -272,7 +272,7 @@
 [h5 Symmetric Difference]
 
 ``
-SymmetricDifference<S,== > : S a,b,c: (a + b) - (a * b) == (a - b) + (b - a)
+SymmetricDifference<S,== > : S a,b,c; (a + b) - (a * b) == (a - b) + (b - a)
 ``
 
 Finally Symmetrical Difference holds for all of itl set types and
@@ -425,15 +425,15 @@
 [h5 Laws on set union, set intersection and set difference]
 
 ``
-Associativity<C,+,== >: C a,b,c: a+(b+c) == (a+b)+c
-Neutrality<C,+,== >   : C a:       a+C() == a
-Commutativity<C,+,== >: C a,b:       a+b == b+a
+Associativity<C,+,== >: C a,b,c; a+(b+c) == (a+b)+c
+Neutrality<C,+,== >   : C a;       a+C() == a
+Commutativity<C,+,== >: C a,b;       a+b == b+a
 
-Associativity<C,*,== >: C a,b,c: a*(b*c) ==(a*b)*c
-Commutativity<C,*,== >: C a,b:       a*b == b*a
+Associativity<C,*,== >: C a,b,c; a*(b*c) ==(a*b)*c
+Commutativity<C,*,== >: C a,b;       a*b == b*a
 
-RightNeutrality<C,-,== >  : C a:   a-C() ==  a
-SelfRemovability<C,-,=v= >: C a:   a - a =v= C()
+RightNeutrality<C,-,== >  : C a;   a-C() ==  a
+SelfRemovability<C,-,=v= >: C a;   a - a =v= C()
 ``
 
 All the fundamental laws could be validated for all 
@@ -453,10 +453,10 @@
 [h5 Distributivity Laws]
 
 ``
-     Distributivity<C,+,*,=v= > : C a,b,c: a + (b * c) =v= (a + b) * (a + c)
-     Distributivity<C,*,+,=v= > : C a,b,c: a * (b + c) =v= (a * b) + (a * c)
-RightDistributivity<C,+,-,=v= > : C a,b,c: (a + b) - c =v= (a - c) + (b - c)
-RightDistributivity<C,*,-,=v= > : C a,b,c: (a * b) - c =v= (a - c) * (b - c)
+     Distributivity<C,+,*,=v= > : C a,b,c; a + (b * c) =v= (a + b) * (a + c)
+     Distributivity<C,*,+,=v= > : C a,b,c; a * (b + c) =v= (a * b) + (a * c)
+RightDistributivity<C,+,-,=v= > : C a,b,c; (a + b) - c =v= (a - c) + (b - c)
+RightDistributivity<C,*,-,=v= > : C a,b,c; (a * b) - c =v= (a - c) * (b - c)
 ``
 
 Results for the distributivity laws are almost identical to 
@@ -478,8 +478,8 @@
 [h5 DeMorgan's Law and Symmetric Difference]
 
 ``
-DeMorgan<C,+,*,=v= > : C a,b,c: a - (b + c) =v= (a - b) * (a - c)
-DeMorgan<C,*,+,=v= > : C a,b,c: a - (b * c) =v= (a - b) + (a - c)
+DeMorgan<C,+,*,=v= > : C a,b,c; a - (b + c) =v= (a - b) * (a - c)
+DeMorgan<C,*,+,=v= > : C a,b,c; a - (b * c) =v= (a - b) + (a - c)
 ``
 
 ``
@@ -489,7 +489,7 @@
 ``
 
 ``
-SymmetricDifference<C,== > : C a,b,c: (a + b) - (a * b) == (a - b) + (b - a)
+SymmetricDifference<C,== > : C a,b,c; (a + b) - (a * b) == (a - b) + (b - a)
 ``
 
 Reviewing the validity tables above shows, that the sets of valid laws for
@@ -554,7 +554,7 @@
 As we can see later in this section this kind of 
 a total `Quantifier` has the basic properties that
 elements of a 
-vector space 
+[@http://en.wikipedia.org/wiki/Vector_space vector space] 
 do provide.
 
 We will use the terms `TotalQuantifier` and
@@ -620,15 +620,15 @@
 
 
 ``
-Associativity<Q,+,== >: Q a,b,c: a+(b+c) == (a+b)+c
-Neutrality<Q,+,== >   : Q a:       a+Q() == a
-Commutativity<Q,+,== >: Q a,b:       a+b == b+a
+Associativity<Q,+,== >: Q a,b,c; a+(b+c) == (a+b)+c
+Neutrality<Q,+,== >   : Q a;       a+Q() == a
+Commutativity<Q,+,== >: Q a,b;       a+b == b+a
 
-Associativity<Q,*,== >: Q a,b,c: a*(b*c) ==(a*b)*c
-Commutativity<Q,*,== >: Q a,b:       a*b == b*a
+Associativity<Q,*,== >: Q a,b,c; a*(b*c) ==(a*b)*c
+Commutativity<Q,*,== >: Q a,b;       a*b == b*a
 
-RightNeutrality<Q,-,== >  : Q a:   a-Q() ==  a
-SelfRemovability<Q,-,=v= >: Q a:   a - a =v= Q()
+RightNeutrality<Q,-,== >  : Q a;   a-Q() ==  a
+SelfRemovability<Q,-,=v= >: Q a;   a - a =v= Q()
 ``
 
 For a `Quantifier` the same basic laws apply that are
@@ -647,16 +647,62 @@
 `Qunatifiers` and the 
 modified `operator *`.
 ``
-SymmetricDifference<Q,== > : Q a,b,c: (a + b) - (a * b) == (a - b) + (b - a)
+SymmetricDifference<Q,== > : Q a,b,c; (a + b) - (a * b) == (a - b) + (b - a)
 ``
 For a `TotalQuantifier` `Qt` symmetrical difference degenerates to 
 a trivial form since `operator *` and `operator +` become identical
 ``
-SymmetricDifference<Qt,== > : Qt a,b,c: (a + b) - (a + b) == (a - b) + (b - a) == 0
+SymmetricDifference<Qt,== > : Qt a,b,c; (a + b) - (a + b) == (a - b) + (b - a) == 0
 ``
 
+[h5 Existence of an Inverse]
 
+By now Quantifiers `Q` are 
+commutative monoids 
+with respect to the
+operation `+` and the neutral element Q(). 
+If the Quantifiers `CodomainT` type has an /inverse element/ 
+like e.g. signed numbers do,
+the `CodomainT` type is a 
+commutative or abelian group.
+In this case a `TotalQuantifier` also has an 
+inverse and the following law holds:
 
+``
+InverseElement<Qt,== > : Qt a; (0 - a) + a == 0
+``
+
+Which means that each `TotalQuantifier` over an
+abelian group is an 
+abelian group 
+itself.
+
+This also implies that a `Quantifier` of `Quantifiers` 
+is again a `Quantifiers` and a
+`TotalQuantifier` of `TotalQuantifiers`
+is also a `TotalQuantifier`. 
+
+`TotalQuantifiers` resemble the notion of a
+vector space partially.
+The concept could be completed to a vector space, 
+if a scalar multiplication was added. 
 [endsect][/ Quantifiers]
 
+
+[section Concept Induction]
+
+Obviously we can observe the induction of semantics
+from the `CodomainT` parameter into the instantiations
+of itl maps.
+
+[table
+[[]                          [is model of]        [if]                       [example]]
+[[`Map<D,Monoid>`]           [`Modoid`]           []                         [`interval_map<int,string>`]]
+[[`Map<D,Set,Trait>`]        [`Set`]              [`Trait::absorbs_neutrons`][`interval_map<int,itl::set<int> >`]]
+[[`Map<D,CommutativeMonoid>`][`CommutativeMonoid`][]                         [`interval_map<int,unsigned int>`]]
+[[`Map<D,CommutativeGroup>`] [`CommutativeGroup`] [`Trait::emits_neutrons`]  [`interval_map<int,int,neutron_emitter>`]]
+]
+
+[endsect][/ Concept Induction]
+
 [endsect][/ Semantics]

Modified: sandbox/itl/libs/validate/example/labat_single/labat_single.cpp
==============================================================================
--- sandbox/itl/libs/validate/example/labat_single/labat_single.cpp	(original)
+++ sandbox/itl/libs/validate/example/labat_single/labat_single.cpp	2009-01-12 05:45:08 EST (Mon, 12 Jan 2009)
@@ -79,10 +79,10 @@
         //LawValidater<TestLawT, RandomGentor> test_law;
         //test_law.setTrialsCount(1000);
 
-	//typedef InplaceInverseRemovability
-	//   <split_interval_map<int, int, neutron_enricher>, inplace_plus>  TestLawT;
-	//LawValidater<TestLawT, RandomGentor> test_law;
-	//test_law.setTrialsCount(1000);
+	typedef InplaceInverseRemovability
+	   <split_interval_map<int, int, neutron_emitter>, inplace_plus>  TestLawT;
+	LawValidater<TestLawT, RandomGentor> test_law;
+	test_law.setTrialsCount(1000);
 
         std::cout << "Start\n";
         ptime start(microsec_clock::local_time());