001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof.mgt;
012:
013: import java.util.*;
014:
015: import de.uka.ilkd.key.casetool.ModelMethod;
016: import de.uka.ilkd.key.java.JavaInfo;
017: import de.uka.ilkd.key.java.Services;
018: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
019: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
020: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
021: import de.uka.ilkd.key.jml.JMLClassSpec;
022: import de.uka.ilkd.key.logic.IteratorOfTerm;
023: import de.uka.ilkd.key.logic.SetOfTerm;
024: import de.uka.ilkd.key.logic.Term;
025: import de.uka.ilkd.key.logic.op.IteratorOfProgramMethod;
026: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
027: import de.uka.ilkd.key.logic.op.Modality;
028: import de.uka.ilkd.key.logic.op.ProgramMethod;
029: import de.uka.ilkd.key.proof.ProofAggregate;
030: import de.uka.ilkd.key.speclang.ClassInvariant;
031: import de.uka.ilkd.key.speclang.ListOfClassInvariant;
032: import de.uka.ilkd.key.speclang.SLListOfClassInvariant;
033: import de.uka.ilkd.key.speclang.TranslatedClassInvariant;
034:
035: /**
036: * The repository where all specification (contracts) of a proof
037: * environment are contained. An instance must belong to only one
038: * {@link ProofEnvironment}.
039: */
040: public class SpecificationRepository {
041:
042: private Map contracts = new HashMap();
043: private LinkedHashMap invariants = null;
044: private Services services;
045:
046: public SpecificationRepository(Services services) {
047: this .services = services;
048: }
049:
050: // TODO: ensure fixed order (?)
051: private void createClassInvariants() {
052: final SortedSet allClassesSorted = new TreeSet(
053: new KeYJavaType.LexicographicalKeYJavaTypeOrder());
054: allClassesSorted.addAll(services.getJavaInfo()
055: .getAllKeYJavaTypes());
056:
057: final Iterator it = allClassesSorted.iterator();
058: invariants = new LinkedHashMap();
059: while (it.hasNext()) {
060: final KeYJavaType kjt = (KeYJavaType) it.next();
061: final JMLClassSpec jmlcs = services
062: .getImplementation2SpecMap().getSpecForClass(kjt);
063: if (jmlcs != null) {
064: SetOfTerm terms = jmlcs.getAllQuantifiedInvariants();
065: IteratorOfTerm it2 = terms.iterator();
066: while (it2.hasNext()) {
067: Term t = it2.next();
068: if (t != null) {
069: ClassInvariant inv = new TranslatedClassInvariant(
070: new JavaModelClass(kjt, services
071: .getJavaInfo()
072: .getJavaSourcePath(), services),
073: t, services);
074: ListOfClassInvariant invs = (ListOfClassInvariant) invariants
075: .get(kjt);
076: if (invs == null) {
077: invs = SLListOfClassInvariant.EMPTY_LIST;
078: }
079: invariants.put(kjt, invs.prepend(inv));
080: }
081: }
082: }
083: }
084: }
085:
086: /** returns an iterator of specifications ({@link Contract})
087: * contained in this repository. Modifications to the underlying
088: * set are not allowed.
089: */
090: public Iterator getSpecs() {
091: return contracts.values().iterator();
092: }
093:
094: public Contract getContractByName(String name) {
095: Iterator it = contracts.entrySet().iterator();
096: while (it.hasNext()) {
097: Contract ct = (Contract) ((ContractSet) ((Map.Entry) it
098: .next()).getValue()).iterator().next();
099: if (ct.getName().equals(name)) {
100: return ct;
101: }
102: }
103: return null;
104: }
105:
106: /** returns a set of contracts with the argument as identifying
107: * contracted object.
108: */
109: public ContractSet getContract(Object objOfContract) {
110: Object o = objOfContract;
111: if (objOfContract instanceof ModelMethod) {
112: o = convertToProgramMethod((ModelMethod) objOfContract);
113: }
114: return (ContractSet) contracts.get(o);
115: }
116:
117: /** returns a set of contracts with one of the elements in
118: * the argument list as identifying contracted object.
119: */
120: public ContractSet getContracts(ListOfProgramMethod objsOfContract,
121: Modality modality) {
122: ContractSet ctSet = new ContractSet();
123: IteratorOfProgramMethod it = objsOfContract.iterator();
124: while (it.hasNext()) {
125: ContractSet cs = getContract(it.next());
126: if (cs != null) {
127: ctSet.addAll(cs.getMethodContracts(modality));
128: }
129: }
130: return ctSet;
131: }
132:
133: /** returns a set of contracts with the argument as identifying
134: * contracted object.
135: */
136: public ContractSet getContract(Object objOfContract,
137: Modality modality) {
138: ContractSet ctSet = getContract(objOfContract);
139: if (ctSet == null) {
140: return new ContractSet();
141: }
142: ctSet = ctSet.getMethodContracts(modality);
143: if (ctSet == null) {
144: return new ContractSet();
145: }
146: return ctSet;
147: }
148:
149: /** adds a contract to this specification repository.
150: */
151: public Contract add(Contract ct) {
152: Object o = ct.getObjectOfContract();
153: if (o instanceof ModelMethod) {
154: o = convertToProgramMethod((ModelMethod) o);
155: }
156: ContractSet cs = (ContractSet) contracts.get(o);
157: if (cs == null) {
158: cs = new ContractSet();
159: contracts.put(o, cs);
160: }
161: return cs.add(ct);
162: }
163:
164: public void removeProofList(ProofAggregate pl) {
165: Iterator it = getSpecs();
166: while (it.hasNext()) {
167: Object o = it.next();
168: ((ContractSet) o).removeProofList(pl);
169: }
170: }
171:
172: public ListOfClassInvariant getAllInvariantsForType(KeYJavaType kjt) {
173: if (invariants == null) {
174: createClassInvariants();
175: }
176: return invariants.containsKey(kjt) ? (ListOfClassInvariant) invariants
177: .get(kjt)
178: : SLListOfClassInvariant.EMPTY_LIST;
179: }
180:
181: public SpecificationRepository copy(Services s) {
182: final SpecificationRepository res = new SpecificationRepository(
183: s);
184: res.contracts = this .contracts; //TODO deepcopy
185: res.invariants = this .invariants; //TODO
186: return res;
187: }
188:
189: //------------------------ Helper methods -----------------------------//
190:
191: private ProgramMethod convertToProgramMethod(ModelMethod m) {
192: JavaInfo javaInfo = services.getJavaInfo();
193: KeYJavaType containingClass = javaInfo
194: .getKeYJavaTypeByClassName(m.getContainingClassName());
195: String name = m.getName();
196:
197: ListOfKeYJavaType signature = SLListOfKeYJavaType.EMPTY_LIST;
198: for (int i = 0; i < m.getNumParameters(); i++) {
199: signature = signature.append(javaInfo.getKeYJavaType(m
200: .getParameterTypeAt(i)));
201: }
202:
203: return javaInfo.getProgramMethod(containingClass, name,
204: signature, javaInfo.getJavaLangObject());
205: }
206:
207: }
|