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.event.ActionEvent;
013: import java.awt.event.ActionListener;
014:
015: import javax.swing.*;
016:
017: import de.uka.ilkd.key.cspec.ComputeSpecification;
018: import de.uka.ilkd.key.gui.nodeviews.SequentView;
019: import de.uka.ilkd.key.logic.ConstrainedFormula;
020: import de.uka.ilkd.key.logic.Semisequent;
021: import de.uka.ilkd.key.logic.Sequent;
022: import de.uka.ilkd.key.logic.Term;
023: import de.uka.ilkd.key.pp.LogicPrinter;
024: import de.uka.ilkd.key.pp.ProgramPrinter;
025: import de.uka.ilkd.key.util.Debug;
026:
027: /**
028: * This class is a facade for computing the specification of a program,
029: * and displaying a corresponding view.
030: *
031: * @author André Platzer
032: * @version 1.1, 2003-02-01
033: * @version-revision $Revision: 1.14.1.1.2.1.2.4.1.1 $, $Date: Tue, 26 Jun 2007 14:56:17 +0200 $
034: * @see de.uka.ilkd.key.cspec.ComputeSpecification
035: */
036: public class ComputeSpecificationView {
037:
038: private ComputeSpecificationView() {
039: }
040:
041: private static final JRadioButtonMenuItem createRadioButton_Prestate(
042: ButtonGroup group, String label, final int value) {
043: JRadioButtonMenuItem menuItem = new JRadioButtonMenuItem(label,
044: ComputeSpecification.getPrestateRemember() == value);
045: group.add(menuItem);
046: menuItem.addActionListener(new ActionListener() {
047: public void actionPerformed(ActionEvent e) {
048: ComputeSpecification.setPrestateRemember(value);
049: }
050: });
051: return menuItem;
052: }
053:
054: private static final JRadioButtonMenuItem createRadioButton_Poststate(
055: ButtonGroup group, String label, final int value) {
056: JRadioButtonMenuItem menuItem = new JRadioButtonMenuItem(label,
057: ComputeSpecification.getPoststateRemember() == value);
058: group.add(menuItem);
059: menuItem.addActionListener(new ActionListener() {
060: public void actionPerformed(ActionEvent e) {
061: ComputeSpecification.setPoststateRemember(value);
062: }
063: });
064: return menuItem;
065: }
066:
067: public static JMenuItem createOptionMenuItems() {
068: ButtonGroup prestateRememberGroup = new ButtonGroup();
069: JMenu rememberMenu = new JMenu("Specification Extraction");
070:
071: rememberMenu.add(createRadioButton_Prestate(
072: prestateRememberGroup, "Prestate Remember Equations",
073: ComputeSpecification.PRESTATE_REMEMBER_EQUATIONS));
074:
075: rememberMenu.add(createRadioButton_Prestate(
076: prestateRememberGroup, "Prestate Remember Updates",
077: ComputeSpecification.PRESTATE_REMEMBER_UPDATES));
078:
079: rememberMenu.add(createRadioButton_Prestate(
080: prestateRememberGroup, "Prestate Remember Implicit",
081: ComputeSpecification.PRESTATE_REMEMBER_IMPLICIT));
082:
083: rememberMenu.addSeparator();
084: ButtonGroup poststateRememberGroup = new ButtonGroup();
085:
086: rememberMenu.add(createRadioButton_Poststate(
087: poststateRememberGroup, "Poststate Remember Equations",
088: ComputeSpecification.POSTSTATE_REMEMBER_EQUATIONS));
089: rememberMenu
090: .add(createRadioButton_Poststate(
091: poststateRememberGroup,
092: "Poststate Remember Accumulator",
093: ComputeSpecification.POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION));
094:
095: return rememberMenu;
096: }
097:
098: /**
099: * A facade for the user-interface, displaying the computed
100: * specification of a program.
101: * @param mediator the KeY-mediator containing the specification construction proof.
102: * @see de.uka.ilkd.key.casetool.FunctionalityOnModel#computeSpecification(ReprModelMethod)
103: */
104: public static final void show(KeYMediator mediator) {
105: try {
106: final Term spec = new ComputeSpecification()
107: .computeSpecification(mediator);
108: final Sequent spec2 = Sequent
109: .createSuccSequent(Semisequent.EMPTY_SEMISEQUENT
110: .insertLast(new ConstrainedFormula(spec))
111: .semisequent());
112: Debug.out("\nOverall specification is:\n", spec);
113: Debug.out("\nalias:\n", spec2);
114: final SequentView view = new SequentView(mediator);
115: view.setPreferredSize(new Dimension(800, 600));
116: view
117: .setPrinter(new LogicPrinter(new ProgramPrinter(
118: null), mediator.getNotationInfo(), mediator
119: .getServices()), spec2);
120: view.printSequent();
121: view.setCaretPosition(0); // at least until a better solution
122: final JScrollPane pane = new JScrollPane(view,
123: JScrollPane.VERTICAL_SCROLLBAR_ALWAYS,
124: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
125:
126: pane.setPreferredSize(new Dimension(600, 400));
127: mediator.popupInformationMessage(pane,
128: "Computed Specification", false);
129: } catch (Exception e) {
130: mediator.getExceptionHandler().reportException(e);
131: new ExceptionDialog(mediator.mainFrame(), mediator
132: .getExceptionHandler().getExceptions());
133: mediator.getExceptionHandler().clear();
134: }
135: }
136:
137: }// ComputeSpecificationView
|