diff --git a/LessThanComparable.html b/LessThanComparable.html new file mode 100644 index 0000000..294101c --- /dev/null +++ b/LessThanComparable.html @@ -0,0 +1,212 @@ + + + +
++X + | ++A type that is a model of LessThanComparable + | +
+x, y, z + | ++Object of type X + | +
+If operator< is a strict weak ordering, and if each equivalence class +has only a single element, then operator< is a total ordering. +
+Name + | ++Expression + | ++Type requirements + | ++Return type + | +
---|---|---|---|
+Less + | ++x < y + | ++ + | ++Convertible to bool + | +
+Name + | ++Expression + | ++Precondition + | ++Semantics + | ++Postcondition + | +
---|---|---|---|---|
+Less + | ++x < y + | ++x and y are in the domain of < + | ++ + | +
+Irreflexivity + | ++x < x must be false. + | +
+Antisymmetry + | ++x < y implies !(y < x) [2] + | +
+Transitivity + | ++x < y and y < z implies x < z [3] + | +
[1] +Only operator< is fundamental; the other inequality operators +are essentially syntactic sugar. +
[2] +Antisymmetry is a theorem, not an axiom: it follows from +irreflexivity and transitivity. +
[3] +Because of irreflexivity and transitivity, operator< always +satisfies the definition of a partial ordering. The definition of +a strict weak ordering is stricter, and the definition of a +total ordering is stricter still. +
Copyright © 2000 | +Jeremy Siek, Univ.of Notre Dame (jsiek@lsc.nd.edu) + |