|
Class Summary |
| 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 used to evaluate single double sequences. |
| SingleScalarSequence |
Abstract base class used to evaluate single long sequences. |
| SingleSequence |
Invariants on a single sequence. |