1<html> 2<head> 3<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> 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.79.1"> 7<link rel="home" href="../index.html" title="Chapter 1. Boost.Icl"> 8<link rel="up" href="../index.html" title="Chapter 1. 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"> 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 class="toc"> 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 <span class="quote">“<span class="quote">Beauty is the ultimate defense against complexity</span>”</span> -- <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"><</span><span class="identifier">T</span><span class="special">,+>:</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"> 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<h5> 75<a name="boost_icl.semantics.orderings_and_equivalences.h0"></a> 76 <span class="phrase"><a name="boost_icl.semantics.orderings_and_equivalences.lexicographical_ordering_and_equality"></a></span><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"><</span></code> that implements a <a href="https://boost.org/sgi/stl/StrictWeakOrdering.html" target="_top">strict 82 weak ordering</a>. The semantics of <code class="computeroutput"><span class="keyword">operator</span> 83 <span class="special"><</span></code> is the same as for an stl's 84 <a href="https://boost.org/sgi/stl/SortedAssociativeContainer.html" target="_top">SortedAssociativeContainer</a>, 85 specifically <a href="https://boost.org/sgi/stl/set.html" target="_top">stl::set</a> 86 and <a href="https://boost.org/sgi/stl/Map.html" target="_top">stl::map</a>: 87</p> 88<pre class="programlisting"><span class="identifier">Irreflexivity</span><span class="special"><</span><span class="identifier">T</span><span class="special">,<</span> <span class="special">></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"><</span><span class="identifier">a</span><span class="special">)</span> 89<span class="identifier">Asymmetry</span><span class="special"><</span><span class="identifier">T</span><span class="special">,<</span> <span class="special">></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"><</span><span class="identifier">b</span> <span class="identifier">implies</span> <span class="special">!(</span><span class="identifier">b</span><span class="special"><</span><span class="identifier">a</span><span class="special">)</span> 90<span class="identifier">Transitivity</span><span class="special"><</span><span class="identifier">T</span><span class="special">,<</span> <span class="special">></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"><</span><span class="identifier">b</span> <span class="special">&&</span> <span class="identifier">b</span><span class="special"><</span><span class="identifier">c</span> <span class="identifier">implies</span> <span class="identifier">a</span><span class="special"><</span><span class="identifier">c</span> 91</pre> 92<p> 93 </p> 94<p> 95 <code class="computeroutput"><span class="identifier">Operator</span> <span class="special"><</span></code> 96 depends on the icl::container's template parameter <code class="computeroutput"><span class="identifier">Compare</span></code> 97 that implements a <span class="emphasis"><em>strict weak ordering</em></span> for the container's 98 <code class="computeroutput"><span class="identifier">domain_type</span></code>. For a given 99 <code class="computeroutput"><span class="identifier">Compare</span></code> ordering, <code class="computeroutput"><span class="keyword">operator</span> <span class="special"><</span></code> 100 implements a lexicographical comparison on icl::containers, that uses the 101 <code class="computeroutput"><span class="identifier">Compare</span></code> order to establish 102 a unique sequence of values in the container. 103 </p> 104<p> 105 The induced equivalence of <code class="computeroutput"><span class="keyword">operator</span> 106 <span class="special"><</span></code> is lexicographical equality which 107 is implemented as <code class="computeroutput"><span class="keyword">operator</span> <span class="special">==</span></code>. 108</p> 109<pre class="programlisting"><span class="comment">//equivalence induced by strict weak ordering <</span> 110<span class="special">!(</span><span class="identifier">a</span><span class="special"><</span><span class="identifier">b</span><span class="special">)</span> <span class="special">&&</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">implies</span> <span class="identifier">a</span> <span class="special">==</span> <span class="identifier">b</span><span class="special">;</span> 111</pre> 112<p> 113 Again this follows the semantics of the <span class="bold"><strong>stl</strong></span>. 114 Lexicographical equality is stronger than the equality of elements. Two containers 115 that contain the same elements can be lexicographically unequal, if their 116 elements are differently sorted. Lexicographical comparison belongs to the 117 <span class="emphasis"><em><span class="bold"><strong>segmental</strong></span></em></span> aspect. Of 118 all the different sequences that are valid for unordered sets and maps, one 119 such sequence is selected by the <code class="computeroutput"><span class="identifier">Compare</span></code> 120 order of elements. Based on this selection a unique iteration is possible. 121 </p> 122<h5> 123<a name="boost_icl.semantics.orderings_and_equivalences.h1"></a> 124 <span class="phrase"><a name="boost_icl.semantics.orderings_and_equivalences.subset_ordering_and_element_equality"></a></span><a class="link" href="semantics.html#boost_icl.semantics.orderings_and_equivalences.subset_ordering_and_element_equality">Subset 125 Ordering and Element Equality</a> 126 </h5> 127<p> 128 On the fundamental aspect only membership of elements matters, not their 129 sequence. So there are functions <code class="computeroutput"><span class="identifier">contained_in</span></code> 130 and <code class="computeroutput"><span class="identifier">element_equal</span></code> that implement 131 the subset relation and the equality on elements. Yet, <code class="computeroutput"><span class="identifier">contained_in</span></code> 132 and <code class="computeroutput"><span class="identifier">is_element_equal</span></code> functions 133 are not really working on the level of elements. They also work on the basis 134 of the containers templates <code class="computeroutput"><span class="identifier">Compare</span></code> 135 parameter. In practical terms we need to distinguish between lexicographical 136 equality <code class="computeroutput"><span class="keyword">operator</span> <span class="special">==</span></code> 137 and equality of elements <code class="computeroutput"><span class="identifier">is_element_equal</span></code>, 138 if we work with interval splitting interval containers: 139</p> 140<pre class="programlisting"><span class="identifier">split_interval_set</span><span class="special"><</span><span class="identifier">time</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">//Pseudocode</span> 141<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</span> 142<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.</span> 143<span class="identifier">w1</span> <span class="special">==</span> <span class="identifier">w2</span><span class="special">;</span> <span class="comment">//false: Different segmentation</span> 144<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 </span> 145</pre> 146<p> 147 </p> 148<p> 149 For a constant <code class="computeroutput"><span class="identifier">Compare</span></code> order 150 on key elements, member function <code class="computeroutput"><span class="identifier">contained_in</span></code> 151 that is defined for all icl::containers implements a <a href="http://en.wikipedia.org/wiki/Partially_ordered_set" target="_top">partial 152 order</a> on icl::containers. 153 </p> 154<p> 155</p> 156<pre class="programlisting"><span class="identifier">with</span> <span class="special"><=</span> <span class="keyword">for</span> <span class="identifier">contained_in</span><span class="special">,</span> 157 <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> 158<span class="identifier">Reflexivity</span><span class="special"><</span><span class="identifier">T</span><span class="special">,<=</span> <span class="special">></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"><=</span> <span class="identifier">a</span> 159<span class="identifier">Antisymmetry</span><span class="special"><</span><span class="identifier">T</span><span class="special">,<=,=</span><span class="identifier">e</span><span class="special">=></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"><=</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="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> 160<span class="identifier">Transitivity</span><span class="special"><</span><span class="identifier">T</span><span class="special">,<=</span> <span class="special">></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"><=</span> <span class="identifier">b</span> <span class="special">&&</span> <span class="identifier">b</span> <span class="special"><=</span> <span class="identifier">c</span> <span class="identifier">implies</span> <span class="identifier">a</span> <span class="special"><=</span> <span class="identifier">c</span> 161</pre> 162<p> 163 </p> 164<p> 165 The induced equivalence is the equality of elements that is implemented via 166 function <code class="computeroutput"><span class="identifier">is_element_equal</span></code>. 167</p> 168<pre class="programlisting"><span class="comment">//equivalence induced by the partial ordering contained_in on icl::container a,b</span> 169<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">&&</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> 170</pre> 171<p> 172 </p> 173</div> 174</div> 175<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr> 176<td align="left"></td> 177<td align="right"><div class="copyright-footer">Copyright © 2007-2010 Joachim 178 Faulhaber<br>Copyright © 1999-2006 Cortex Software 179 GmbH<p> 180 Distributed under the Boost Software License, Version 1.0. (See accompanying 181 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>) 182 </p> 183</div></td> 184</tr></table> 185<hr> 186<div class="spirit-nav"> 187<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> 188</div> 189</body> 190</html> 191
