libs/icl/doc/html/boost_icl/semantics.html

   1 <html>
   2 <head>
   3 <meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
   4 <title>Semantics</title>
   5 <link rel="stylesheet" href="../../../../../doc/src/boostbook.css" type="text/css">
   6 <meta name="generator" content="DocBook XSL Stylesheets V1.74.0">
   7 <link rel="home" href="../index.html" title="Chapter&#160;1.&#160;Boost.Icl">
   8 <link rel="up" href="../index.html" title="Chapter&#160;1.&#160;Boost.Icl">
   9 <link rel="prev" href="concepts/map_traits.html" title="Map Traits">
  10 <link rel="next" href="semantics/sets.html" title="Sets">
  11 </head>
  12 <body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
  13 <table cellpadding="2" width="100%"><tr>
  14 <td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../../boost.png"></td>
  15 <td align="center"><a href="../../../../../index.html">Home</a></td>
  16 <td align="center"><a href="../../../../libraries.htm">Libraries</a></td>
  17 <td align="center"><a href="http://www.boost.org/users/people.html">People</a></td>
  18 <td align="center"><a href="http://www.boost.org/users/faq.html">FAQ</a></td>
  19 <td align="center"><a href="../../../../../more/index.htm">More</a></td>
  20 </tr></table>
  21 <hr>
  22 <div class="spirit-nav">
  23 <a accesskey="p" href="concepts/map_traits.html"><img src="../../../../../doc/src/images/prev.png" alt="Prev"></a><a accesskey="u" href="../index.html"><img src="../../../../../doc/src/images/up.png" alt="Up"></a><a accesskey="h" href="../index.html"><img src="../../../../../doc/src/images/home.png" alt="Home"></a><a accesskey="n" href="semantics/sets.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
  24 </div>
  25 <div class="section" lang="en">
  26 <div class="titlepage"><div><div><h2 class="title" style="clear: both">
  27 <a name="boost_icl.semantics"></a><a class="link" href="semantics.html" title="Semantics">Semantics</a>
  28 </h2></div></div></div>
  29 <div class="toc"><dl>
  30 <dt><span class="section"><a href="semantics.html#boost_icl.semantics.orderings_and_equivalences">Orderings
  31       and Equivalences</a></span></dt>
  32 <dt><span class="section"><a href="semantics/sets.html">Sets</a></span></dt>
  33 <dt><span class="section"><a href="semantics/maps.html">Maps</a></span></dt>
  34 <dt><span class="section"><a href="semantics/collectors__maps_of_sets.html">Collectors:
  35       Maps of Sets</a></span></dt>
  36 <dt><span class="section"><a href="semantics/quantifiers__maps_of_numbers.html">Quantifiers:
  37       Maps of Numbers</a></span></dt>
  38 <dt><span class="section"><a href="semantics/concept_induction.html">Concept Induction</a></span></dt>
  39 </dl></div>
  40 <p>
  41       &#8220;<span class="quote">Beauty is the ultimate defense against complexity</span>&#8221; -- <a href="http://en.wikipedia.org/wiki/David_Gelernter" target="_top">David Gelernter</a>
  42     </p>
  43 <p>
  44       In the <span class="bold"><strong>icl</strong></span> we follow the notion, that the
  45       semantics of a <span class="emphasis"><em><span class="bold"><strong>concept</strong></span></em></span>
  46       or <span class="emphasis"><em><span class="bold"><strong>abstract data type</strong></span></em></span>
  47       can be expressed by <span class="emphasis"><em><span class="bold"><strong>laws</strong></span></em></span>.
  48       We formulate laws over interval containers that can be evaluated for a given
  49       instantiation of the variables contained in the law. The following pseudocode
  50       gives a shorthand notation of such a law.
  51 </p>
  52 <pre class="programlisting"><span class="identifier">Commutativity</span><span class="special">&lt;</span><span class="identifier">T</span><span class="special">,+&gt;:</span>
  53 <span class="identifier">T</span> <span class="identifier">a</span><span class="special">,</span> <span class="identifier">b</span><span class="special">;</span> <span class="identifier">a</span> <span class="special">+</span> <span class="identifier">b</span> <span class="special">==</span> <span class="identifier">b</span> <span class="special">+</span> <span class="identifier">a</span><span class="special">;</span>
  54 </pre>
  55 <p>
  56       This can of course be coded as a proper c++ class template which has been done
  57       for the validation of the <span class="bold"><strong>icl</strong></span>. For sake of
  58       simplicity we will use pseudocode here.
  59     </p>
  60 <p>
  61       The laws that describe the semantics of the <span class="bold"><strong>icl's</strong></span>
  62       class templates were validated using the Law based Test Automaton <span class="emphasis"><em><span class="bold"><strong>LaBatea</strong></span></em></span>, a tool that generates instances
  63       for the law's variables and then tests it's validity. Since the <span class="bold"><strong>icl</strong></span>
  64       deals with sets, maps and relations, that are well known objects from mathematics,
  65       the laws that we are using are mostly <span class="emphasis"><em>recycled</em></span> ones. Also
  66       some of those laws are grouped in notions like e.g. <span class="emphasis"><em>orderings</em></span>
  67       or <span class="emphasis"><em>algebras</em></span>.
  68     </p>
  69 <div class="section" lang="en">
  70 <div class="titlepage"><div><div><h3 class="title">
  71 <a name="boost_icl.semantics.orderings_and_equivalences"></a><a class="link" href="semantics.html#boost_icl.semantics.orderings_and_equivalences" title="Orderings and Equivalences">Orderings
  72       and Equivalences</a>
  73 </h3></div></div></div>
  74 <a name="boost_icl.semantics.orderings_and_equivalences.lexicographical_ordering_and_equality"></a><h5>
  75 <a name="id1078610"></a>
  76         <a class="link" href="semantics.html#boost_icl.semantics.orderings_and_equivalences.lexicographical_ordering_and_equality">Lexicographical
  77         Ordering and Equality</a>
  78       </h5>
  79 <p>
  80         On all set and map containers of the icl, there is an <code class="computeroutput"><span class="keyword">operator</span>
  81         <span class="special">&lt;</span></code> that implements a <a href="http://www.sgi.com/tech/stl/StrictWeakOrdering.html" target="_top">strict
  82         weak ordering</a>.
  83       </p>
  84 <p>
  85         The semantics of <code class="computeroutput"><span class="keyword">operator</span> <span class="special">&lt;</span></code>
  86         is the same as for an stl's <a href="http://www.sgi.com/tech/stl/SortedAssociativeContainer.html" target="_top">SortedAssociativeContainer</a>,
  87         specifically <a href="http://www.sgi.com/tech/stl/set.html" target="_top">stl::set</a>
  88         and <a href="http://www.sgi.com/tech/stl/map.html" target="_top">stl::map</a>:
  89 </p>
  90 <pre class="programlisting"><span class="identifier">Irreflexivity</span><span class="special">&lt;</span><span class="identifier">T</span><span class="special">,&lt;</span> <span class="special">&gt;</span> <span class="special">:</span> <span class="identifier">T</span> <span class="identifier">a</span><span class="special">;</span>     <span class="special">!(</span><span class="identifier">a</span><span class="special">&lt;</span><span class="identifier">a</span><span class="special">)</span>
  91 <span class="identifier">Asymmetry</span><span class="special">&lt;</span><span class="identifier">T</span><span class="special">,&lt;</span> <span class="special">&gt;</span>     <span class="special">:</span> <span class="identifier">T</span> <span class="identifier">a</span><span class="special">,</span><span class="identifier">b</span><span class="special">;</span>   <span class="identifier">a</span><span class="special">&lt;</span><span class="identifier">b</span> <span class="identifier">implies</span> <span class="special">!(</span><span class="identifier">b</span><span class="special">&lt;</span><span class="identifier">a</span><span class="special">)</span>
  92 <span class="identifier">Transitivity</span><span class="special">&lt;</span><span class="identifier">T</span><span class="special">,&lt;</span> <span class="special">&gt;</span>  <span class="special">:</span> <span class="identifier">T</span> <span class="identifier">a</span><span class="special">,</span><span class="identifier">b</span><span class="special">,</span><span class="identifier">c</span><span class="special">;</span> <span class="identifier">a</span><span class="special">&lt;</span><span class="identifier">b</span> <span class="special">&amp;&amp;</span> <span class="identifier">b</span><span class="special">&lt;</span><span class="identifier">c</span> <span class="identifier">implies</span> <span class="identifier">a</span><span class="special">&lt;</span><span class="identifier">c</span>
  93 </pre>
  94 <p>
  95       </p>
  96 <p>
  97         <code class="computeroutput"><span class="identifier">Operator</span> <span class="special">&lt;</span></code>
  98         depends on the icl::container's template parameter <code class="computeroutput"><span class="identifier">Compare</span></code>
  99         that implements a <span class="emphasis"><em>strict weak ordering</em></span> for the container's
 100         <code class="computeroutput"><span class="identifier">domain_type</span></code>. For a given
 101         <code class="computeroutput"><span class="identifier">Compare</span></code> ordering, <code class="computeroutput"><span class="keyword">operator</span> <span class="special">&lt;</span></code>
 102         implements a lexicographical comparison on icl::containers, that uses the
 103         <code class="computeroutput"><span class="identifier">Compare</span></code> order to establish
 104         a unique sequence of values in the container.
 105       </p>
 106 <p>
 107         The induced equivalence of <code class="computeroutput"><span class="keyword">operator</span>
 108         <span class="special">&lt;</span></code> is lexicographical equality which
 109         is implemented as <code class="computeroutput"><span class="keyword">operator</span> <span class="special">==</span></code>.
 110 </p>
 111 <pre class="programlisting"><span class="comment">//equivalence induced by strict weak ordering &lt;
 112 </span><span class="special">!(</span><span class="identifier">a</span><span class="special">&lt;</span><span class="identifier">b</span><span class="special">)</span> <span class="special">&amp;&amp;</span> <span class="special">!(</span><span class="identifier">b</span><span class="special">&lt;</span><span class="identifier">a</span><span class="special">)</span> <span class="identifier">implies</span> <span class="identifier">a</span> <span class="special">==</span> <span class="identifier">b</span><span class="special">;</span>
 113 </pre>
 114 <p>
 115         Again this follows the semantics of the <span class="bold"><strong>stl</strong></span>.
 116         Lexicographical equality is stronger than the equality of elements. Two containers
 117         that contain the same elements can be lexicographically unequal, if their
 118         elements are differently sorted. Lexicographical comparison belongs to the
 119         <span class="emphasis"><em><span class="bold"><strong>segmental</strong></span></em></span> aspect. Of
 120         all the different sequences that are valid for unordered sets and maps, one
 121         such sequence is selected by the <code class="computeroutput"><span class="identifier">Compare</span></code>
 122         order of elements. Based on this selection a unique iteration is possible.
 123       </p>
 124 <a name="boost_icl.semantics.orderings_and_equivalences.subset_ordering_and_element_equality"></a><h5>
 125 <a name="id1079099"></a>
 126         <a class="link" href="semantics.html#boost_icl.semantics.orderings_and_equivalences.subset_ordering_and_element_equality">Subset
 127         Ordering and Element Equality</a>
 128       </h5>
 129 <p>
 130         On the fundamental aspect only membership of elements matters, not their
 131         sequence. So there are functions <code class="computeroutput"><span class="identifier">contained_in</span></code>
 132         and <code class="computeroutput"><span class="identifier">element_equal</span></code> that implement
 133         the subset relation and the equality on elements. Yet, <code class="computeroutput"><span class="identifier">contained_in</span></code>
 134         and <code class="computeroutput"><span class="identifier">is_element_equal</span></code> functions
 135         are not really working on the level of elements. They also work on the basis
 136         of the containers templates <code class="computeroutput"><span class="identifier">Compare</span></code>
 137         parameter. In practical terms we need to distinguish between lexicographical
 138         equality <code class="computeroutput"><span class="keyword">operator</span> <span class="special">==</span></code>
 139         and equality of elements <code class="computeroutput"><span class="identifier">is_element_equal</span></code>,
 140         if we work with interval splitting interval containers:
 141 </p>
 142 <pre class="programlisting"><span class="identifier">split_interval_set</span><span class="special">&lt;</span><span class="identifier">time</span><span class="special">&gt;</span> <span class="identifier">w1</span><span class="special">,</span> <span class="identifier">w2</span><span class="special">;</span> <span class="comment">//Pseudocode
 143 </span><span class="identifier">w1</span> <span class="special">=</span> <span class="special">{[</span><span class="identifier">Mon</span>       <span class="special">..</span>       <span class="identifier">Sun</span><span class="special">)};</span> <span class="comment">//split_interval_set containing a week
 144 </span><span class="identifier">w2</span> <span class="special">=</span> <span class="special">{[</span><span class="identifier">Mon</span> <span class="special">..</span> <span class="identifier">Fri</span><span class="special">)[</span><span class="identifier">Sat</span> <span class="special">..</span> <span class="identifier">Sun</span><span class="special">)};</span> <span class="comment">//Same week split in work and week end parts.
 145 </span><span class="identifier">w1</span> <span class="special">==</span> <span class="identifier">w2</span><span class="special">;</span>                        <span class="comment">//false: Different segmentation
 146 </span><span class="identifier">is_element_equal</span><span class="special">(</span><span class="identifier">w1</span><span class="special">,</span><span class="identifier">w2</span><span class="special">);</span>         <span class="comment">//true:  Same elements contained
 147 </span></pre>
 148 <p>
 149       </p>
 150 <p>
 151         For a constant <code class="computeroutput"><span class="identifier">Compare</span></code> order
 152         on key elements, member function <code class="computeroutput"><span class="identifier">contained_in</span></code>
 153         that is defined for all icl::containers implements a <a href="http://en.wikipedia.org/wiki/Partially_ordered_set" target="_top">partial
 154         order</a> on icl::containers.
 155       </p>
 156 <p>
 157
 158 </p>
 159 <pre class="programlisting"><span class="identifier">with</span> <span class="special">&lt;=</span> <span class="keyword">for</span> <span class="identifier">contained_in</span><span class="special">,</span>
 160     <span class="special">=</span><span class="identifier">e</span><span class="special">=</span> <span class="keyword">for</span> <span class="identifier">is_element_equal</span><span class="special">:</span>
 161 <span class="identifier">Reflexivity</span><span class="special">&lt;</span><span class="identifier">T</span><span class="special">,&lt;=</span> <span class="special">&gt;</span>     <span class="special">:</span> <span class="identifier">T</span> <span class="identifier">a</span><span class="special">;</span>     <span class="identifier">a</span> <span class="special">&lt;=</span> <span class="identifier">a</span>
 162 <span class="identifier">Antisymmetry</span><span class="special">&lt;</span><span class="identifier">T</span><span class="special">,&lt;=,=</span><span class="identifier">e</span><span class="special">=&gt;</span> <span class="special">:</span> <span class="identifier">T</span> <span class="identifier">a</span><span class="special">,</span><span class="identifier">b</span><span class="special">;</span>   <span class="identifier">a</span> <span class="special">&lt;=</span> <span class="identifier">b</span> <span class="special">&amp;&amp;</span> <span class="identifier">b</span> <span class="special">&lt;=</span> <span class="identifier">a</span> <span class="identifier">implies</span> <span class="identifier">a</span> <span class="special">=</span><span class="identifier">e</span><span class="special">=</span> <span class="identifier">b</span>
 163 <span class="identifier">Transitivity</span><span class="special">&lt;</span><span class="identifier">T</span><span class="special">,&lt;=</span> <span class="special">&gt;</span>    <span class="special">:</span> <span class="identifier">T</span> <span class="identifier">a</span><span class="special">,</span><span class="identifier">b</span><span class="special">,</span><span class="identifier">c</span><span class="special">;</span> <span class="identifier">a</span> <span class="special">&lt;=</span> <span class="identifier">b</span> <span class="special">&amp;&amp;</span> <span class="identifier">b</span> <span class="special">&lt;=</span> <span class="identifier">c</span> <span class="identifier">implies</span> <span class="identifier">a</span> <span class="special">&lt;=</span> <span class="identifier">c</span>
 164 </pre>
 165 <p>
 166       </p>
 167 <p>
 168         The induced equivalence is the equality of elements that is implemented via
 169         function <code class="computeroutput"><span class="identifier">is_element_equal</span></code>.
 170
 171 </p>
 172 <pre class="programlisting"><span class="comment">//equivalence induced by the partial ordering contained_in on icl::container a,b
 173 </span><span class="identifier">a</span><span class="special">.</span><span class="identifier">contained_in</span><span class="special">(</span><span class="identifier">b</span><span class="special">)</span> <span class="special">&amp;&amp;</span> <span class="identifier">b</span><span class="special">.</span><span class="identifier">contained_in</span><span class="special">(</span><span class="identifier">a</span><span class="special">)</span> <span class="identifier">implies</span> <span class="identifier">is_element_equal</span><span class="special">(</span><span class="identifier">a</span><span class="special">,</span> <span class="identifier">b</span><span class="special">);</span>
 174 </pre>
 175 <p>
 176       </p>
 177 </div>
 178 </div>
 179 <table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
 180 <td align="left"></td>
 181 <td align="right"><div class="copyright-footer">Copyright &#169; 2007 -2010 Joachim Faulhaber<br>Copyright &#169; 1999 -2006 Cortex Software GmbH<p>
 182         Distributed under the Boost Software License, Version 1.0. (See accompanying
 183         file LICENSE_1_0.txt or copy at <a href="http://www.boost.org/LICENSE_1_0.txt" target="_top">http://www.boost.org/LICENSE_1_0.txt</a>)
 184       </p>
 185 </div></td>
 186 </tr></table>
 187 <hr>
 188 <div class="spirit-nav">
 189 <a accesskey="p" href="concepts/map_traits.html"><img src="../../../../../doc/src/images/prev.png" alt="Prev"></a><a accesskey="u" href="../index.html"><img src="../../../../../doc/src/images/up.png" alt="Up"></a><a accesskey="h" href="../index.html"><img src="../../../../../doc/src/images/home.png" alt="Home"></a><a accesskey="n" href="semantics/sets.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
 190 </div>
 191 </body>
 192 </html>