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

Interface SymbolicUniverse

All Superinterfaces:

CoreUniverse

All Known Implementing Classes:

CommonSymbolicUniverse, MathUniverse

public interface SymbolicUniverse
extends CoreUniverse

A symbolic universe is used for the creation and manipulation of SymbolicObjects. The symbolic objects created by this universe are said to belong to this universe. Every symbolic object belongs to one universe, though a reference to the universe is not necessarily stored in the object.

s are one kind of symbolic object. Other symbolic objects include SymbolicCollections (such as sequences, sets, and maps), SymbolicTypes, and various concrete SymbolicObjects.

SymbolicObjects implement the Immutable Pattern: all symbolic objects are immutable, i.e., they cannot be modified after they are created.

Nested Class Summary

Nested classes/interfaces inherited from interface edu.udel.cis.vsl.sarl.IF.CoreUniverse

CoreUniverse.ForallStructure

Method Summary

Modifier and Type	Method	Description
void	enableSARLTestGeneration(boolean enable)	Enable SARL test generation.
Number	extractNumber(BooleanExpression assumption, NumericExpression expression)	Attempts to extract a concrete numeric value from the given expression, using the assumption if necessary to simplify the expression.
void	generateTestClass(String className)	pre-condition enableSARLTestGeneration(boolean) has been set to true
Reasoner	reasoner(BooleanExpression context)	Returns a Reasoner for the given context.
void	saveValidCallAsSARLTest(BooleanExpression context, BooleanExpression predicate, ValidityResult.ResultType expectedResult, boolean useWhy3, String testName, String... comments)	pre-condition enableSARLTestGeneration(boolean) has been set to true
void	setLogicFunctions(ProverFunctionInterpretation[] logicFunctions)	Set a list of logic functions with their definitions to the universe so that Reasoners created by this universe can take use of the definitions of the given logic functions.
Reasoner	why3Reasoner(BooleanExpression context)	Same as #reasoner(BooleanExpression, boolean) but only Why3 prove platform will be used if it is installed.

Methods inherited from interface edu.udel.cis.vsl.sarl.IF.CoreUniverse

add, add, and, and, append, apply, array, array, arrayDimensionAndBaseType, arrayElementReference, arrayLambda, arrayRead, arrayType, arrayType, arrayWrite, assign, bitand, bitnot, bitor, bitshiftLeft, bitshiftRight, bitvector2Integer, bitVectorType, bitxor, bool, bool, booleanObject, booleanType, boundedIntegerType, canonicalRenamer, canonicalRenamer, cardinality, cast, ceil, character, characterType, comparator, compatible, concreteValueOfUninterpretedType, cond, constantArray, denseArrayWrite, dereference, derivative, differentiable, divide, divides, emptyArray, emptyMap, entrySet, entryType, equals, equiv, exists, existsInt, expand, extractBoolean, extractCharacter, extractNumber, falseExpression, floor, forall, forallInt, fullySubstitute, functionType, get, getErrFile, getForallStructure, getFreeSymbolicConstants, getIntegerLengthBound, getOutputStream, getProbabilisticBound, getShowProverQueries, getShowQueries, getSummands, getUseBackwardSubstitution, herbrandIntegerType, herbrandRealType, identityReference, implies, insertElementAt, integer, integer, integer, integer2Bitvector, integerType, intObject, isPermutCall, isSigmaCall, isSubsetOf, keySet, lambda, length, lessThan, lessThanEquals, make, mapSize, mapSubstituter, mapType, minus, modulo, multiply, multiply, nameSubstituter, neq, not, nullExpression, nullReference, number, number, numberFactory, numberObject, numObjects, numProverValidCalls, numValidCalls, objectWithId, offsetReference, oneInt, oneReal, or, or, permut, power, power, power, printCompressed, printCompressedTree, printExprTree, pureType, put, rational, rational, rational, rational, rational, rational, rational, rational, realType, reduction, referencedType, referenceType, removeElementAt, removeEntryWithKey, roundToZero, setAdd, setDifference, setErrFile, setIntegerLengthBound, setIntersection, setOutputStream, setProbabilisticBound, setRemove, setShowProverQueries, setShowQueries, setType, setUnion, setUseBackwardSubstitution, sigma, simpleSubstituter, stringExpression, stringObject, subtract, symbolicConstant, symbolicUninterpretedType, trueExpression, tuple, tuple, tupleComponentReference, tupleRead, tupleType, tupleWrite, unionExtract, unionInject, unionMemberReference, unionTest, unionType, valueSetAssigns, valueSetContains, valueSetNoIntersect, valueSetReferences, valueSetReferenceType, valueSetTemplate, valueSetTemplateType, valueSetUnion, valueSetWidening, valueType, vsArrayElementReference, vsArraySectionReference, vsArraySectionReference, vsIdentityReference, vsOffsetReference, vsTupleComponentReference, vsUnionMemberReference, zeroInt, zeroReal

Method Details

reasoner

Reasoner reasoner(BooleanExpression context)

Returns a Reasoner for the given context. A Reasoner provides simplification and reasoning services. The context is the boolean expression assumed to hold by the reasoner. The Reasoner can be used to determine if a boolean predicate is valid; it may use an external theorem prover to assist in this task.

Parameters:

context - the boolean expression assumed to hold by the Reasoner

Returns:

a Reasoner with the given context

extractNumber

Number extractNumber(BooleanExpression assumption,
 NumericExpression expression)

Attempts to extract a concrete numeric value from the given expression, using the assumption if necessary to simplify the expression. For example, if the assumption is "N=5" and the expression is "N", this method will probably return the number 5. If it cannot obtain a concrete value for whatever reason, it will return null.

Parameters:

assumption - a boolean expression that is assumed to hold

expression - a symbolic expression of numeric type

Returns:

a concrete Number or null

why3Reasoner

Reasoner why3Reasoner(BooleanExpression context)

Same as #reasoner(BooleanExpression, boolean) but only Why3 prove platform will be used if it is installed. If Why3 is not installed, this function is equivalent to #reasoner(BooleanExpression, boolean)

Parameters:

context - a non-null boolean expression to be used as the context for the Reasoner

Returns:

a Reasoner based on the given context

setLogicFunctions

void setLogicFunctions(ProverFunctionInterpretation[] logicFunctions)

Set a list of logic functions with their definitions to the universe so that Reasoners created by this universe can take use of the definitions of the given logic functions.

Logic functions are instances of ProverFunctionInterpretations

Parameters:

logicFunctions - an array of ProverFunctionInterpretations

enableSARLTestGeneration

void enableSARLTestGeneration(boolean enable)

Enable SARL test generation. Once it is enabled, clients can call #saveValidCallAsSARLTest(BooleanExpression, BooleanExpression, ProverFunctionInterpretation[], ResultType, String[]) to add new tests and call generateTestClass(String) to generate Junit test class file.

Parameters:

enable - true to enable SARL test generation; otherwise, disable SARL test generation

saveValidCallAsSARLTest

void saveValidCallAsSARLTest(BooleanExpression context,
 BooleanExpression predicate,
 ValidityResult.ResultType expectedResult,
 boolean useWhy3,
 String testName,
 String... comments)

pre-condition enableSARLTestGeneration(boolean) has been set to true

Saving a query as a SARL's Junit test. No-op if pre-condition is not satisified.

Parameters:

context - a non-null boolean expression to be used as the context for the Reasoner

predicate - a non-null boolean expression which is the asserted predicate of the saving query

expectedResult - the expected ValidityResult.ResultType of this query. If the test gets a result that is same as the expectedResult, the test passes, otherwise the test fails.

useWhy3 - if this valid call must be proved by why3

testName - name of this saving test

comments - Variable number of arguments for Java comments over the generated query. One comment block per argument.

generateTestClass

void generateTestClass(String className)

pre-condition enableSARLTestGeneration(boolean) has been set to true

Flush all saved SARLTests to a java class. No-op if pre-condition is not satisified.

Parameters:

className - the name of the generated class