| CommonFloatSequence |
Represents sequences of double values that contain a common subset.
|
| CommonSequence |
Represents sequences of long values that contain a common subset.
|
| EltLowerBound |
Represents the invariant that each element of a sequence of long values is greater than or
equal to a constant.
|
| EltLowerBoundFloat |
Represents the invariant that each element of a sequence of double values is greater than or
equal to a constant.
|
| EltNonZero |
Represents the invariant "x !
|
| EltNonZeroFloat |
Represents the invariant "x !
|
| EltOneOf |
Represents sequences of long values where the elements of the sequence take on only a
few distinct values.
|
| EltOneOfFloat |
Represents sequences of double values where the elements of the sequence take on only a
few distinct values.
|
| EltRangeFloat |
Baseclass for unary range based invariants.
|
| EltRangeFloat.EqualMinusOne |
Internal invariant representing double scalars that are equal to minus one.
|
| EltRangeFloat.EqualOne |
Internal invariant representing double scalars that are equal to one.
|
| EltRangeFloat.EqualZero |
Internal invariant representing double scalars that are equal to zero.
|
| EltRangeFloat.GreaterEqual64 |
Internal invariant representing double scalars that are greater than or equal to 64.
|
| EltRangeFloat.GreaterEqualZero |
Internal invariant representing double scalars that are greater than or equal to 0.
|
| EltRangeInt |
Baseclass for unary range based invariants.
|
| EltRangeInt.BooleanVal |
Internal invariant representing longs whose values are always 0 or 1.
|
| EltRangeInt.Bound0_63 |
Internal invariant representing longs whose values are between 0 and 63.
|
| EltRangeInt.EqualMinusOne |
Internal invariant representing long scalars that are equal to minus one.
|
| EltRangeInt.EqualOne |
Internal invariant representing long scalars that are equal to one.
|
| EltRangeInt.EqualZero |
Internal invariant representing long scalars that are equal to zero.
|
| EltRangeInt.Even |
Invariant representing longs whose values are always even.
|
| EltRangeInt.GreaterEqual64 |
Internal invariant representing long scalars that are greater than or equal to 64.
|
| EltRangeInt.GreaterEqualZero |
Internal invariant representing long scalars that are greater than or equal to 0.
|
| EltRangeInt.PowerOfTwo |
Invariant representing longs whose values are always a power of 2 (exactly one bit is set).
|
| EltUpperBound |
Represents the invariant that each element of a sequence of long values is less than or
equal to a constant.
|
| EltUpperBoundFloat |
Represents the invariant that each element of a sequence of double values is less than or
equal to a constant.
|
| EltwiseFloatComparison |
Abstract base class defined so that the different types of EltwiseIntComparison (and separately
EltwiseFloatComparison), at the current moment those are ==, !
|
| EltwiseFloatEqual |
Represents equality between adjacent elements (x[i], x[i+1]) of a double sequence.
|
| EltwiseFloatGreaterEqual |
Represents the invariant ≥ between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
| EltwiseFloatGreaterThan |
Represents the invariant > between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
| EltwiseFloatLessEqual |
Represents the invariant ≤ between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
| EltwiseFloatLessThan |
Represents the invariant < between adjacent elements
(x[i], x[i+1]) of a double sequence.
|
| EltwiseIntComparison |
Abstract base class defined so that the different types of EltwiseIntComparison (and separately
EltwiseFloatComparison), at the current moment those are ==, !
|
| EltwiseIntEqual |
Represents equality between adjacent elements (x[i], x[i+1]) of a long sequence.
|
| EltwiseIntGreaterEqual |
Represents the invariant ≥ between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
| EltwiseIntGreaterThan |
Represents the invariant > between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
| EltwiseIntLessEqual |
Represents the invariant ≤ between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
| EltwiseIntLessThan |
Represents the invariant < between adjacent elements
(x[i], x[i+1]) of a long sequence.
|
| NoDuplicates |
Represents sequences of long that contain no duplicate elements.
|
| NoDuplicatesFloat |
Represents sequences of double that contain no duplicate elements.
|
| OneOfFloatSequence |
Represents double[] variables that take on only a few distinct values.
|
| OneOfSequence |
Represents long[] variables that take on only a few distinct values.
|
| SeqIndexFloatEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
| SeqIndexFloatGreaterEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
| SeqIndexFloatGreaterThan |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
| SeqIndexFloatLessEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
| SeqIndexFloatLessThan |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
| SeqIndexFloatNonEqual |
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself.
|
| SeqIndexIntEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
| SeqIndexIntGreaterEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
| SeqIndexIntGreaterThan |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
| SeqIndexIntLessEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
| SeqIndexIntLessThan |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
| SeqIndexIntNonEqual |
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself.
|
| SingleFloatSequence |
Abstract base class for invariants over one variable of type double[].
|
| SingleScalarSequence |
Abstract base class for invariants over one variable of type long[].
|
| SingleSequence |
Invariants on a single sequence (array) variable, such as a[] contains no duplicates.
|