|
Class Summary |
| 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 two variable double invariants. |
| TwoScalar |
Base class for two variable long invariants. |