| java.lang.Object
 de.uka.ilkd.key.jml.UsefulTools
| UsefulTools | | public class UsefulTools (Code) | | |
| Method Summary | |
| public static Term | addRepresents(Term t, Services services, ProgramVariable self)
adds updates for represents clauses if necessary. | | public static Term | allInvariants(Implementation2SpecMap ism)
Returns a conjunction of the terms returned by getAllInvariants() for
every JMLClassSpec. | | public static Namespace | buildParamNamespace(MethodDeclaration md)
| | public static SetOfTerm | collectModelVariables(Term b, boolean ignoreMod)
Collects the model variables in b. | | public static Term | createQuantifierTermWithPV(Quantifier q, Term vTerm, LogicVariable lv, Term body)
| | public static Term | createTermForQuery(ProgramMethod pm, ListOfTerm args, ReferencePrefix prefix)
| | public static ParameterDeclaration | getParameterDeclForVar(Term var, Services serv)
| | public static ListOfNamed | getParameters(MethodDeclaration md)
| | public static ListOfTerm | getProgramVariablesFromTerm(Term t, ListOfTerm result)
| | public static boolean | isClassSpec(Comment c)
| | public static Term | isCreated(Term objectToGuard, Services s)
| | public static Term | makeConjunction(Term t1, Term t2)
| | public static ListOfTerm | occursAsAttr(ProgramVariable attr, Term b, boolean ignoreMod)
Checks whether attr occurs in b and
returns the terms of the form t.attr that have been found in
b. | | public static boolean | occursIn(Term a, Term b, boolean ignoreMod)
Checks whether a occurs in b or not. | | public static ProgramMethod | purityCheck(JMLMethodSpec spec, Implementation2SpecMap ism)
Checks whether only pure methods have been used in this specification or
not. | | public static ProgramMethod | purityCheck(Term t, Implementation2SpecMap ism)
Checks whether only pure methods have been used in this term or
not. | | public static Term | quantifyProgramVariable(Term t, ProgramVariable v, Quantifier q, Services serv)
Returns q lv . | | public static Term | quantifyProgramVariables(Term t, Namespace ns, Quantifier q, Services serv)
Creates a quantified LogicVariable lv_i for ProgramVariabes p_i in
t that aren't contained in the Namespace ns. | | public static Term | quantifyProgramVariables(Term t, IteratorOfNamed it, Quantifier q, Services serv)
| | public static Term | quantifySelf(Term t, MethodDeclaration md, ProgramVariable self)
Returns forall self_lv( {self:=self_lv} t ) if t is neither
static nor a constructor or t otherwise. |
| addRepresents | | public static Term addRepresents(Term t, Services services, ProgramVariable self)(Code) | | adds updates for represents clauses if necessary. These Updates have the
form {m := m()}t
where m is a modelfield and m() is a query generated from the represents
clause for m.
|
| allInvariants | | public static Term allInvariants(Implementation2SpecMap ism)(Code) | | Returns a conjunction of the terms returned by getAllInvariants() for
every JMLClassSpec.
|
| collectModelVariables | | public static SetOfTerm collectModelVariables(Term b, boolean ignoreMod)(Code) | | Collects the model variables in b.
If ignoreMod is true,
subterms with a modality as top operant are ignored.
|
| createQuantifierTermWithPV | | public static Term createQuantifierTermWithPV(Quantifier q, Term vTerm, LogicVariable lv, Term body)(Code) | | creates <{typeof(vTerm) v;}> q lv ({vTerm := lv} body)
where v = vTerm.op()
|
| getProgramVariablesFromTerm | | public static ListOfTerm getProgramVariablesFromTerm(Term t, ListOfTerm result)(Code) | | |
| isClassSpec | | public static boolean isClassSpec(Comment c)(Code) | | returns true if c contains a jml keyword that does not occur in
methodspecs
|
| occursAsAttr | | public static ListOfTerm occursAsAttr(ProgramVariable attr, Term b, boolean ignoreMod)(Code) | | Checks whether attr occurs in b and
returns the terms of the form t.attr that have been found in
b. If ignoreMod is true,
subterms with a modality as top operant are ignored.
|
| occursIn | | public static boolean occursIn(Term a, Term b, boolean ignoreMod)(Code) | | Checks whether a occurs in b or not. If
ignoreMod is true, subterms with a modality as top operant
are ignored.
|
| purityCheck | | public static ProgramMethod purityCheck(JMLMethodSpec spec, Implementation2SpecMap ism)(Code) | | Checks whether only pure methods have been used in this specification or
not.
null iff every method used in this term is declared with the jml-modifier pure or a method that isn't declared with pure otherwise. |
| purityCheck | | public static ProgramMethod purityCheck(Term t, Implementation2SpecMap ism)(Code) | | Checks whether only pure methods have been used in this term or
not.
null iff every method used in this term is declared with the jml-modifier pure or a method that isn't declared with pure otherwise. |
| quantifyProgramVariables | | public static Term quantifyProgramVariables(Term t, Namespace ns, Quantifier q, Services serv)(Code) | | Creates a quantified LogicVariable lv_i for ProgramVariabes p_i in
t that aren't contained in the Namespace ns.
q lv_1...lv_n {p_1 := lv_1}..{p_n := lv_n} t. |
|
|