| PairwiseFloatEqual |
Represents an invariant between corresponding elements of two sequences of double values.
|
| PairwiseFloatGreaterEqual |
Represents an invariant between corresponding elements of two sequences of double values.
|
| PairwiseFloatGreaterThan |
Represents an invariant between corresponding elements of two sequences of double values.
|
| PairwiseFloatLessEqual |
Represents an invariant between corresponding elements of two sequences of double values.
|
| PairwiseFloatLessThan |
Represents an invariant between corresponding elements of two sequences of double values.
|
| PairwiseIntEqual |
Represents an invariant between corresponding elements of two sequences of long values.
|
| PairwiseIntGreaterEqual |
Represents an invariant between corresponding elements of two sequences of long values.
|
| PairwiseIntGreaterThan |
Represents an invariant between corresponding elements of two sequences of long values.
|
| PairwiseIntLessEqual |
Represents an invariant between corresponding elements of two sequences of long values.
|
| PairwiseIntLessThan |
Represents an invariant between corresponding elements of two sequences of long values.
|
| PairwiseLinearBinary |
Represents a linear invariant (i.e., y = ax + b) between the corresponding elements
of two sequences of long values.
|
| PairwiseLinearBinaryFloat |
Represents a linear invariant (i.e., y = ax + b) between the corresponding elements
of two sequences of double values.
|
| PairwiseNumericFloat |
Baseclass for binary numeric invariants.
|
| PairwiseNumericFloat.Divides |
Represents the divides without remainder invariant between corresponding elements of two sequences of double.
|
| PairwiseNumericFloat.Square |
Represents the square invariant between corresponding elements of two sequences of double.
|
| PairwiseNumericFloat.ZeroTrack |
Represents the zero tracks invariant between
corresponding elements of two sequences of double; that is, when x[] is zero,
y[] is also zero.
|
| PairwiseNumericInt |
Baseclass for binary numeric invariants.
|
| PairwiseNumericInt.BitwiseAndZero |
Represents the BitwiseAnd == 0 invariant between corresponding elements of two sequences of long; that is, x[] and
y[] have no bits in common.
|
| PairwiseNumericInt.BitwiseComplement |
Represents the bitwise complement invariant between corresponding elements of two sequences of long.
|
| PairwiseNumericInt.BitwiseSubset |
Represents the bitwise subset invariant between corresponding elements of two sequences of long; that is, the bits of
y[] are a subset of the bits of x[].
|
| PairwiseNumericInt.Divides |
Represents the divides without remainder invariant between corresponding elements of two sequences of long.
|
| PairwiseNumericInt.ShiftZero |
Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, x[]
right-shifted by y[] is always zero.
|
| PairwiseNumericInt.Square |
Represents the square invariant between corresponding elements of two sequences of long.
|
| PairwiseNumericInt.ZeroTrack |
Represents the zero tracks invariant between
corresponding elements of two sequences of long; that is, when x[] is zero,
y[] is also zero.
|
| PairwiseString |
Baseclass for binary numeric invariants.
|
| PairwiseString.SubString |
Represents the substring invariant between corresponding elements of two sequences of String.
|
| PairwiseStringEqual |
Represents an invariant between corresponding elements of two sequences of String values.
|
| PairwiseStringGreaterEqual |
Represents an invariant between corresponding elements of two sequences of String values.
|
| PairwiseStringGreaterThan |
Represents an invariant between corresponding elements of two sequences of String values.
|
| PairwiseStringLessEqual |
Represents an invariant between corresponding elements of two sequences of String values.
|
| PairwiseStringLessThan |
Represents an invariant between corresponding elements of two sequences of String values.
|
| Reverse |
Represents two sequences of long where one is in the reverse order of the other.
|
| ReverseFloat |
Represents two sequences of double where one is in the reverse order of the other.
|
| SeqSeqFloatEqual |
Represents invariants between two sequences of double values.
|
| SeqSeqFloatGreaterEqual |
Represents invariants between two sequences of double values.
|
| SeqSeqFloatGreaterThan |
Represents invariants between two sequences of double values.
|
| SeqSeqFloatLessEqual |
Represents invariants between two sequences of double values.
|
| SeqSeqFloatLessThan |
Represents invariants between two sequences of double values.
|
| SeqSeqIntEqual |
Represents invariants between two sequences of long values.
|
| SeqSeqIntGreaterEqual |
Represents invariants between two sequences of long values.
|
| SeqSeqIntGreaterThan |
Represents invariants between two sequences of long values.
|
| SeqSeqIntLessEqual |
Represents invariants between two sequences of long values.
|
| SeqSeqIntLessThan |
Represents invariants between two sequences of long values.
|
| SeqSeqStringEqual |
Represents invariants between two sequences of String values.
|
| SeqSeqStringGreaterEqual |
Represents invariants between two sequences of String values.
|
| SeqSeqStringGreaterThan |
Represents invariants between two sequences of String values.
|
| SeqSeqStringLessEqual |
Represents invariants between two sequences of String values.
|
| SeqSeqStringLessThan |
Represents invariants between two sequences of String values.
|
| SubSequence |
Represents two sequences of long values where one sequence is a subsequence of the
other.
|
| SubSequenceFloat |
Represents two sequences of double values where one sequence is a subsequence of the
other.
|
| SubSet |
Represents two sequences of long values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other.
|
| SubSetFloat |
Represents two sequences of double values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other.
|
| SuperSequence |
Represents two sequences of long values where one sequence is a subsequence of the
other.
|
| SuperSequenceFloat |
Represents two sequences of double values where one sequence is a subsequence of the
other.
|
| SuperSet |
Represents two sequences of long values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other.
|
| SuperSetFloat |
Represents two sequences of double values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other.
|
| TwoSequence |
Base class for invariants over two variables of type long[].
|
| TwoSequenceFloat |
Base class for invariants over two variables of type double[].
|
| TwoSequenceString |
Base class for invariants over two variables of type String[].
|