| java.lang.Object
 de.uka.ilkd.key.logic.TermBuilder
de.uka.ilkd.key.jml.JMLSpec
de.uka.ilkd.key.jml.JMLMethodSpec
All known Subclasses: de.uka.ilkd.key.jml.JMLNormalMethodSpec, de.uka.ilkd.key.jml.JMLPuritySpec, de.uka.ilkd.key.jml.JMLExceptionalMethodSpec,
| Inner Class :protected class ModTermKey | |
| Method Summary | |
| public void | addAssignable(SetOfLocationDescriptor locations)
| | public void | addDiverges(Term t)
| | public static Term | addOldQuantifiers(Term a, Map term2old, boolean useQuantifiers, Namespace params)
Applies the transformation tau_update to a iff
useQuantifiers == false or tau_old otherwise. | | public void | addPost(Term t)
| | public void | addPre(Term t)
| | public void | addSignals(KeYJavaType exc, ProgramVariable v, Term cond)
| | public Term | bindSpecVars(Term t)
| | protected JavaBlock | catchAllJB(boolean desugar)
| | public void | clearModalityTermForEnsuresCache()
| | public JMLMethodSpec | cloneFor(ProgramMethod pm, JMLClassSpec cSpec)
This is used for modelling specification inheritance for overwritten
methods. | | protected JMLMethodSpec | cloneForHelper(JMLMethodSpec clone, ProgramMethod pm, JMLClassSpec cSpec)
| | public boolean | containsQuantifiedAssignableLocation()
| | public JMLMethodSpec | copy()
| | protected JMLMethodSpec | copyHelper(JMLMethodSpec copy)
copys several fields to the incomplete copy copy of this. | | public Term | createDLFormula(boolean withPostInvariant, boolean allInvariants)
Creates a DL formula from this method specification:
((pre & inv) -> [{methodbody}]post) & ((pre & inv & !diverges) -> <{methodbody}>post)
(This is the DL formula that is needed for an "ensured postcondition
proofobligation")
withInvariant: iff true the invariant of the containing typeis added to the postcondition which is needed for JMLPostAndInvPOs created by JMLMethodContracts. | | protected Term | createDiverges()
| | protected static Term | createEqualityTermForOldLV(Term t, Term old, LinkedList l, LinkedList oldFS, Map lv2old)
| | protected Term | createModalityTermForEnsures(Term post, boolean desugar, boolean withInv, boolean allInv)
| | public SetOfLocationDescriptor | getAssignable()
| | public String | getAssignableMode()
| | public CatchAllStatement | getCatchAllStatement()
| | public TypeDeclaration | getClassDeclaration()
| | public Term | getCompletePost(boolean withClassSpec, boolean allInv)
| | public Term | getCompletePostFunctional(boolean withClassSpec, boolean allInv)
| | public Term | getCompletePre(boolean withClassSpec, boolean allInv, boolean terminationCase)
returns the precondition + represents for model fields
(+ invariants iff withClassSpec = true, + the negation of the diverges
clause in order to retrieve a precondition under which the method must
terminate). | | public ProgramVariable | getExceptionVariable()
returns the ProgramVariable that is used for expressing the excetional
behavior of a method. | | public ReferencePrefix | getInheritedPrefix()
| | public String | getJavaPath()
| | public Map | getLv2Const()
| | public MethodDeclaration | getMethodDeclaration()
| | public JavaModelMethod | getModelMethod()
| | public NamespaceSet | getNamespaces()
| | public ListOfOperator | getOldFuncSymbols()
| | public ListOfQuantifierPrefixEntry | getOldLVs()
| | public ProgramVariable | getParameterAt(int i)
| | public Term | getPi1()
| | public Term | getPi1Functional()
| | public Term | getPost()
| | public Term | getPre()
| | public ReferencePrefix | getPrefix()
| | public ProgramMethod | getProgramMethod()
| | public ProgramElement | getProofStatement()
| | public ProgramVariable | getResultVar()
| | public ProgramVariable | getSelf()
| | public Services | getServices()
| | public SetOfSignals | getSignals()
| | public ListOfNamed | getSpecVars()
| | public LinkedHashMap | getTerm2Old()
| | public int | id()
| | public Collection | introducedConstants()
| | public boolean | isCloneableFor(ProgramMethod method)
Checks if name, signature, accessibility and so on are equal for
this.pm and pm. | | public StatementBlock | makeMBS()
| | public Term | replaceFreeVarsWithConsts(Term t)
| | public SetOfLocationDescriptor | replaceModelFieldsInAssignable()
| | public SetOfLocationDescriptor | replaceModelFieldsInAssignable(JMLClassSpec cs)
| | public void | setAssignableMode(String s)
| | public void | setId(int id)
| | public void | setSpecVars(ListOfNamed svs)
| | public boolean | terminates()
returns true if this specification demands termination of the method,
which means in this case that terminating by throwing an exception
is also considered to be a termination. | | public String | toString()
| | protected String | toStringHelper(String s)
| | protected Term | updateParameters(ArrayOfParameterDeclaration oldParams, ArrayOfParameterDeclaration newParams, Term target)
| | protected Term | updatePrefix(Term t)
|
| assignableVariables | | protected SetOfLocationDescriptor assignableVariables(Code) | | |
| excCondCount | | protected static int excCondCount(Code) | | |
| exceptionVarCount | | protected static int exceptionVarCount(Code) | | |
| logicVarCount | | protected static int logicVarCount(Code) | | |
| resultVarCount | | protected static int resultVarCount(Code) | | |
| signals | | protected SetOfSignals signals(Code) | | |
| staticInit | | protected boolean staticInit(Code) | | |
| JMLMethodSpec | | protected JMLMethodSpec()(Code) | | |
| addAssignable | | public void addAssignable(SetOfLocationDescriptor locations)(Code) | | |
| addOldQuantifiers | | public static Term addOldQuantifiers(Term a, Map term2old, boolean useQuantifiers, Namespace params)(Code) | | Applies the transformation tau_update to a iff
useQuantifiers == false or tau_old otherwise.
|
| clearModalityTermForEnsuresCache | | public void clearModalityTermForEnsuresCache()(Code) | | |
| containsQuantifiedAssignableLocation | | public boolean containsQuantifiedAssignableLocation()(Code) | | |
| createDLFormula | | public Term createDLFormula(boolean withPostInvariant, boolean allInvariants)(Code) | | Creates a DL formula from this method specification:
((pre & inv) -> [{methodbody}]post) & ((pre & inv & !diverges) -> <{methodbody}>post)
(This is the DL formula that is needed for an "ensured postcondition
proofobligation")
withInvariant: iff true the invariant of the containing typeis added to the postcondition which is needed for JMLPostAndInvPOs created by JMLMethodContracts. allInvariants: iff true all existing invariants for every existing type are added to the precondition (and postcondition if withInvariant is also true). |
| createDiverges | | protected Term createDiverges()(Code) | |
Parameters:
t1 - the precondition.
Parameters:
jb - the JavaBlock used in the modality. |
| createModalityTermForEnsures | | protected Term createModalityTermForEnsures(Term post, boolean desugar, boolean withInv, boolean allInv)(Code) | | |
| getAssignable | | public SetOfLocationDescriptor getAssignable()(Code) | | |
| getCompletePost | | public Term getCompletePost(boolean withClassSpec, boolean allInv)(Code) | | |
| getCompletePostFunctional | | public Term getCompletePostFunctional(boolean withClassSpec, boolean allInv)(Code) | | |
| getCompletePre | | public Term getCompletePre(boolean withClassSpec, boolean allInv, boolean terminationCase)(Code) | | returns the precondition + represents for model fields
(+ invariants iff withClassSpec = true, + the negation of the diverges
clause in order to retrieve a precondition under which the method must
terminate).
|
| getExceptionVariable | | public ProgramVariable getExceptionVariable()(Code) | | returns the ProgramVariable that is used for expressing the excetional
behavior of a method.
|
| getOldFuncSymbols | | public ListOfOperator getOldFuncSymbols()(Code) | | |
| getOldLVs | | public ListOfQuantifierPrefixEntry getOldLVs()(Code) | | |
| getPi1Functional | | public Term getPi1Functional()(Code) | | |
| getPost | | public Term getPost()(Code) | | returns the locally declared postcondition
|
| getPre | | public Term getPre()(Code) | | returns the locally declared precondition
|
| getSignals | | public SetOfSignals getSignals()(Code) | | |
| getSpecVars | | public ListOfNamed getSpecVars()(Code) | | |
| isCloneableFor | | public boolean isCloneableFor(ProgramMethod method)(Code) | | Checks if name, signature, accessibility and so on are equal for
this.pm and pm. If this.pm and pm occur on the same branch in the
class hierarchy must be checked somewhere else!
|
| replaceFreeVarsWithConsts | | public Term replaceFreeVarsWithConsts(Term t)(Code) | | |
| replaceModelFieldsInAssignable | | public SetOfLocationDescriptor replaceModelFieldsInAssignable()(Code) | | |
| replaceModelFieldsInAssignable | | public SetOfLocationDescriptor replaceModelFieldsInAssignable(JMLClassSpec cs)(Code) | | |
| setAssignableMode | | public void setAssignableMode(String s)(Code) | | |
| setId | | public void setId(int id)(Code) | | |
| setSpecVars | | public void setSpecVars(ListOfNamed svs)(Code) | | |
| terminates | | public boolean terminates()(Code) | | returns true if this specification demands termination of the method,
which means in this case that terminating by throwing an exception
is also considered to be a termination.
|
| updateParameters | | protected Term updateParameters(ArrayOfParameterDeclaration oldParams, ArrayOfParameterDeclaration newParams, Term target)(Code) | | |
| Methods inherited from de.uka.ilkd.key.logic.TermBuilder | public Term FALSE(Services services)(Code)(Java Doc)
public Term NULL(Services services)(Code)(Java Doc)
public Term TRUE(Services services)(Code)(Java Doc)
public Term all(QuantifiableVariable lv, Term t2)(Code)(Java Doc)
public Term all(QuantifiableVariable[] lv, Term t2)(Code)(Java Doc)
public Term and(Term t1, Term t2)(Code)(Java Doc)
public Term and(Term[] subTerms)(Code)(Java Doc)
public Term and(ListOfTerm subTerms)(Code)(Java Doc)
public Term array(Term ref, Term idx)(Code)(Java Doc)
public Term box(JavaBlock jb, Term t)(Code)(Java Doc)
public Term dia(JavaBlock jb, Term t)(Code)(Java Doc)
public Term dot(Term o, ProgramVariable a)(Code)(Java Doc)
public Term equals(Term t1, Term t2)(Code)(Java Doc)
public Term equiv(Term t1, Term t2)(Code)(Java Doc)
public Term ex(QuantifiableVariable lv, Term t2)(Code)(Java Doc)
public Term ex(QuantifiableVariable[] lv, Term t2)(Code)(Java Doc)
public Term ff()(Code)(Java Doc)
public Term func(TermSymbol op)(Code)(Java Doc)
public Term func(TermSymbol op, Term s)(Code)(Java Doc)
public Term func(TermSymbol op, Term s1, Term s2)(Code)(Java Doc)
public Term func(TermSymbol op, Term[] s)(Code)(Java Doc)
public Term geq(Term t1, Term t2, Services services)(Code)(Java Doc)
public Term gt(Term t1, Term t2, Services services)(Code)(Java Doc)
public Term ife(Term cond, Term _then, Term _else)(Code)(Java Doc)
public Term imp(Term t1, Term t2)(Code)(Java Doc)
public Term leq(Term t1, Term t2, Services services)(Code)(Java Doc)
public Term lt(Term t1, Term t2, Services services)(Code)(Java Doc)
public Term not(Term t)(Code)(Java Doc)
public Term one(Services services)(Code)(Java Doc)
public Term or(Term t1, Term t2)(Code)(Java Doc)
public Term or(Term[] subTerms)(Code)(Java Doc)
public Term or(ListOfTerm subTerms)(Code)(Java Doc)
public TermFactory tf()(Code)(Java Doc)
public Term tt()(Code)(Java Doc)
public Term var(LogicVariable v)(Code)(Java Doc)
public Term var(ProgramVariable v)(Code)(Java Doc)
public Term var(ParsableVariable v)(Code)(Java Doc)
public Term zTerm(Services services, String numberString)(Code)(Java Doc)
public Term zero(Services services)(Code)(Java Doc)
|
|
|