|
Class Summary |
| 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 two variable long[] invariants. |
| TwoSequenceFloat |
Base class for two variable double[] invariants. |
| TwoSequenceString |
Base class for two variable String[] invariants. |