| java.lang.Object
 de.uka.ilkd.key.parser.ocl.FunctionFactory
| FunctionFactory | | public class FunctionFactory (Code) | | ATTENTION: This is not a real factory in the sense of the design
pattern "Factory"!
This Class creates all necessary functions (for the
ocl-translation).
It also creates axioms, defining the semantics of the created functions
and puts them into the AxiomCollector.
Don't forget to reset (resetFactory) the factory for initialization!
|
| Method Summary | |
| public static Term | buildAddTerm(Term[] subTerms)
| | public Function | createAllInstancesConstant(CollectionSort csort)
| | public Function | createAllInstancesConstant(Sort sort)
| | public Function | createCollectFunction(LogicVariable collectVar, Term collectTerm, int collectionType)
| | public Term | createRangedBag(Term lowerBound, Term upperBound, Function leq)
| | public Term | createRangedSequence(Term lowerBound, Term upperBound, Function leq)
| | public Term | createRangedSet(Term lowerBound, Term upperBound, Function leq)
| | public Function | createRejectFunction(LogicVariable rejectVar, Term rejectTerm, int collectionType)
| | public Function | createSelectFunction(LogicVariable selectVar, Term selectTerm, int collectionType)
| | public Term | excluding(Term setSymbol, Term element)
| | public static CollectionSort | getBagSort(Sort sort)
| | public static CollectionSort | getCollectionSort(Sort sort, int collectionType)
| | public SetOfLogicVariable | getCreatedVars()
| | public Function | getEmptyBag(Sort sort)
| | public Function | getEmptyCollection(Sort sort, int collectionType)
| | public Function | getEmptySequence(Sort sort)
| | public Function | getEmptySet(Sort sort)
| | public Namespace | getFunctions()
| | public static CollectionSort | getSequenceSort(Sort sort)
| | public static CollectionSort | getSetSort(Sort sort)
| | public Term | including(Term setSymbol, Term element)
| | public void | resetFactory(Services services, AxiomCollector ac)
initialises the required parameters for the FunctionFactory to work properly
ATTENTION: must be called once before any of the other non-static methods. | | public Term | simplify(Term t)
| | public Term | union(Term t1, Term t2)
| | public Term | unionAndSimplify(Term t1, Term t2)
|
| buildAddTerm | | public static Term buildAddTerm(Term[] subTerms)(Code) | | Conjunction of subTerms |
| createAllInstancesConstant | | public Function createAllInstancesConstant(CollectionSort csort)(Code) | | creates an appropriate function-symbol representing allInstances of the given sort
and the axiom that specifies the meaning of this function-symbol
C.allInstances()
Parameters:
csort - CollectionSort of the function-symbol |
| createAllInstancesConstant | | public Function createAllInstancesConstant(Sort sort)(Code) | | creates an appropriate function-symbol representing allInstances of the given sort
and the axiom that specifies the meaning of this function-symbol
Parameters:
sort - Element-Sort of the function-symbol |
| createCollectFunction | | public Function createCollectFunction(LogicVariable collectVar, Term collectTerm, int collectionType) throws OCLTranslationError(Code) | | creates an appropriate function-symbol representing collect for the given term
and adds the axioms that specifie the meaning of this function-symbol to the
local axiom-list
c->collect(e | b)
Parameters:
collectVar - Translation of e
Parameters:
selectTerm - Translation of b
throws:
OCLTranslationError - |
| createRejectFunction | | public Function createRejectFunction(LogicVariable rejectVar, Term rejectTerm, int collectionType) throws OCLTranslationError(Code) | | creates an appropriate function-symbol representing reject for the given term
and adds the axioms that specifie the meaning of this function-symbol to the
local axiom-list
c->reject(e | b)
Parameters:
rejectVar - Translation of e
Parameters:
rejectTerm - Translation of b
throws:
OCLTranslationError - |
| createSelectFunction | | public Function createSelectFunction(LogicVariable selectVar, Term selectTerm, int collectionType) throws OCLTranslationError(Code) | | creates an appropriate function-symbol representing select for the given term
and adds the axioms that specifie the meaning of this function-symbol to the
local axiom-list
c->select(e | b)
Parameters:
selectVar - Translation of e
Parameters:
selectTerm - Translation of b
throws:
OCLTranslationError - |
| getCollectionSort | | public static CollectionSort getCollectionSort(Sort sort, int collectionType)(Code) | | Returns the corresponding CollectionSort of the given sort
Parameters:
sort -
Parameters:
collectionType - the concrete collection type according to OCLCollection null if no AbstractNonCollectionSort is given,otherwise the corresponding CollectionSort is returned. |
| getCreatedVars | | public SetOfLogicVariable getCreatedVars()(Code) | | returns the list of created variables which are used in the axioms
|
| getEmptyBag | | public Function getEmptyBag(Sort sort)(Code) | | Returns the function-symbol representing emptyBag of the given sort
Parameters:
sort - may be the elementsort or the collectionsort function-symbol representing emptyBag |
| getEmptyCollection | | public Function getEmptyCollection(Sort sort, int collectionType)(Code) | | Returns the function-symbol representing emptyCollection of the given type and sort
Parameters:
elementsort - of the collection function-symbol representing emptyCollection |
| getEmptySequence | | public Function getEmptySequence(Sort sort)(Code) | | Returns the function-symbol representing emptySequence of the given sort
Parameters:
sort - may be the elementsort or the collectionsort function-symbol representing emptySequence |
| getEmptySet | | public Function getEmptySet(Sort sort)(Code) | | Returns the function-symbol representing emptySet of the given sort
Parameters:
sort - may be the elementsort or the collectionsort function-symbol representing emptySet |
| getFunctions | | public Namespace getFunctions()(Code) | | returns the namespace which holds all the created functions
|
| resetFactory | | public void resetFactory(Services services, AxiomCollector ac)(Code) | | initialises the required parameters for the FunctionFactory to work properly
ATTENTION: must be called once before any of the other non-static methods.
Sets all parameters to initial values - any prior changes get lost!
Parameters:
services -
Parameters:
ac - |
|
|