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: package de.uka.ilkd.key.gui;
010:
011: import java.awt.Dimension;
012: import java.awt.FlowLayout;
013: import java.awt.Font;
014: import java.awt.event.ActionEvent;
015: import java.awt.event.ActionListener;
016:
017: import javax.swing.*;
018: import javax.swing.border.TitledBorder;
019: import javax.swing.event.ListSelectionEvent;
020: import javax.swing.event.ListSelectionListener;
021:
022: import de.uka.ilkd.key.casetool.ModelClass;
023: import de.uka.ilkd.key.casetool.ModelMethod;
024: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
025: import de.uka.ilkd.key.logic.op.Modality;
026: import de.uka.ilkd.key.proof.mgt.ContractSet;
027: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
028: import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
029: import de.uka.ilkd.key.rule.ContractConfigurator;
030: import de.uka.ilkd.key.speclang.IteratorOfClassInvariant;
031: import de.uka.ilkd.key.speclang.ListOfClassInvariant;
032: import de.uka.ilkd.key.speclang.SLListOfClassInvariant;
033:
034: public class DefaultContractConfigurator extends JDialog implements
035: ContractConfigurator {
036:
037: private SpecificationRepository repos;
038: private OldOperationContract base;
039: private Modality modality;
040: private ListOfClassInvariant preInvs = SLListOfClassInvariant.EMPTY_LIST;
041: private ListOfClassInvariant postInvs = SLListOfClassInvariant.EMPTY_LIST;
042: private ListOfProgramMethod programMethods;
043: private boolean successful;
044: private JEditorPane contractTextArea;
045: private boolean allowConfig;
046:
047: public DefaultContractConfigurator(String title, JFrame parent) {
048: super (parent, title, true);
049: }
050:
051: public void setSpecification(SpecificationRepository repos) {
052: this .repos = repos;
053: }
054:
055: public void setProgramMethods(ListOfProgramMethod pm) {
056: this .programMethods = pm;
057: }
058:
059: public void setModality(Modality modality) {
060: this .modality = modality;
061: }
062:
063: public void start() {
064: getContentPane().removeAll();
065: ContractSet ctSet = repos
066: .getContracts(programMethods, modality);
067: ModelMethod mm = ((OldOperationContract) ctSet.iterator()
068: .next()).getModelMethod();
069: ModelClass mc = mm.getContainingClass();
070: final ClassInvariantSelectionPanel selectionPanelPre = new ClassInvariantSelectionPanel(
071: mc.getAllClasses(), false, mc, false);
072: final ClassInvariantSelectionPanel selectionPanelPost = new ClassInvariantSelectionPanel(
073: mc.getAllClasses(), false, mc, false);
074: ContractSelectionPanel contractSelectionPanel = new ContractSelectionPanel(
075: ctSet, false);
076:
077: contractSelectionPanel
078: .addListSelectionListener(new ContractListSelectionListener(
079: this ));
080:
081: JComponent tabs;
082: if (allowConfig) {
083: tabs = new JTabbedPane();
084: ((JTabbedPane) tabs).addTab("Base Contract",
085: new JScrollPane(contractSelectionPanel));
086: ((JTabbedPane) tabs).addTab("Assumed Invariants",
087: selectionPanelPre);
088: ((JTabbedPane) tabs).addTab("Ensured Invariants",
089: selectionPanelPost);
090: } else {
091: tabs = new JScrollPane(contractSelectionPanel);
092: }
093: tabs.setPreferredSize(new Dimension(800, 500));
094: getContentPane().setLayout(
095: new BoxLayout(getContentPane(), BoxLayout.Y_AXIS));
096:
097: contractTextArea = new JEditorPane("text/html", "Contract");
098: contractTextArea.setEditable(false);
099: final Font contractTextAreaFont = contractTextArea.getFont()
100: .deriveFont(Font.PLAIN, 10);
101: contractTextArea.setFont(contractTextAreaFont);
102: JScrollPane scrollPane = new JScrollPane(contractTextArea);
103: scrollPane.setPreferredSize(new Dimension(200, 150));
104: scrollPane.setBorder(new TitledBorder("Configured Contract"));
105:
106: JSplitPane splitPane = new JSplitPane(
107: JSplitPane.VERTICAL_SPLIT, tabs, scrollPane);
108: splitPane.setResizeWeight(.75);
109: splitPane.setDividerLocation(.75);
110: splitPane.resetToPreferredSizes();
111: getContentPane().add(splitPane);
112:
113: JPanel buttons = new JPanel();
114: buttons.setLayout(new FlowLayout(FlowLayout.RIGHT, 5, 5));
115: buttons.setPreferredSize(new Dimension(400, 40));
116:
117: Dimension buttonDim = new Dimension(95, 25);
118:
119: // create "ok" button
120: JButton okButton = new JButton("OK");
121: okButton.setPreferredSize(buttonDim);
122: okButton.setMinimumSize(buttonDim);
123: okButton.addActionListener(new ActionListener() {
124: public void actionPerformed(ActionEvent e) {
125: successful = true;
126: setVisible(false);
127: }
128: });
129: buttons.add(okButton);
130: getRootPane().setDefaultButton(okButton);
131:
132: //create "cancel" button
133: JButton cancelButton = new JButton("Cancel");
134: cancelButton.setPreferredSize(buttonDim);
135: cancelButton.setMinimumSize(buttonDim);
136: cancelButton.addActionListener(new ActionListener() {
137: public void actionPerformed(ActionEvent e) {
138: setVisible(false);
139: }
140: });
141: buttons.add(cancelButton);
142:
143: getContentPane().add(buttons);
144:
145: selectionPanelPre
146: .addInvariantSelectionListener(new ListSelectionListener() {
147: public void valueChanged(ListSelectionEvent e) {
148: setPreInvs(selectionPanelPre
149: .getClassInvariants());
150: }
151: });
152:
153: selectionPanelPost
154: .addInvariantSelectionListener(new ListSelectionListener() {
155: public void valueChanged(ListSelectionEvent e) {
156: setPostInvs(selectionPanelPost
157: .getClassInvariants());
158: }
159: });
160:
161: updateContractWithBase((OldOperationContract) contractSelectionPanel
162: .getCurrentSelection());
163: setPostInvs(selectionPanelPost.getClassInvariants());
164: setPreInvs(selectionPanelPre.getClassInvariants());
165:
166: pack();
167: setVisible(true);
168: }
169:
170: public OldOperationContract getMethodContract() {
171: return base;
172: }
173:
174: public ListOfClassInvariant getPreInvariants() {
175: return preInvs;
176: }
177:
178: public ListOfClassInvariant getPostInvariants() {
179: return postInvs;
180: }
181:
182: public boolean wasSuccessful() {
183: return successful;
184: }
185:
186: public void updateDisplay() {
187: StringBuffer sb = new StringBuffer();
188: sb
189: .append("<html><p style=\"font-family: lucida;font-size: 11pt\"><b>pre:</b> "
190: + base.getPreText());
191: IteratorOfClassInvariant it = preInvs.iterator();
192: while (it.hasNext()) {
193: sb.append("<br><b>pre:</b> ");
194: sb.append(it.next().toString());
195: }
196: sb.append("<br><b>modifies:</b> " + base.getModifiesText());
197: sb.append("<br><b>post:</b> " + base.getPostText());
198: it = postInvs.iterator();
199: while (it.hasNext()) {
200: sb.append("<br><b>post:</b> ");
201: sb.append(it.next().toString());
202: }
203: sb.append("</p></html>");
204: contractTextArea.setText(sb.toString());
205: repaint();
206: }
207:
208: public void updateContractWithBase(OldOperationContract mc) {
209: base = mc;
210: updateDisplay();
211: }
212:
213: public void setPreInvs(ListOfClassInvariant preInvs) {
214: this .preInvs = preInvs;
215: updateDisplay();
216: }
217:
218: public void setPostInvs(ListOfClassInvariant postInvs) {
219: this .postInvs = postInvs;
220: updateDisplay();
221: }
222:
223: public void clear() {
224: //do nothing, we create an instance of this class each time
225: }
226:
227: public void allowConfiguration(boolean allowConfig) {
228: this .allowConfig = allowConfig;
229: }
230:
231: class ContractListSelectionListener implements
232: ListSelectionListener {
233:
234: private DefaultContractConfigurator conf;
235:
236: ContractListSelectionListener(DefaultContractConfigurator conf) {
237: this .conf = conf;
238: }
239:
240: public void valueChanged(ListSelectionEvent e) {
241: conf
242: .updateContractWithBase((OldOperationContract) ((JList) e
243: .getSource()).getSelectedValue());
244: }
245:
246: }
247:
248: }
|