| java.lang.Object
 de.uka.ilkd.key.logic.op.QuanUpdateOperator
| QuanUpdateOperator | | public class QuanUpdateOperator implements IUpdateOperator(Code) | |
Operator for simultaneous, guarded and quantified updates. In concrete
syntax, such updates have the shape
[ for (Variables) ] [ if (Formula) ] lhs := value
( , [ for (Variables) ] [ if (Formula) ] lhs := value ) * .
The update operator is uniquely defined by the contained locations, their
order, and the information which of the assigments are guarded (a boolean
array). This has some odd consequences of the sub terms of an update term as
given above:
- Let
loc_1,...,loc_i be local or static variables then
only the corresponding values val_1, ..., val_n are subterms
the locations itself are part of the operator.
- For
loc_i (=r_i.a_i),...,loc_n(=r_n.a_n) that refer to an
instance attribute, only their reference prefix r_i is a
subterm while the attribute a_i is part of the update
operator. If loc_i is an array a[l] then the
sort of a is fixed and a, i are sub terms
There are methods that return the location access part (attribute, local or
static variable) and also the complete n-th location as term.
|
| Method Summary | |
| public int | arity()
| | public ArrayOfQuantifiableVariable | boundVars(Term t, int locPos)
| | public static QuanUpdateOperator | createUpdateOp(Term[] locs, boolean[] guards)
| | public static QuanUpdateOperator | createUpdateOp(Location[] locs, boolean[] guards)
| | public int | entryBegin(int locPos)
| | public int | entryEnd(int locPos)
the index after the last subterm belonging to update entrylocPos. | | public int[] | getLocationPos(Operator loc)
| | public Term | guard(Term t, int n)
| | public boolean | guardExists(int locPos)
| | public int | guardPos(int locPos)
| | public boolean | isRigid(Term term)
| | public Location | location(int n)
| | public Term | location(Term t, int n)
| | public int | locationCount()
| | public int | locationSubtermsBegin(int locPos)
| | public int | locationSubtermsEnd(int locPos)
the index after the last subterm belonging to the location ofupdate entry locPos. | | public ArrayOfLocation | locationsAsArray()
| | public MatchConditions | match(SVSubstitute subst, MatchConditions mc, Services services)
| | public Name | name()
| | public static Term | normalize(ArrayOfQuantifiableVariable[] boundVars, Term[] guards, Term[] leftHandSides, Term[] values, Term target)
Create a term from a list of (quantified, guarded) elementary updates and
a target term/formula. | | public Term | normalize(ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs)
Given the update operator (this), the variables that are
bound and the subterms, create a new term. | | public IUpdateOperator | replaceLocations(Location[] newLocs)
Replace the locations of this operator without changing anything else. | | public Sort | sort(Term[] term)
returns the sort a term would have if constructed with this operator and
the given sunterms. | | public Term | target(Term t)
| | public int | targetPos()
| | public ArrayOfQuantifiableVariable[] | toBoundVarsPerAssignment(ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs)
The term class for quantified updates requires that the same variables
are quantified for all parts of an update entry (subterms of the
left-hand side, guard and the value); in principle this could also be
done more generally and with different variables. | | public String | toString()
| | public boolean | validTopLevel(Term term)
checks whether the top level structure of the given
Term is
syntactically valid, given the assumption that the top level operator of
the term is the same as this Operator. | | public Term | value(Term t, int n)
| | public int | valuePos(int locPos)
|
| arity | | public int arity()(Code) | | returns the arity of the operator
|
| boundVars | | public ArrayOfQuantifiableVariable boundVars(Term t, int locPos)(Code) | | the variables that are quantified for the elementary updatelocPos |
| createUpdateOp | | public static QuanUpdateOperator createUpdateOp(Term[] locs, boolean[] guards)(Code) | | returns the update operator for the given location order
|
| createUpdateOp | | public static QuanUpdateOperator createUpdateOp(Location[] locs, boolean[] guards)(Code) | |
Parameters:
guards - boolean array telling which of the elementary updates areguarded the update operator for the given location order |
| entryBegin | | public int entryBegin(int locPos)(Code) | | the index of the first subterm belonging to update entrylocPos |
| entryEnd | | public int entryEnd(int locPos)(Code) | | the index after the last subterm belonging to update entrylocPos. The entry is described within[entryBegin(i), entryEnd(i)) |
| getLocationPos | | public int[] getLocationPos(Operator loc)(Code) | | returns an array with all location positions of loc
Parameters:
loc - a n Operator accessing a location all location positions of loc |
| guard | | public Term guard(Term t, int n)(Code) | | returns the guard of the n-th update entry; if this entry does not have a
guard, TRUE is returned
Parameters:
t - Term with this operator as top level operator
Parameters:
n - an int specifying the position of the location the guard of the n-th update entry |
| guardExists | | public boolean guardExists(int locPos)(Code) | | true iff the elementary update with indexlocPos is guarded |
| guardPos | | public int guardPos(int locPos)(Code) | | the number of the subterm representing the guard constraining thelocPos -th update, provided that this guard exists(otherwise -1) |
| isRigid | | public boolean isRigid(Term term)(Code) | | true if the value of "term" having this operator as top-leveloperator and may not be changed by modalities |
| location | | public Location location(int n)(Code) | | returns the operator of n-th location
|
| location | | public Term location(Term t, int n)(Code) | | returns the n-th location of the update as term
Parameters:
t - Term with this operator as top level operator
Parameters:
n - an int specifying the position of the requested location the n-th location of term t updated by this operator |
| locationCount | | public int locationCount()(Code) | | returns the number of locations
the number of locations as int |
| locationSubtermsBegin | | public int locationSubtermsBegin(int locPos)(Code) | | the index of the first subterm belonging to the location of entrylocPos |
| locationSubtermsEnd | | public int locationSubtermsEnd(int locPos)(Code) | | the index after the last subterm belonging to the location ofupdate entry locPos. The location is describedwithin[locationSubtermsBegin(i), locationSubtermsEnd(i)) |
| locationsAsArray | | public ArrayOfLocation locationsAsArray()(Code) | | returns the array of location operators which are updated
|
| normalize | | public static Term normalize(ArrayOfQuantifiableVariable[] boundVars, Term[] guards, Term[] leftHandSides, Term[] values, Term target)(Code) | | Create a term from a list of (quantified, guarded) elementary updates and
a target term/formula. The update of the result is optimized as far as
possible by sorting the elementary updates, removing unnecessary updates
and removing trivial guards. The four array arguments are supposed to
have the same size.
|
| normalize | | public Term normalize(ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs)(Code) | | Given the update operator (this), the variables that are
bound and the subterms, create a new term. This applies the same
optimisations as
normalize (ArrayOfQuantifiableVariable[], Term[], Term[], Term[], Term )
|
| replaceLocations | | public IUpdateOperator replaceLocations(Location[] newLocs)(Code) | | Replace the locations of this operator without changing anything else.
This must not change the number of locations, i.e.
newLocs.length==locationCount()
|
| sort | | public Sort sort(Term[] term)(Code) | | returns the sort a term would have if constructed with this operator and
the given sunterms. It is assumed that the term would be allowed if
constructed.
Parameters:
term - an array of Term containing the subterms of a (potential)simultaneous update term sort of the simultaneous update term consisting of the givensubterms, if this op would be the top symbol |
| target | | public Term target(Term t)(Code) | | the index of the subterm representing the formula/term the updateis applied to |
| targetPos | | public int targetPos()(Code) | | the position of the term the quantified update is applied to
the sub term position of the target term |
| toBoundVarsPerAssignment | | public ArrayOfQuantifiableVariable[] toBoundVarsPerAssignment(ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs)(Code) | | The term class for quantified updates requires that the same variables
are quantified for all parts of an update entry (subterms of the
left-hand side, guard and the value); in principle this could also be
done more generally and with different variables. Given arrays of
variables for each entry part, an common array is constructed here
(unification). This can include bound renaming.
Parameters:
boundVarsPerSub - the arrays of variables bound for each subterm
Parameters:
subs - the subterms of the update entry. The components of this arrayare modified if bound renaming is necessary the arrays of variables bound for each location |
| toString | | public String toString()(Code) | | returns a string representation of the update operator
|
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | checks whether the top level structure of the given
Term is
syntactically valid, given the assumption that the top level operator of
the term is the same as this Operator. The assumption that the top level
operator and the operator are equal is NOT checked.
true iff the top level structure of the Termis valid. |
| value | | public Term value(Term t, int n)(Code) | | returns value the n-th location is updated with
Parameters:
t - Term with this operator as top level operator
Parameters:
n - an int specifying the position of the location the value the n-th location is updated with |
| valuePos | | public int valuePos(int locPos)(Code) | | returns the number of the subterm representing the value to which
the locPos-th location is updated
|
|
|