| FloatEqual |
Represents an invariant of == between two double scalars.
|
| FloatGreaterEqual |
Represents an invariant of ≥ between two double scalars.
|
| FloatGreaterThan |
Represents an invariant of > between two double scalars.
|
| FloatLessEqual |
Represents an invariant of ≤ between two double scalars.
|
| FloatLessThan |
Represents an invariant of < between two double scalars.
|
| FloatNonEqual |
Represents an invariant of !
|
| IntEqual |
Represents an invariant of == between two long scalars.
|
| IntGreaterEqual |
Represents an invariant of ≥ between two long scalars.
|
| IntGreaterThan |
Represents an invariant of > between two long scalars.
|
| IntLessEqual |
Represents an invariant of ≤ between two long scalars.
|
| IntLessThan |
Represents an invariant of < between two long scalars.
|
| IntNonEqual |
Represents an invariant of !
|
| LinearBinary |
Represents a Linear invariant between two long scalars x and y, of
the form ax + by + c = 0.
|
| LinearBinaryCore |
|
| LinearBinaryCoreFloat |
|
| LinearBinaryFloat |
Represents a Linear invariant between two double scalars x and y, of
the form ax + by + c = 0.
|
| NumericFloat |
Baseclass for binary numeric invariants.
|
| NumericFloat.Divides |
Represents the divides without remainder invariant between two double scalars.
|
| NumericFloat.Square |
Represents the square invariant between two double scalars.
|
| NumericFloat.ZeroTrack |
Represents the zero tracks invariant between
two double scalars; that is, when x is zero,
y is also zero.
|
| NumericInt |
Baseclass for binary numeric invariants.
|
| NumericInt.BitwiseAndZero |
Represents the BitwiseAnd == 0 invariant between two long scalars; that is, x and
y have no bits in common.
|
| NumericInt.BitwiseComplement |
Represents the bitwise complement invariant between two long scalars.
|
| NumericInt.BitwiseSubset |
Represents the bitwise subset invariant between two long scalars; that is, the bits of
y are a subset of the bits of x.
|
| NumericInt.Divides |
Represents the divides without remainder invariant between two long scalars.
|
| NumericInt.ShiftZero |
Represents the ShiftZero invariant between two long scalars; that is, x
right-shifted by y is always zero.
|
| NumericInt.Square |
Represents the square invariant between two long scalars.
|
| NumericInt.ZeroTrack |
Represents the zero tracks invariant between
two long scalars; that is, when x is zero,
y is also zero.
|
| TwoFloat |
Base class for invariants over two variables of type double.
|
| TwoScalar |
Base class for invariants over two variables of type long.
|