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.gui;
012:
013: import java.awt.Color;
014: import java.awt.Component;
015: import java.awt.event.ActionEvent;
016: import java.awt.event.ActionListener;
017: import java.util.HashMap;
018: import java.util.Iterator;
019: import java.util.LinkedHashMap;
020: import java.util.Vector;
021:
022: import javax.swing.*;
023: import javax.swing.border.TitledBorder;
024: import javax.swing.event.ListSelectionEvent;
025: import javax.swing.event.ListSelectionListener;
026: import javax.swing.event.TreeSelectionEvent;
027: import javax.swing.event.TreeSelectionListener;
028: import javax.swing.tree.DefaultMutableTreeNode;
029: import javax.swing.tree.DefaultTreeModel;
030: import javax.swing.tree.MutableTreeNode;
031: import javax.swing.tree.TreeModel;
032:
033: import de.uka.ilkd.key.java.JavaInfo;
034: import de.uka.ilkd.key.java.Services;
035: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
036: import de.uka.ilkd.key.java.declaration.InterfaceDeclaration;
037: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
038: import de.uka.ilkd.key.java.recoderext.ClassInitializeMethodBuilder;
039: import de.uka.ilkd.key.jml.*;
040: import de.uka.ilkd.key.logic.NamespaceSet;
041: import de.uka.ilkd.key.logic.op.IteratorOfProgramMethod;
042: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
043: import de.uka.ilkd.key.logic.op.ProgramMethod;
044: import de.uka.ilkd.key.proof.init.*;
045:
046: public class JMLSpecBrowser extends JDialog {
047:
048: /** the package hierarchy as a tree */
049: private JTree packageHierarchy;
050:
051: private JList methodList;
052: private JList poList;
053:
054: private JCheckBox allInv;
055: private JCheckBox invPost;
056:
057: private Implementation2SpecMap ism;
058:
059: /** true if the JMLSpecBrowser was invoked by Main and we already have
060: * a proofenvironment for the javaModel we are dealing with.
061: */
062: private boolean envMode = true;
063:
064: private KeYMediator mediator;
065: private Services services;
066:
067: private JMLProofOblInput poi = null;
068:
069: private String javaPath = "";
070:
071: private Object[] emptyArray = new Object[0];
072:
073: private TreeModel treeModel;
074:
075: private static HashMap ism2browser = new HashMap();
076:
077: private boolean inheritedMethods = false;
078:
079: //the selected class
080: private KeYJavaType classType = null;
081:
082: private JMLSpecBrowser(KeYMediator mediator) {
083: super (new JFrame(), "JML Specification Browser", true);
084: this .services = mediator.getServices();
085: ism = services.getImplementation2SpecMap();
086: this .mediator = mediator;
087: this .javaPath = mediator.getProof().env().getJavaModel()
088: .getModelDir();
089: buildTreeModel();
090: layoutJMLSpecBrowser();
091: pack();
092: setLocation(70, 70);
093: setVisible(true);
094: }
095:
096: public JMLSpecBrowser(Services services, String javaPath) {
097: super (new JFrame(), "JML Specification Browser", true);
098: this .services = services;
099: ism = services.getImplementation2SpecMap();
100: this .javaPath = javaPath;
101: envMode = false;
102: buildTreeModel();
103: layoutJMLSpecBrowser();
104: pack();
105: setLocation(70, 70);
106: setVisible(true);
107: ism2browser.put(services.getImplementation2SpecMap(), this );
108: }
109:
110: public static JMLSpecBrowser getJMLSpecBrowser(KeYMediator mediator) {
111: JMLSpecBrowser browser = (JMLSpecBrowser) ism2browser
112: .get(mediator.getServices().getImplementation2SpecMap());
113: if (browser == null) {
114: browser = new JMLSpecBrowser(mediator);
115: ism2browser.put(mediator.getServices()
116: .getImplementation2SpecMap(), browser);
117: }
118: browser.envMode = true;
119: browser.mediator = mediator;
120: browser.setModal(true);
121: browser.setVisible(true);
122: return browser;
123: }
124:
125: /**
126: * builds a TreeModel from the package structure of the Java model.
127: */
128: private void buildTreeModel() {
129: JavaInfo ji = services.getJavaInfo();
130: HashMap package2Node = new HashMap();
131: DefaultMutableTreeNode root = new DefaultMutableTreeNode("");
132: // ism.checkPurity();
133:
134: Iterator it = ism.getAllClasses().iterator();
135: while (it.hasNext()) {
136: KeYJavaType kjt = (KeYJavaType) it.next();
137: String name = ji.getFullName(kjt);
138: if (name.lastIndexOf(".") != -1) {
139: DefaultMutableTreeNode parent = treeHelper(name
140: .substring(0, name.lastIndexOf(".")),
141: package2Node, root);
142: parent.add(new DefaultMutableTreeNode(kjt) {
143: public String toString() {
144: final String sortName = ((KeYJavaType) userObject)
145: .getSort().toString();
146: return sortName.substring(sortName
147: .lastIndexOf(".") + 1);
148: }
149: });
150: } else {
151: root.add(new DefaultMutableTreeNode(kjt) {
152: public String toString() {
153: return ((KeYJavaType) userObject).getSort()
154: .toString();
155: }
156: });
157: }
158: }
159: sortTree(root);
160: if (root.getChildCount() == 1) {
161: treeModel = new DefaultTreeModel(root.getFirstChild());
162: } else {
163: treeModel = new DefaultTreeModel(root);
164: }
165: packageHierarchy = new JTree(treeModel);
166: packageHierarchy
167: .addTreeSelectionListener(new GUIPackageTreeSelectionListener());
168: }
169:
170: private void sortTree(DefaultMutableTreeNode root) {
171: for (int i = 0; i < root.getChildCount(); i++) {
172: sortTree((DefaultMutableTreeNode) root.getChildAt(i));
173: }
174: boolean changed = true;
175: while (changed) {
176: changed = false;
177: for (int i = 0; i < root.getChildCount() - 1; i++) {
178: if (root.getChildAt(i).toString().compareTo(
179: root.getChildAt(i + 1).toString()) > 0) {
180: changed = true;
181: root.insert((MutableTreeNode) root
182: .getChildAt(i + 1), i);
183: }
184: }
185: }
186: }
187:
188: private DefaultMutableTreeNode treeHelper(String pname,
189: HashMap p2n, DefaultMutableTreeNode root) {
190: if (p2n.get(pname) != null) {
191: return (DefaultMutableTreeNode) p2n.get(pname);
192: } else {
193: final int dot = pname.lastIndexOf(".");
194: DefaultMutableTreeNode node = new DefaultMutableTreeNode(
195: pname) {
196: public String toString() {
197: return userObject.toString().substring(dot + 1);
198: }
199: };
200: p2n.put(pname, node);
201: if (dot != -1) {
202: DefaultMutableTreeNode parent = treeHelper(pname
203: .substring(0, dot), p2n, root);
204: parent.add(node);
205: } else {
206: root.add(node);
207: }
208: return node;
209: }
210: }
211:
212: /** layout */
213: protected void layoutJMLSpecBrowser() {
214: JScrollPane classListScroll = new JScrollPane(
215: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
216: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
217: classListScroll.getViewport().setView(packageHierarchy);
218: classListScroll.setBorder(new TitledBorder("Classes"));
219:
220: methodList = new JList();
221: JPanel methodPanel = new JPanel();
222: methodPanel.setLayout(new BoxLayout(methodPanel,
223: BoxLayout.PAGE_AXIS));
224: final JButton hide = new JButton(
225: inheritedMethods ? "Hide Inherited Methods"
226: : "Show Inherited Methods");
227: hide.addActionListener(new ActionListener() {
228: public void actionPerformed(ActionEvent e) {
229: inheritedMethods = !inheritedMethods;
230: hide
231: .setText(inheritedMethods ? "Hide Inherited Methods"
232: : "Show Inherited Methods");
233: updateMethodList(classType);
234: }
235:
236: });
237: methodList
238: .addListSelectionListener(new ListSelectionListener() {
239: public void valueChanged(ListSelectionEvent e) {
240: setPOList();
241: }
242: });
243: methodList.setCellRenderer(new DefaultListCellRenderer() {
244: public Component getListCellRendererComponent(JList list,
245: Object value, int index, boolean isSelected,
246: boolean cellHasFocus) {
247: if (value != null) {
248: ProgramMethod pm = (ProgramMethod) value;
249: MethodDeclaration md = pm.getMethodDeclaration();
250: String params = md.getParameters().toString();
251: setText((md.getTypeReference() == null ? "void"
252: : md.getTypeReference().getName())
253: + " "
254: + md.getFullName()
255: + "("
256: + params.substring(1, params.length() - 1)
257: + ")");
258: if (isSelected) {
259: setBackground(list.getSelectionBackground());
260: setForeground(list.getSelectionForeground());
261: } else {
262: setBackground(list.getBackground());
263: setForeground(list.getForeground());
264: }
265: setEnabled(list.isEnabled());
266: setFont(list.getFont());
267: setOpaque(true);
268: }
269: return this ;
270: }
271: });
272: JScrollPane methodListScroll = new JScrollPane(
273: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
274: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
275: methodListScroll.getViewport().setView(methodList);
276: methodListScroll.setBorder(new TitledBorder("Methods"));
277:
278: poList = new JList();
279:
280: poList.setCellRenderer(new TextAreaRenderer());
281: JScrollPane poListScroll = new JScrollPane(
282: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
283: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
284: poListScroll.getViewport().setView(poList);
285: poListScroll.setBorder(new TitledBorder("Proof Obligations"));
286:
287: JPanel buttonPanel = new JPanel();
288:
289: JPanel optionPanel = new JPanel();
290: optionPanel.setLayout(new BoxLayout(optionPanel,
291: BoxLayout.Y_AXIS));
292: buttonPanel.add(optionPanel);
293:
294: allInv = new JCheckBox("Use all applicable invariants");
295: allInv.setToolTipText("<html><pre>"
296: + "If selected, the POs change to that effect,<br>"
297: + "that every invariant of every class is added\n"
298: + "to the precondition in the case of method\n"
299: + "specification POs, or to the pre- and\n"
300: + "postcondition in the case of invariant POs.\n "
301: + " This changes the semantics of the invariant\n"
302: + "PO to that extend that it now expresses that\n"
303: + "the method preserves every invariant of every"
304: + "\nexisting object and type.\n"
305: + " The effect on method spec POs is that they\n"
306: + "are then reflecting the fact that a method\n"
307: + "can assume all invariants of every existing\n"
308: + "object and type to hold in its prestate.\n"
309: + "Assuming all invariants to hold in the\n"
310: + "prestate of a certain method is often not\n"
311: + "necessary when proving its specification!"
312: + "</pre>");
313: optionPanel.add(allInv);
314: allInv.addActionListener(new ActionListener() {
315: public void actionPerformed(ActionEvent e) {
316: setPOList();
317: }
318: });
319:
320: invPost = new JCheckBox("Add invariants to postcondition");
321: invPost.setToolTipText("<html><pre>"
322: + "If selected the history constraints and\n"
323: + "invariants of the current class are added\n"
324: + "to the postcondition of the method speccase PO\n"
325: + "(this is the case if \"Use all applicable\n"
326: + "invariants\" is not selected otherwise also\n"
327: + "the invariants of every other class are added)"
328: + "</pre>");
329: optionPanel.add(invPost);
330:
331: JButton lo = new JButton("Load Proof Obligation");
332: lo.addActionListener(new ActionListener() {
333: public void actionPerformed(ActionEvent e) {
334: if (poList.getSelectedValue() == null) {
335: JOptionPane.showMessageDialog(null,
336: "Please select the PO you wish to load!",
337: "Which Proof Obligation?",
338: JOptionPane.ERROR_MESSAGE);
339: } else {
340: createProofObl();
341: setVisible(false);
342: setModal(false);
343: // dispose();
344: }
345: }
346: });
347: buttonPanel.add(lo);
348: JButton cancel = new JButton("Cancel");
349: cancel.addActionListener(new ActionListener() {
350: public void actionPerformed(ActionEvent e) {
351: setVisible(false);
352: setModal(false);
353: // dispose();
354: }
355: });
356: buttonPanel.add(cancel);
357:
358: java.awt.Dimension paneDim = new java.awt.Dimension(220, 400);
359: classListScroll.setPreferredSize(paneDim);
360: classListScroll.setMinimumSize(paneDim);
361: methodListScroll.setMinimumSize(paneDim);
362: methodListScroll.setPreferredSize(paneDim);
363: paneDim = new java.awt.Dimension(370, 400);
364: poListScroll.setMinimumSize(paneDim);
365: poListScroll.setPreferredSize(paneDim);
366: methodPanel.add(hide);
367: methodPanel.add(methodListScroll);
368:
369: JPanel listPanel = new JPanel();
370: listPanel.setLayout(new BoxLayout(listPanel, BoxLayout.X_AXIS));
371: listPanel.add(classListScroll);
372: listPanel.add(methodPanel);
373: listPanel.add(poListScroll);
374:
375: getContentPane().setLayout(
376: new BoxLayout(getContentPane(), BoxLayout.Y_AXIS));
377: getContentPane().add(listPanel);
378: getContentPane().add(buttonPanel);
379: }
380:
381: /**
382: * Sets a new proof obligation list (when the selected method has changed
383: * for example)
384: */
385: private void setPOList() {
386: ProgramMethod m = (ProgramMethod) methodList.getSelectedValue();
387: poList.setListData(emptyArray);
388: if (m != null
389: && !m.isAbstract()
390: && !(classType.getJavaType() instanceof InterfaceDeclaration)) {
391: SetOfJMLMethodSpec specs = ism.getSpecsForMethod(m);
392: JMLClassSpec cSpec = ism.getSpecForClass(classType);
393: if (specs != null) {
394: specs = specs.union(ism.getInheritedMethodSpecs(m,
395: classType));
396: } else {
397: specs = ism.getInheritedMethodSpecs(m, classType);
398: }
399: IteratorOfJMLMethodSpec mit = specs.iterator();
400: specs = SetAsListOfJMLMethodSpec.EMPTY_SET;
401: boolean pureFound = false;
402: boolean pureInh = false;
403: while (mit.hasNext()) {
404: JMLMethodSpec s = mit.next();
405: if (s instanceof JMLPuritySpec) {
406: pureFound = true;
407: }
408: if (services.getJavaInfo().getKeYJavaType(
409: s.getClassDeclaration()) == classType) {
410: specs = specs.add(s);
411: }
412: }
413: if (pureInh && !pureFound) {
414: specs = specs.add(new JMLPuritySpec(m, services,
415: UsefulTools.buildParamNamespace(m
416: .getMethodDeclaration()),
417: new LinkedHashMap(), ism
418: .getSpecForClass(classType),
419: new NamespaceSet(), javaPath));
420: }
421: if (specs != SetAsListOfJMLMethodSpec.EMPTY_SET
422: || cSpec != null) {
423: Vector specVector = new Vector();
424: if (specs != null) {
425: IteratorOfJMLMethodSpec it = specs.iterator();
426: while (it.hasNext()) {
427: JMLMethodSpec mSpec = it.next();
428: specVector.add(mSpec);
429: if (mSpec.replaceModelFieldsInAssignable() != null
430: && !JMLMethodSpec.EVERYTHING
431: .equals(mSpec
432: .getAssignableMode()) &&
433: // !mSpec.containsQuantifiedAssignableLocation() &&
434: mSpec.isValid()) {
435: specVector
436: .add(new AssignableCheckProofOblInput(
437: mSpec, javaPath));
438: }
439: }
440: }
441: if (cSpec != null
442: && (cSpec.containsInvOrConst() || allInv
443: .isSelected())) {
444: specVector.add(cSpec);
445: }
446: poList.setListData(specVector);
447: }
448: }
449: }
450:
451: /**
452: * creates a JMLProofOblInput and starts the proofer.
453: */
454: private void createProofObl() {
455: Object spec = poList.getSelectedValue();
456: if (spec instanceof JMLMethodSpec) {
457: if (invPost.isSelected()) {
458: poi = new JMLPostAndInvPO((JMLMethodSpec) spec,
459: javaPath, allInv.isSelected());
460: } else {
461: poi = new JMLPostPO((JMLMethodSpec) spec, javaPath,
462: allInv.isSelected());
463: }
464: } else if (spec instanceof JMLClassSpec) {
465: poi = new JMLInvPO((JMLClassSpec) spec,
466: (ProgramMethod) methodList.getSelectedValue(),
467: javaPath, allInv.isSelected());
468: } else if (spec instanceof AssignableCheckProofOblInput) {
469: poi = (AssignableCheckProofOblInput) spec;
470: ((AssignableCheckProofOblInput) poi)
471: .setAllInvariants(allInv.isSelected());
472: }
473: if (envMode) {
474: ProblemInitializer pi = new ProblemInitializer(Main
475: .getInstance());
476: try {
477: pi.startProver(mediator.getProof().env(), poi);
478: } catch (ProofInputException e) {
479: //too bad
480: }
481: }
482: }
483:
484: public JMLProofOblInput getPOI() {
485: return poi;
486: }
487:
488: class GUIPackageTreeSelectionListener implements
489: TreeSelectionListener, java.io.Serializable {
490: /**
491: * Sets a new methodlist if the selection in the package tree has
492: * changed and the selected value is a class.
493: */
494: public void valueChanged(TreeSelectionEvent e) {
495: Object o = ((DefaultMutableTreeNode) e.getPath()
496: .getLastPathComponent()).getUserObject();
497: if (o instanceof KeYJavaType) {
498: updateMethodList((KeYJavaType) o);
499: }
500: }
501: }
502:
503: private void updateMethodList(KeYJavaType kjt) {
504: if (kjt != null) {
505: classType = kjt;
506: ListOfProgramMethod l = inheritedMethods ? services
507: .getJavaInfo().getAllProgramMethods(classType)
508: : services.getJavaInfo().getKeYProgModelInfo()
509: .getAllProgramMethodsLocallyDeclared(
510: classType);
511: Vector mVector = new Vector();
512: IteratorOfProgramMethod it = l.iterator();
513: while (it.hasNext()) {
514: ProgramMethod pm = it.next();
515: MethodDeclaration md = pm.getMethodDeclaration();
516: if (!md.getName().startsWith("<")
517: || md
518: .getName()
519: .equals(
520: ClassInitializeMethodBuilder.CLASS_INITIALIZE_IDENTIFIER)) {
521: addOrdered(mVector, pm);
522: }
523: }
524: ListOfProgramMethod ml = services.getJavaInfo()
525: .getKeYProgModelInfo().getConstructors(classType);
526: IteratorOfProgramMethod mit = ml.iterator();
527: while (mit.hasNext()) {
528: addOrdered(mVector, mit.next());
529: }
530: methodList.setListData(mVector);
531: }
532: }
533:
534: private void addOrdered(Vector v, ProgramMethod m) {
535: for (int i = 0; i < v.size(); i++) {
536: if (m.getName().compareTo(
537: ((ProgramMethod) v.get(i)).getName()) < 0) {
538: v.add(i, m);
539: return;
540: }
541: }
542: v.add(m);
543: }
544:
545: class TextAreaRenderer extends JTextArea implements
546: ListCellRenderer {
547:
548: private Color getColor(Object o) {
549: if (o instanceof JMLNormalMethodSpec) {
550: return new Color(230, 255, 230);
551: } else if (o instanceof JMLExceptionalMethodSpec) {
552: return new Color(255, 210, 210);
553: } else if (o instanceof JMLMethodSpec) {
554: return Color.LIGHT_GRAY;
555: } else if (o instanceof AssignableCheckProofOblInput) {
556: return new Color(255, 255, 190);
557: } else {
558: return new Color(230, 230, 255);
559: }
560: }
561:
562: public TextAreaRenderer() {
563: setLineWrap(false);
564: setWrapStyleWord(false);
565: }
566:
567: public Component getListCellRendererComponent(JList list,
568: Object value, int index, boolean isSelected,
569: boolean cellHasFocus) {
570: setText(value.toString());
571: if ((value instanceof JMLSpec)
572: && !((JMLSpec) value).isValid()) {
573: setBackground(Color.DARK_GRAY);
574: setForeground(Color.GRAY);
575: setEnabled(false);
576: } else {
577: setBackground(isSelected ? Color.BLACK
578: : getColor(value));
579: setForeground(isSelected ? Color.WHITE : Color.BLACK);
580: setEnabled(true);
581: }
582: return this;
583: }
584: }
585:
586: }
|