| java.lang.Object
 de.uka.ilkd.key.logic.UpdateFactory
| UpdateFactory | | public class UpdateFactory (Code) | | Factory providing the update constructors that are described in "Sequential,
Parallel and Quantified Updates of First-Order Structures". Don't try to use
this class together with anonymous updates, this would probably screw up
everything horribly.
TODO: so far, updates are not simplified during construction; the factory
could be optimized
|
| Method Summary | |
| public Term | apply(Update update, Term target)
| | public Update | apply(Update update, Update target)
| | public Update | elementaryUpdate(Term leftHandSide, Term value)
Create an elementary update leftHandSide := value
Parameters:
leftHandSide - Term describing the location that is updated. | | public Update | guard(Term guard, Update update)
Add the guard guard as a condition to update,
i.e. | | public Update | parallel(Update update1, Update update2)
| | public Update | parallel(Update[] updates)
Compute the parallel composition of an array of updates. | | public Term | prepend(Update update, Term target)
| | public Update | quantify(QuantifiableVariable var, Update update)
Quantify over var, i.e. | | public Update | sequential(Update update1, Update update2)
| | public Update | sequential(Update[] updates)
Compute the sequential composition of an array of updates. | | public Update | skip()
|
| apply | | public Term apply(Update update, Term target)(Code) | | Apply an update to a term or a formula, simplify the result
|
| elementaryUpdate | | public Update elementaryUpdate(Term leftHandSide, Term value)(Code) | | Create an elementary update leftHandSide := value
Parameters:
leftHandSide - Term describing the location that is updated. The operator ofthe term has to implement the interface Location.
Parameters:
value - Term describing the new value of the updated location the resulting update |
| guard | | public Update guard(Term guard, Update update)(Code) | | Add the guard guard as a condition to update,
i.e. only carry out the update if guard evaluates to true
|
| parallel | | public Update parallel(Update update1, Update update2)(Code) | | Compute the parallel composition of two updates,
update1 | update2
|
| parallel | | public Update parallel(Update[] updates)(Code) | | Compute the parallel composition of an array of updates.
TODO: this could be implemented more efficiently
|
| prepend | | public Term prepend(Update update, Term target)(Code) | | Apply an update to a term or a formula, without simplifying the result
|
| sequential | | public Update sequential(Update update1, Update update2)(Code) | | Compute the sequential composition of two updates,
update1 ; update2
|
| sequential | | public Update sequential(Update[] updates)(Code) | | Compute the sequential composition of an array of updates.
|
| skip | | public Update skip()(Code) | | The neutral update (neutral element concerning parallel and sequential
composition) not updating anything
|
|
|