Package edu.udel.cis.vsl.sarl.IF

package edu.udel.cis.vsl.sarl.IF

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:

• edu.udel.cis.vsl.sarl.IF.expr - symbolic expressions
• edu.udel.cis.vsl.sarl.IF.number - infinite precision integer and rational numbers
• edu.udel.cis.vsl.sarl.IF.object - general symbolic objects
• edu.udel.cis.vsl.sarl.IF.type - symbolic types

See Also:

• SymbolicUniverse
• SARL

Related Packages

Package	Description
edu.udel.cis.vsl.sarl	This is the root package for SARL, and contains the single class SARL.
edu.udel.cis.vsl.sarl.IF.config	The config module provides a SARLConfig type, which encapsulates configuration information such as the list of available theorem provers with information on each.
edu.udel.cis.vsl.sarl.IF.expr	The public interface package dealing with symbolic expressions.
edu.udel.cis.vsl.sarl.IF.number	The number package supports infinite-precision integer and rational numbers.
edu.udel.cis.vsl.sarl.IF.object	The object package provides the SymbolicObject interface, which is the root of the symbolic object type hierarchy.
edu.udel.cis.vsl.sarl.IF.type	The type package provides interfaces for all of the symbolic types.

Class	Description
CanonicalRenamer	A substituter used to assign new, canonical names to all symbolic constants occurring in a sequence of expressions.
CoreUniverse	A CoreUniverse provides most of the functionality of a SymbolicUniverse, including the mechanisms to create and manipulate SymbolicExpressions and other SymbolicObjects.
CoreUniverse.ForallStructure	The result of analyzing certain "forall" expressions.
ModelResult	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 true or false.
Reasoner	A reasoner provides methods to simplify SymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context".
SARLBoundException	An exception that occurs when an index is out of bounds.
SARLConstants
SARLException	Root of the SARL exception type hierarchy.
SARLInternalException	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.
SymbolicUniverse	A symbolic universe is used for the creation and manipulation of SymbolicObjects.
TheoremProverException
Transform<S,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.
UnaryOperator<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.
ValidityResult	A ValidityResult represents the result of a validity query.
ValidityResult.ResultType	The 3 kinds of results to the "valid" question: yes, no, or maybe (a.k.a, "I don't know").