introducing the script-aware prep macro

Author: mattulbrich

key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java

@@ -50,7 +50,7 @@ public class ApplyScriptsMacro extends AbstractProofMacro {
 
     private static final Logger LOGGER = LoggerFactory.getLogger(ApplyScriptsMacro.class);
 
-    private final ProofMacro fallBackMacro;
+    private final @Nullable ProofMacro fallBackMacro;
 
     public ApplyScriptsMacro(ProofMacro fallBackMacro) {
         this.fallBackMacro = fallBackMacro;
@@ -74,7 +74,7 @@ public String getDescription() {
     @Override
     public boolean canApplyTo(Proof proof, ImmutableList<@NonNull Goal> goals,
             PosInOccurrence posInOcc) {
-        return fallBackMacro.canApplyTo(proof, goals, posInOcc)
+        return fallBackMacro != null && fallBackMacro.canApplyTo(proof, goals, posInOcc)
                 || goals.exists(g -> getJmlAssert(g.node()) != null);
     }
 
@@ -137,7 +137,9 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             if (Thread.interrupted()) {
                 throw new InterruptedException();
             }
-            fallBackMacro.applyTo(uic, proof, ImmutableList.of(goal), posInOcc, listener);
+            if(fallBackMacro != null) {
+                fallBackMacro.applyTo(uic, proof, ImmutableList.of(goal), posInOcc, listener);
+            }
 
         }
 

key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java

@@ -18,19 +18,19 @@
 
 /**
  * This class captures a proof macro which is meant to fully automise KeY proof
- * workflow.
+ * workflow if scripts are present in the JML code.
  *
  * It is experimental.
  *
  * It performs the following steps:
  * <ol>
  * <li>Finish symbolic execution
- * <li>>Separate proof obligations" +
- * <li>Expand invariant definitions
- * <li>Try to close all proof obligations
+ * <li>Apply macros
+ * <li>Try to close provable goals
  * </ol>
  *
  * @author mattias ulbrich
+ * @see ScriptAwarePrepMacro
  */
 public class ScriptAwareMacro extends SequentialProofMacro {
 

key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwarePrepMacro.java

@@ -0,0 +1,61 @@
+// 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-2014 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.
+//
+
+package de.uka.ilkd.key.macros;
+
+/**
+ * This class captures a proof macro which is meant to automise KeY proof
+ * workflow if scripts are present in the JML code.
+ *
+ * It is experimental.
+ *
+ * It performs the following steps:
+ * <ol>
+ * <li>Finish symbolic execution
+ * <li>Apply macros
+ * <li>It does not try to close provable goals
+ * </ol>
+ *
+ * @author mattias ulbrich
+ * @see ScriptAwareMacro
+ */
+public class ScriptAwarePrepMacro extends SequentialProofMacro {
+
+    private final ProofMacro autoMacro = new FinishSymbolicExecutionMacro();
+    private final ApplyScriptsMacro applyMacro = new ApplyScriptsMacro(null);
+
+    @Override
+    public String getScriptCommandName() {
+        return "script-prep-auto";
+    }
+
+    @Override
+    public String getName() {
+        return "Script-aware Prep Auto";
+    }
+
+    @Override
+    public String getCategory() {
+        return "Auto Pilot";
+    }
+
+    @Override
+    public String getDescription() {
+        return "TODO";
+    }
+
+    @Override
+    protected ProofMacro[] createProofMacroArray() {
+        return new ProofMacro[] { autoMacro, applyMacro };
+    }
+}

key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro

@@ -31,3 +31,4 @@ de.uka.ilkd.key.macros.WellDefinednessMacro
 de.uka.ilkd.key.macros.UpdateSimplificationMacro
 de.uka.ilkd.key.macros.TranscendentalFloatSMTMacro
 de.uka.ilkd.key.macros.ScriptAwareMacro
+de.uka.ilkd.key.macros.ScriptAwarePrepMacro