| Method Summary |
|
| public void | addAllMethodSpecs(Set set)
|
| public void | addClassSpec(JMLClassSpec cs)
checks whether the methods annotated with the pureModifier really
have no side effect. |
| public void | addLoopSpec(LoopInvariant l)
|
| public void | addMethodSpec(JMLMethodSpec ms)
|
| public void | addModifier(ProgramMethod md, String modifier)
|
| public Term | allInvariants()
returns the conjunction of all existing class invariants. |
| public void | clearSpecsForLoop(LoopStatement ls)
|
| public void | clearSpecsForMethod(ProgramMethod md)
Removes the specifications for md. |
| public Implementation2SpecMap | copy(Services serv)
|
| public void | createLoopAnnotations()
Creates LoopInvariantAnnotations from the parsed loop specifications and
adds them to the correcponding loop statements. |
| public boolean | equals(Object o)
|
| public ListOfKeYJavaType | findSpecifications(String name, KeYJavaType classType)
returns a list of KeYJavaTypes, that contain a specification for the
method with the name name, in depth first order. |
| public Set | getAllClasses()
returns all classtypes in this map. |
| public Namespace | getAllInvPVNS()
|
| public Set | getAllMethods()
returns all methoddeclarations in this map. |
| public SetOfJMLMethodSpec | getInheritedMethodSpecs(ProgramMethod md, KeYJavaType classType)
|
| public SetOfString | getModifiers(ProgramMethod md)
|
| public JMLClassSpec | getSpecForClass(KeYJavaType classType)
|
| public LoopInvariant | getSpecForLoop(LoopStatement ls)
|
| public SetOfJMLMethodSpec | getSpecsForMethod(ProgramMethod md)
|
| public int | hashCode()
|
| public ProgramVariable | lookupModelField(KeYJavaType classType, String fieldName)
returns the field fieldName if such an attribute is
declared in classType, null otherwise. |
| public ProgramMethod | lookupModelMethod(KeYJavaType classType, Name methodName)
returns the method methodName if such a method is declared
in classType, null otherwise. |
| public void | removeClassSpec(JMLClassSpec cs)
|
| public void | removeMethodSpec(JMLMethodSpec ms)
|
| public void | setAllInvPVNS(Namespace ns)
|
| public void | setAllInvariants(Term inv)
|
| public void | setPure(KeYJavaType kjt, NamespaceSet nss, String javaPath)
|
