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 expressionsedu.udel.cis.vsl.sarl.IF.number
 infinite precision integer and rational numbersedu.udel.cis.vsl.sarl.IF.object
 general symbolic objectsedu.udel.cis.vsl.sarl.IF.type
 symbolic types
 See Also:

ClassDescriptionA substituter used to assign new, canonical names to all symbolic constants occurring in a sequence of expressions.A
CoreUniverse
provides most of the functionality of aSymbolicUniverse
, including the mechanisms to create and manipulateSymbolicExpression
s and otherSymbolicObject
s.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 returnstrue
orfalse
.A reasoner provides methods to simplifySymbolicExpression
s and prove or disprove certain theorems, all under an overarching 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 ofSymbolicObject
s.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.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.AValidityResult
represents 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").