LessThanComparable

Description

A type is LessThanComparable if it is ordered: it must be possible to compare two objects of that type using operator<, and operator< must be a strict weak ordering relation.

Refinement of

Associated types

Notation

`X`	A type that is a model of LessThanComparable
`x`, `y`, `z`	Object of type `X`

Definitions

Consider the relation !(x < y) && !(y < x). If this relation is transitive (that is, if !(x < y) && !(y < x) && !(y < z) && !(z < y) implies !(x < z) && !(z < x)), then it satisfies the mathematical definition of an equivalence relation. In this case, operator< is a strict weak ordering.

If operator< is a strict weak ordering, and if each equivalence class has only a single element, then operator< is a total ordering.

Valid expressions

Name	Expression	Type requirements	Return type
Less	`x < y`		Convertible to `bool`

Expression semantics

Name	Expression	Precondition	Semantics	Postcondition
Less	`x < y`	`x` and `y` are in the domain of `<`

Complexity guarantees

Invariants

Irreflexivity	`x < x` must be false.
Antisymmetry	`x < y` implies !(y < x) [2]
Transitivity	`x < y` and `y < z` implies `x < z` [3]

Models

Notes

[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.