Class  Description 

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