This package and its subpackages provide the "public interface" to SARL. The interfaces in these packages provide all the functionality that a typical user needs to know. The most important interface defined here is
SymbolicUniverse. To obtain an instance of a SymbolicUniverse, use one of the static methods in
SARL. In addition the types defined directly in this package, the public interface comprises the following subpackages:
ClassDescriptionA substituter used to assign new, canonical names to all symbolic constants occurring in a sequence of expressions.The result of analyzing certain "forall" expressions.A result to a validity query which also requested a model in case the answer was "NO", and for which the answer was "NO".Predicate<T>A Predicate on type T is an object that provides a method "apply" which takes an element of T and returns
false.A reasoner provides methods to simplify
SymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context".An exception that occurs when an index is out of bounds.Root of the SARL exception type hierarchy.A SARL internal exception represents an error that is "not supposed to happen." It can be used like an assertion, whenever you feel that something should always be true.A symbolic universe is used for the creation and manipulation of
T>A Transform from type S to type T is an object that provides a method "apply" which takes an element of S and returns an element of T.A UnaryOperator on a type T is an object which provides a method "apply" that takes an element of T and returns an element of T.A
ValidityResultrepresents the result of a validity query.The 3 kinds of results to the "valid" question: yes, no, or maybe (a.k.a, "I don't know").