Accurate Numeric Operations

When the Accurate numeric operations control in the MrSpidey Analysis preferences window is turned on, MrSpidey performs a more accurate analysis of numeric operations, as follows.

The type language is extended with the unary constructors apply+, apply-, apply* and apply/. The return type of the numeric operations +, -, *, and / record information about the numeric operation and its argument value sets. For example, the type returned by the operation + is (apply+ arglist), where arglist is the argument list to +. The resulting types are simplified before being presented to the programmer. For example, type (apply+ (list x1 ... xn)) is transformed into (+ x1 ... xn), etc.

In addition, the binary constructors =, not=, <, <=, > and >= are added to the type language. The meaning of the type (< X Y) is the set of numbers x in X such that there exists some y in Y with x<y. MrSpidey generates these types for if-expressions where the predicate is one of zero?, =, <, <=, > or >=.