| java.lang.Object
 de.uka.ilkd.key.logic.TermBuilder
de.uka.ilkd.key.jml.JMLSpec
de.uka.ilkd.key.jml.JMLClassSpec
| JMLClassSpec | | public class JMLClassSpec extends JMLSpec (Code) | | wraps specifications that are valid for the entire class (e.g. invariants
or history constraints) or interface
|
| Method Summary | |
| public Term | addClassSpec2Post(Term post, boolean constraints, boolean invariants, ProgramMethod md, JMLClassSpec cSpec)
Adds invariants and history constraints to the postcondition iff md
isn't declared with the modifier helper. | | public Term | addClassSpec2Pre(Term pre, ProgramMethod md, JMLClassSpec cSpec)
Adds the applicable invariants of cSpec to the precondition of md
iff md isn't declared with the modifier helper. | | public void | addInstanceConstraint(Term t)
| | public void | addInstanceInvariant(Term t)
| | public void | addModelMethod(ProgramMethod pm)
| | public void | addModelVariable(ProgramVariable v)
| | public void | addRepresents(Term loc, Term rep)
adds the representation rep for the model variable
var. | | public void | addRepresents(ProgramVariable v, Term rep)
adds the representation rep for the model variable
var. | | public void | addStaticConstraint(Term t)
| | public void | addStaticInvariant(Term t)
| | public void | addSuchThat(Term t_loc, Term axiom)
| | public HashMap | buildModelMethod2Specs()
returns a mapping from modelmethods to their specifications. | | public boolean | containsInvOrConst()
| | public Term | getAllLocalInvariants()
Returns the Term ((self!=null & self.created=true) -> instanceInvariants
) & staticInvariants, which is sometimes needed in POs. | | public SetOfTerm | getAllQuantifiedInvariants()
| | public TypeDeclaration | getClassDeclaration()
returns the class or interfacedeclaration this specification refers to. | | public Term | getExTermForModelVar(Term modelVar, Term axiom)
generates \exists x . | | public Term | getInstanceConstraints()
| | public Term | getInstanceInvariants()
returns locally declared and inherited instance invariants. | | public ReferencePrefix | getInstancePrefix()
| | public Term | getLocalInstanceConstraints()
| | public Term | getLocalInstanceInvariants()
| | public Term | getLocalStaticConstraints()
| | public Term | getLocalStaticInvariants()
| | public Namespace | getModelMethods()
| | public Namespace | getModelVars()
| | public Term | getPreservesInvariantBehavior(ProgramMethod md, boolean allInv)
returns a term of the form inv -> <{try{ m();}catch(Exception e)}>inv
If allInv is true, inv is a conjunction of all
(static and instance) invariants of every existing type or just
the invariants of this type specification otherwise. | | public SetOfTerm | getQuantifiedInstanceInvariants()
| | public HashMap | getRepresents()
returns a HashMap that contains the locally defined and inherited
represents relations. | | public Services | getServices()
| | public Term | getStaticConstraints()
| | public Term | getStaticInvariants()
| | public ReferencePrefix | getStaticPrefix()
| | public LinkedHashMap | getTerm2Old()
| | protected Term | getTermForModelMethod(ProgramMethod pm)
| | public ProgramVariable | lookupModelField(Name name)
| | public ProgramMethod | lookupModelMethod(Name name)
| | public ProgramMethod | lookupModelMethodLocally(String name)
returns the model method with the name name,
iff it is loacally declared within the type that is specified by this
specification. | | public String | toString()
|
| staticInit | | protected boolean staticInit(Code) | | |
| addClassSpec2Post | | public Term addClassSpec2Post(Term post, boolean constraints, boolean invariants, ProgramMethod md, JMLClassSpec cSpec)(Code) | | Adds invariants and history constraints to the postcondition iff md
isn't declared with the modifier helper.
|
| addClassSpec2Pre | | public Term addClassSpec2Pre(Term pre, ProgramMethod md, JMLClassSpec cSpec)(Code) | | Adds the applicable invariants of cSpec to the precondition of md
iff md isn't declared with the modifier helper. md must be a member
method of cSpec.
|
| addInstanceConstraint | | public void addInstanceConstraint(Term t)(Code) | | |
| addInstanceInvariant | | public void addInstanceInvariant(Term t)(Code) | | |
| addRepresents | | public void addRepresents(Term loc, Term rep)(Code) | | adds the representation rep for the model variable
var.
|
| addRepresents | | public void addRepresents(ProgramVariable v, Term rep)(Code) | | adds the representation rep for the model variable
var.
|
| addStaticConstraint | | public void addStaticConstraint(Term t)(Code) | | |
| addStaticInvariant | | public void addStaticInvariant(Term t)(Code) | | |
| buildModelMethod2Specs | | public HashMap buildModelMethod2Specs()(Code) | | returns a mapping from modelmethods to their specifications.
|
| containsInvOrConst | | public boolean containsInvOrConst()(Code) | | |
| getAllLocalInvariants | | public Term getAllLocalInvariants()(Code) | | Returns the Term ((self!=null & self.created=true) -> instanceInvariants
) & staticInvariants, which is sometimes needed in POs.
|
| getAllQuantifiedInvariants | | public SetOfTerm getAllQuantifiedInvariants()(Code) | | |
| getClassDeclaration | | public TypeDeclaration getClassDeclaration()(Code) | | returns the class or interfacedeclaration this specification refers to.
|
| getExTermForModelVar | | public Term getExTermForModelVar(Term modelVar, Term axiom)(Code) | | generates \exists x . p(x) where p is the relation for
modelvar described by its represents-such_that clause.
|
| getInstanceConstraints | | public Term getInstanceConstraints()(Code) | | |
| getInstanceInvariants | | public Term getInstanceInvariants()(Code) | | returns locally declared and inherited instance invariants.
|
| getLocalInstanceConstraints | | public Term getLocalInstanceConstraints()(Code) | | |
| getLocalInstanceInvariants | | public Term getLocalInstanceInvariants()(Code) | | |
| getLocalStaticConstraints | | public Term getLocalStaticConstraints()(Code) | | |
| getLocalStaticInvariants | | public Term getLocalStaticInvariants()(Code) | | |
| getModelMethods | | public Namespace getModelMethods()(Code) | | returns the model methods declared in this class
|
| getModelVars | | public Namespace getModelVars()(Code) | | returns the model variables declared in this class
|
| getPreservesInvariantBehavior | | public Term getPreservesInvariantBehavior(ProgramMethod md, boolean allInv)(Code) | | returns a term of the form inv -> <{try{ m();}catch(Exception e)}>inv
If allInv is true, inv is a conjunction of all
(static and instance) invariants of every existing type or just
the invariants of this type specification otherwise.
|
| getQuantifiedInstanceInvariants | | public SetOfTerm getQuantifiedInstanceInvariants()(Code) | | |
| getRepresents | | public HashMap getRepresents()(Code) | | returns a HashMap that contains the locally defined and inherited
represents relations.
|
| getStaticConstraints | | public Term getStaticConstraints()(Code) | | |
| getStaticInvariants | | public Term getStaticInvariants()(Code) | | |
| lookupModelMethodLocally | | public ProgramMethod lookupModelMethodLocally(String name)(Code) | | returns the model method with the name name,
iff it is loacally declared within the type that is specified by this
specification.
|
| 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)
|
|
|