Uses of Package
dev.civl.sarl.IF
Packages that use dev.civl.sarl.IF
Package
Description
This is the root package for SARL, and contains the single class
SARL.This package and its subpackages provide the "public interface" to SARL.
The config module provides a
SARLConfig type, which
encapsulates configuration information such as the list of available theorem
provers with information on each.The public interface package dealing with symbolic expressions.
The object package provides the
SymbolicObject
interface, which is the root of the symbolic object type hierarchy.This package provides the internal interface for the representation of basic
symbolic expressions.
This package provides all of the functionality of a symbolic universe except
reasoning.
Module "prove" constitutes the interface between SARL and (possibly external)
theorem provers.
The internal interface for the "reason" module, which deals with
Reasoners --- objects used to prove
theorems and simplify symbolic expressions.Internal interface for the "universe" module.
-
Classes in dev.civl.sarl.IF used by dev.civl.sarl
-
Classes in dev.civl.sarl.IF used by dev.civl.sarl.IFClassDescriptionA substituter used to assign new, canonical names to all symbolic constants occurring in a sequence of expressions.A
CoreUniverseprovides most of the functionality of aSymbolicUniverse, including the mechanisms to create and manipulateSymbolicExpressions and otherSymbolicObjects.The result of analyzing certain "forall" expressions.A Predicate on type T is an object that provides a method "apply" which takes an element of T and returnstrueorfalse.A reasoner provides methods to simplifySymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context".Root of the SARL exception type hierarchy.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.AValidityResultrepresents 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"). -
Classes in dev.civl.sarl.IF used by dev.civl.sarl.IF.config
-
Classes in dev.civl.sarl.IF used by dev.civl.sarl.IF.exprClassDescriptionThe 3 kinds of results to the "valid" question: yes, no, or maybe (a.k.a, "I don't know").
-
Classes in dev.civl.sarl.IF used by dev.civl.sarl.IF.objectClassDescriptionA 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.
-
Classes in dev.civl.sarl.IF used by dev.civl.sarl.expr.IFClassDescriptionA reasoner provides methods to simplify
SymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context". -
Classes in dev.civl.sarl.IF used by dev.civl.sarl.preuniverse.IFClassDescriptionA
CoreUniverseprovides most of the functionality of aSymbolicUniverse, including the mechanisms to create and manipulateSymbolicExpressions and otherSymbolicObjects.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. -
Classes in dev.civl.sarl.IF used by dev.civl.sarl.prove.IFClassDescriptionA result to a validity query which also requested a model in case the answer was "NO", and for which the answer was "NO".A symbolic universe is used for the creation and manipulation of
SymbolicObjects.AValidityResultrepresents 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"). -
Classes in dev.civl.sarl.IF used by dev.civl.sarl.reason.IFClassDescriptionA reasoner provides methods to simplify
SymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context". -
Classes in dev.civl.sarl.IF used by dev.civl.sarl.universe.IF