| java.lang.Object de.uka.ilkd.key.logic.AnonymisingUpdateFactory
AnonymisingUpdateFactory | public class AnonymisingUpdateFactory (Code) | | Creates anonymising updates for sets of locations, i.e. (quantified) updates
which assign uninterpreted functions to all locations of such a set.
|
Method Summary | |
public Update | createAnonymisingUpdate(LocationDescriptor[] locations, Function[] functions, Services services) Creates the anonymising update for the passed locations using the passed
uninterpreted functions (which must have the correct signature). | public Update | createAnonymisingUpdate(SetOfLocationDescriptor locations, Services services) Creates the anonymising update for the passed locations using new
uninterpreted functions. | public Update | createAnonymisingUpdate(SetOfLocationDescriptor locations, Term[] commonArguments, Services services) | public Term | createAnonymisingUpdateAsFor(LocationDescriptor[] locationsArray, Term[] commonArguments, Services services) Creates the anonymising update for the passed locations using new
uninterpreted functions and applies it to the passed target term. | public Term | createAnonymisingUpdateTerm(LocationDescriptor[] locations, Function[] functions, Term targetTerm, Services services) Creates the anonymising update for the passed locations using the passed
uninterpreted functions (which must have the correct signature) and
applies it to the passed target term. | public Term | createAnonymisingUpdateTerm(SetOfLocationDescriptor locations, Term targetTerm, Services services) Creates the anonymising update for the passed locations using new
uninterpreted functions and applies it to the passed target term. | public static RigidFunction[] | createUninterpretedFunctions(LocationDescriptor[] locations, Sort[] commonArguments, Services services) Creates suitable uninterpreted functions for the passed locations. | public static RigidFunction[] | createUninterpretedFunctions(LocationDescriptor[] locations, Services services) Creates suitable uninterpreted functions for the passed locations. |
createAnonymisingUpdate | public Update createAnonymisingUpdate(LocationDescriptor[] locations, Function[] functions, Services services)(Code) | | Creates the anonymising update for the passed locations using the passed
uninterpreted functions (which must have the correct signature).
|
createAnonymisingUpdate | public Update createAnonymisingUpdate(SetOfLocationDescriptor locations, Services services)(Code) | | Creates the anonymising update for the passed locations using new
uninterpreted functions.
|
createAnonymisingUpdate | public Update createAnonymisingUpdate(SetOfLocationDescriptor locations, Term[] commonArguments, Services services)(Code) | | |
createAnonymisingUpdateAsFor | public Term createAnonymisingUpdateAsFor(LocationDescriptor[] locationsArray, Term[] commonArguments, Services services)(Code) | | Creates the anonymising update for the passed locations using new
uninterpreted functions and applies it to the passed target term.
|
createAnonymisingUpdateTerm | public Term createAnonymisingUpdateTerm(LocationDescriptor[] locations, Function[] functions, Term targetTerm, Services services)(Code) | | Creates the anonymising update for the passed locations using the passed
uninterpreted functions (which must have the correct signature) and
applies it to the passed target term.
|
createAnonymisingUpdateTerm | public Term createAnonymisingUpdateTerm(SetOfLocationDescriptor locations, Term targetTerm, Services services)(Code) | | Creates the anonymising update for the passed locations using new
uninterpreted functions and applies it to the passed target term.
|
|
|