Examples menu and package-info.java

src/main/java/edu/kit/formal/psdb/examples/Example.java

+package edu.kit.formal.psdb.examples;
+
+import edu.kit.formal.psdb.gui.controller.DebuggerMain;
+import edu.kit.formal.psdb.gui.model.MainScriptIdentifier;
+import lombok.*;
+import org.apache.commons.io.FileUtils;
+import org.apache.commons.io.IOUtils;
+
+import java.io.File;
+import java.io.IOException;
+import java.net.URL;
+import java.nio.charset.Charset;
+
+@Data
+@AllArgsConstructor
+@NoArgsConstructor
+@ToString
+@EqualsAndHashCode
+public abstract class Example {
+    protected String name;
+    protected URL helpText;
+    protected URL keyFile;
+    protected URL scriptFile;
+    protected MainScriptIdentifier mainScriptIdentifier;
+
+    public static File newTempFile(URL url, String filename) throws IOException {
+        File f = new File(FileUtils.getTempDirectoryPath(), filename);
+        FileUtils.copyURLToFile(url, f);
+        return f;
+    }
+
+    protected void defaultInit(Class aClass) {
+        setHelpText(aClass.getResource("help.html"));
+        setKeyFile(aClass.getResource("problem.key"));
+        setMainScriptIdentifier(new MainScriptIdentifier("script.kps", -1, "main", null));
+        setScriptFile(aClass.getResource("script.kps"));
+    }
+
+    public void open(DebuggerMain debuggerMain) {
+        try {
+            File script = newTempFile(scriptFile, getName() + ".kps");
+            debuggerMain.openScript(script);
+            File key = newTempFile(keyFile, "problem.key");
+            debuggerMain.openKeyFile(key);
+            if (helpText != null) {
+                String content = IOUtils.toString(helpText, Charset.defaultCharset());
+                debuggerMain.openNewHelpDock(getName() + " Example", content);
+            }
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+    }
+}

src/main/java/edu/kit/formal/psdb/examples/Examples.java

+package edu.kit.formal.psdb.examples;
+
+import java.util.*;
+import java.util.stream.Collectors;
+import java.util.stream.StreamSupport;
+
+/**
+ * A facade for loading examples.
+ * @author Alexander Weigl
+ */
+public class Examples {
+    public static Collection<Example> loadExamples() {
+        ServiceLoader<Example> sl = ServiceLoader.load(Example.class);
+        return StreamSupport.stream(sl.spliterator(), false).collect(Collectors.toList());
+    }
+}

src/main/java/edu/kit/formal/psdb/examples/JavaExample.java

+package edu.kit.formal.psdb.examples;
+
+import edu.kit.formal.psdb.gui.controller.DebuggerMain;
+import org.apache.commons.io.IOUtils;
+
+import java.io.File;
+import java.io.IOException;
+import java.net.URL;
+import java.nio.charset.Charset;
+
+/**
+ * Under construction!!!!!!
+ * @author Alexander Weigl
+ */
+public class JavaExample extends Example {
+    protected URL javaFile;
+
+    @Override
+    public void open(DebuggerMain debuggerMain) {
+        //TODO should be reworked if we have an example
+        //     Loading via key file, or using an automatic contract selector?
+
+        try {
+            File script = newTempFile(scriptFile, getName() + ".kps");
+            debuggerMain.openScript(script);
+            File key = newTempFile(keyFile, "problem.key");
+            File java = newTempFile(javaFile, getName() + ".java");
+            debuggerMain.openKeyFile(key);
+            if (helpText != null) {
+                String content = IOUtils.toString(helpText, Charset.defaultCharset());
+                debuggerMain.openNewHelpDock(getName() + " Example", content);
+            }
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+    }
+}

src/main/java/edu/kit/formal/psdb/examples/contraposition/ContrapositionExample.java

+package edu.kit.formal.psdb.examples.contraposition;
+
+import edu.kit.formal.psdb.examples.Example;
+import edu.kit.formal.psdb.gui.model.MainScriptIdentifier;
+
+import java.net.URL;
+
+/**
+ *
+ */
+public class ContrapositionExample extends Example {
+
+    public ContrapositionExample() {
+        setName("Contraposition");
+        defaultInit(getClass());
+
+        System.out.println(this);
+    }
+
+}

src/main/java/edu/kit/formal/psdb/examples/fol/FirstOrderLogicExample.java

+package edu.kit.formal.psdb.examples.fol;
+
+import edu.kit.formal.psdb.examples.Example;
+
+public class FirstOrderLogicExample extends Example {
+    public FirstOrderLogicExample() {
+        name = "First Order Logic";
+        defaultInit(getClass());
+    }
+}

src/main/java/edu/kit/formal/psdb/gui/ProofScriptDebugger.java

 package edu.kit.formal.psdb.gui;
 
-/**
- * Main Entry for Debugger GUI
- *
- * @author S. Grebing
- */
 
 import de.uka.ilkd.key.util.KeYConstants;
 import javafx.application.Application;
@@ -19,6 +14,15 @@ import org.dockfx.DockNode;
 
 import java.util.Locale;
 
+/**
+ * Entry class for the {@link ProofScriptDebugger} (JavaFX Application).
+ * <p>
+ * For a command line interface see {@link edu.kit.formal.psdb.interpreter.Execute}
+ * <p>
+ *
+ * @author S. Grebing
+ * @author Alexander Weigl
+ */
 public class ProofScriptDebugger extends Application {
     public static final String NAME = "Proof Script Debugger";
     public static final String VERSION = "0.1";

src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java

@@ -5,6 +5,7 @@ import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.api.ProofApi;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.speclang.Contract;
+import edu.kit.formal.psdb.examples.Examples;
 import edu.kit.formal.psdb.gui.ProofScriptDebugger;
 import edu.kit.formal.psdb.gui.controls.*;
 import edu.kit.formal.psdb.gui.model.Breakpoint;
@@ -26,6 +27,8 @@ import javafx.concurrent.Task;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
 import javafx.fxml.Initializable;
+import javafx.scene.control.Menu;
+import javafx.scene.control.MenuItem;
 import javafx.scene.control.ProgressBar;
 import javafx.scene.web.WebEngine;
 import javafx.scene.web.WebView;
@@ -111,7 +114,8 @@ public class DebuggerMain implements Initializable {
 
 
     //-----------------------------------------------------------------------------------------------------------------
-
+    @FXML
+    private Menu examplesMenu;
 
     @Override
     public void initialize(URL location, ResourceBundle resources) {
@@ -137,16 +141,27 @@ public class DebuggerMain implements Initializable {
         );
 
 
-
         //Debugging
         Utils.addDebugListener(javaCode);
         Utils.addDebugListener(executeNotPossible, "executeNotPossible");
 
         scriptController.mainScriptProperty().bindBidirectional(statusBar.mainScriptIdentifierProperty());
 
+        initializeExamples();
 
     }
 
+    private void initializeExamples() {
+        examplesMenu.getItems().clear();
+        Examples.loadExamples().forEach(example -> {
+            MenuItem item = new MenuItem(example.getName());
+            item.setOnAction(event -> {
+                example.open(this);
+            });
+            examplesMenu.getItems().add(item);
+        });
+    }
+
     /**
      * If the mouse moves other toolbar button, the help text should display in the status bar
      */
@@ -364,6 +379,10 @@ public class DebuggerMain implements Initializable {
         return keyFile.get();
     }
 
+    public void setKeyFile(File keyFile) {
+        this.keyFile.set(keyFile);
+    }
+
     /**
      * Reload the KeY environment, to execute the script again
      * TODO: reload views
@@ -450,6 +469,11 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+
+    //endregion
+
+    //region Santa's Little Helper
+
     public void openJavaFile(File javaFile) {
         if (javaFile != null) {
             setJavaFile(javaFile);
@@ -458,15 +482,6 @@ public class DebuggerMain implements Initializable {
         }
     }
 
-
-    //endregion
-
-    //region Santa's Little Helper
-
-    public void setKeyFile(File keyFile) {
-        this.keyFile.set(keyFile);
-    }
-
     @FXML
     public void saveScript() {
         try {
@@ -496,7 +511,6 @@ public class DebuggerMain implements Initializable {
     //endregion
 
     //region Santa's Little Helper
-
     @FXML
     protected void loadJavaFile() {
         File javaFile = openFileChooserOpenDialog("Select Java File", "Java Files", "java");
@@ -742,15 +756,25 @@ public class DebuggerMain implements Initializable {
     }
 
     public void showHelpText() {
+        String url = ProofScriptDebugger.class.getResource("intro.html").toExternalForm();
+        showHelpText(url);
+    }
 
+    public void showHelpText(String url) {
         WebView browser = new WebView();
         WebEngine webEngine = browser.getEngine();
-        String url = ProofScriptDebugger.class.getResource("intro.html").toExternalForm();
         webEngine.load(url);
         DockNode dn = new DockNode(browser);
+        //this.dockStation.getChildren().add(dn);
+        dn.dock(dockStation, DockPos.LEFT);
+    }
 
-        this.dockStation.getChildren().add(dn);
-
+    public void openNewHelpDock(String title, String content) {
+        WebView browser = new WebView();
+        WebEngine webEngine = browser.getEngine();
+        webEngine.loadContent(content);
+        DockNode dn = new DockNode(browser, title);
+        dn.dock(dockStation, DockPos.LEFT);
     }
 
     public ScriptController getScriptController() {

src/main/java/edu/kit/formal/psdb/package-info.java

+/**
+ * <h1>Proof script debugger</h1>
+ * <p>
+ * <p>
+ * <h2>Programing conventions</h2>
+ * <ul>
+ * <li></li>
+ * </ul>
+ *
+ * @author Sarah Grebing
+ * @author Alexander Weigl
+ */
+package edu.kit.formal.psdb;

src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java

@@ -20,6 +20,12 @@ public class MatcherFacade {
         return matcher.accept(ctx, keyTerm);
     }
 
+    /**
+     * Returns a {@link MatchPatternParser} for the given input pattern.
+     *
+     * @param pattern
+     * @return
+     */
     public static MatchPatternParser getParser(String pattern) {
         return getParser(CharStreams.fromString(pattern));
     }

src/main/java/edu/kit/formal/psdb/termmatcher/package-info.java

+/**
+ *
+ */
+package edu.kit.formal.psdb.termmatcher;
\ No newline at end of file

src/main/resources/META-INF/services/edu.kit.formal.psdb.examples.Example

+edu.kit.formal.psdb.examples.contraposition.ContrapositionExample
+edu.kit.formal.psdb.examples.fol.FirstOrderLogicExample
\ No newline at end of file

src/main/resources/edu/kit/formal/psdb/examples/contraposition/help.html

+<html>
+<body>
+<h1>Contraposition</h1>
+</body>
+</html>
\ No newline at end of file

src/main/resources/edu/kit/formal/psdb/examples/contraposition/problem.key

+// This file is part of KeY - Integrated Deductive Software Design
+//
+// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
+//                         Universitaet Koblenz-Landau, Germany
+//                         Chalmers University of Technology, Sweden
+// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany
+//                         Technical University Darmstadt, Germany
+//                         Chalmers University of Technology, Sweden
+//
+// The KeY system is protected by the GNU General
+// Public License. See LICENSE.TXT for details.
+//
+
+// Input file for KeY standalone prover version 0.497
+\sorts {
+	s;
+}
+
+\predicates {
+	p;
+	q;
+}
+
+\problem {
+    (p -> q) -> !q -> !p
+}

src/main/resources/edu/kit/formal/psdb/examples/contraposition/script.kps

+// Please select one of the following scripts.
+//
+
+script main() {}
+
+
+script cpauto () {
+    auto;
+}
+
+script cpwob () {
+    impRight;
+    impRight;
+    notLeft;
+    notRight;
+    replace_known_left occ='2';
+    concrete_impl_1;
+    close;
+}
\ No newline at end of file

src/main/resources/edu/kit/formal/psdb/examples/fol/problem.key

+// This file is part of KeY - Integrated Deductive Software Design
+//
+// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
+//                         Universitaet Koblenz-Landau, Germany
+//                         Chalmers University of Technology, Sweden
+// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany
+//                         Technical University Darmstadt, Germany
+//                         Chalmers University of Technology, Sweden
+//
+// The KeY system is protected by the GNU General
+// Public License. See LICENSE.TXT for details.
+//
+
+\sorts {
+	s;
+}
+
+\functions {
+        s f(s);
+        s c;
+}
+
+\problem {
+        ( \forall s x; f(f(x)) = f(x) )  ->  f(c) = f(f(f(c)))
+}

src/main/resources/edu/kit/formal/psdb/examples/fol/script.kps

+// This file is not written yet!!
+script main() {
+    impRight;
+    //instantiate with ...
+
+}
\ No newline at end of file

src/main/resources/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml

@@ -63,6 +63,11 @@
                                 <MenuItem onAction="#showProofTree" text="Show Proof Tree"/>
                             </items>
                         </Menu>
+                        <Menu fx:id="examplesMenu" text="Examples">
+                            <items>
+                                <MenuItem text="Examples not loaded" disable="true"/>
+                            </items>
+                        </Menu>
                         <Menu text="Help">
                             <items>
                                 <MenuItem text="About"/>