Create a JSON-RPC for KeY

key.core.example/src/main/java/org/key_project/Main.java

@@ -97,6 +97,7 @@ private static void proveEnvironmemt(KeYEnvironment<?> env) {
                 LOGGER.info("Found contract '" + contract.getDisplayName());
                 proveContract(env, contract);
             }
+        } catch (InterruptedException ignored) {
         } finally {
             env.dispose(); // Ensure always that all instances of KeYEnvironment are disposed
         }
@@ -135,7 +136,8 @@ private static List<Contract> getContracts(KeYEnvironment<?> env) {
      * @param env the {@link KeYEnvironment} in which to prove the contract
      * @param contract the {@link Contract} to be proven
      */
-    private static void proveContract(KeYEnvironment<?> env, Contract contract) {
+    private static void proveContract(KeYEnvironment<?> env, Contract contract)
+            throws InterruptedException {
         Proof proof = null;
         try {
             // Create proof

key.core/src/main/java/de/uka/ilkd/key/Identifiable.java

@@ -0,0 +1,14 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (14.10.23)
+ */
+public interface Identifiable {
+    default String identification() {
+        return getClass().getName() + "_" + hashCode();
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.util.KeYTypeUtil;
 
@@ -333,6 +334,45 @@ public boolean isDisposed() {
         return proofScript;
     }
 
+    /**
+     * Retrieve a list of all available contracts for all known Java types.
+     *
+     * @return a non-null list, possible empty
+     */
+    public List<Contract> getAvailableContracts() {
+        List<Contract> proofContracts = new ArrayList<>(512);
+        Set<KeYJavaType> kjts = getJavaInfo().getAllKeYJavaTypes();
+        for (KeYJavaType type : kjts) {
+            if (!KeYTypeUtil.isLibraryClass(type)) {
+                ImmutableSet<IObserverFunction> targets =
+                    getSpecificationRepository().getContractTargets(type);
+                for (IObserverFunction target : targets) {
+                    ImmutableSet<Contract> contracts =
+                        getSpecificationRepository().getContracts(type, target);
+                    for (Contract contract : contracts) {
+                        proofContracts.add(contract);
+                    }
+                }
+            }
+        }
+        return proofContracts;
+    }
+
+
+    /**
+     * Constructs a list containing all known rules that are registered in the current
+     * environment.
+     *
+     * @return always returns a non-null list
+     */
+    public List<Rule> getRules() {
+        var rules = new ArrayList<Rule>(4096);
+        rules.addAll(getInitConfig().activatedTaclets());
+        getInitConfig().builtInRules().forEach(rules::add);
+        return rules;
+    }
+
+
     /**
      * constructs the possible proof contracts from the java info in the environment.
      */

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

@@ -36,7 +36,7 @@ public void taskStarted(TaskStartedInfo info) {
         numOfInvokedMacros++;
         if (superordinateListener != null) {
             superordinateListener.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro,
-                macroName + (macroName.length() == 0 ? "" : " -- ") + info.message(),
+                macroName + (macroName.isEmpty() ? "" : " -- ") + info.message(),
                 info.size()));
         }
     }

key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java

@@ -13,16 +13,15 @@
 import de.uka.ilkd.key.logic.op.ProgramVariable;
 import de.uka.ilkd.key.pp.LogicPrinter;
 import de.uka.ilkd.key.pp.NotationInfo;
+import de.uka.ilkd.key.proof.mgt.RuleJustification;
 import de.uka.ilkd.key.proof.proofevent.NodeChangeJournal;
 import de.uka.ilkd.key.proof.proofevent.RuleAppInfo;
-import de.uka.ilkd.key.rule.AbstractExternalSolverRuleApp;
-import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.rule.merge.MergeRule;
 import de.uka.ilkd.key.strategy.QueueRuleApplicationManager;
 import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.util.MiscTools;
 import de.uka.ilkd.key.util.properties.MapProperties;
 import de.uka.ilkd.key.util.properties.Properties;
 import de.uka.ilkd.key.util.properties.Properties.Property;
@@ -757,6 +756,13 @@ public List<RuleApp> getAllBuiltInRuleApps() {
         return ruleApps;
     }
 
+    /**
+     * Return a list with available taclet application on this goal.
+     */
+    public List<TacletApp> getAllTacletApps() {
+        return getAllTacletApps(proof().getServices());
+    }
+
     public List<TacletApp> getAllTacletApps(Services services) {
         RuleAppIndex index = ruleAppIndex();
         index.autoModeStopped();
@@ -781,4 +787,37 @@ protected boolean filter(Taclet taclet) {
         return allApps;
     }
 
+    /**
+     * Returns a list with all known rule applications within this proof goal.
+     */
+    public List<RuleApp> getAllAvailableRules() {
+        var taclets = getAllTacletApps();
+        var builtin = getAllBuiltInRuleApps();
+        builtin.addAll(taclets);
+        return builtin;
+    }
+
+    public List<Rule> getAvailableRules() {
+        var s = new ArrayList<Rule>(2048);
+        for (final BuiltInRule br : ruleAppIndex().builtInRuleAppIndex()
+                .builtInRuleIndex().rules()) {
+            s.add(br);
+        }
+
+        Set<NoPosTacletApp> set = ruleAppIndex().tacletIndex().allNoPosTacletApps();
+        OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(proof());
+        if (simplifier != null && !simplifier.isShutdown()) {
+            set.addAll(simplifier.getCapturedTaclets());
+        }
+
+        for (final NoPosTacletApp app : set) {
+            RuleJustification just = proof().mgt().getJustification(app);
+            if (just == null) {
+                continue; // do not break system because of this
+            }
+            s.add(app.taclet()); // TODO not good
+        }
+        return s;
+    }
+
 }

key.core/src/main/java/de/uka/ilkd/key/proof/Node.java

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
+import java.util.*;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
@@ -12,6 +13,7 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.ListIterator;
+import java.util.stream.Stream;
 
 import de.uka.ilkd.key.logic.RenamingTable;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
@@ -838,4 +840,8 @@ public int getStepIndex() {
     void setStepIndex(int stepIndex) {
         this.stepIndex = stepIndex;
     }
+
+    public Stream<Node> childrenStream() {
+        return children.stream();
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java

@@ -10,6 +10,7 @@
 import java.util.function.Consumer;
 import java.util.function.Predicate;
 
+import de.uka.ilkd.key.Identifiable;
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
@@ -42,6 +43,7 @@
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.lookup.Lookup;
 
+import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 
@@ -56,7 +58,7 @@
  * goals, namespaces and several other information about the current state of the proof.
  */
 @NullMarked
-public class Proof implements ProofObject<Goal>, Named {
+public class Proof implements ProofObject<Goal>, Named, Identifiable {
 
     /**
      * The time when the {@link Proof} instance was created.
@@ -1381,4 +1383,12 @@ public void printSymbols(PrintWriter ps) {
     public long getCreationTime() {
         return creationTime;
     }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public String identification() {
+        return getClass().getName() + "_" + name + "_" + hashCode();
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/ProofNodeDescription.java

@@ -0,0 +1,45 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.proof;
+
+import java.io.Serializable;
+
+public class ProofNodeDescription implements Serializable {
+    /**
+     * Collects the information from the tree to which branch the current node belongs:
+     * <ul>
+     * <li>Invariant Initially Valid</li>
+     * <li>Body Preserves Invariant</li>
+     * <li>Use Case</li>
+     * <li>...</li>
+     * </ul>
+     *
+     * @param node the current node
+     * @return a String containing the path information to display
+     */
+    public static String collectPathInformation(Node node) {
+        while (node != null) {
+            if (node.getNodeInfo() != null && node.getNodeInfo().getBranchLabel() != null) {
+                String label = node.getNodeInfo().getBranchLabel();
+                /*
+                 * Are there other interesting labels? Please feel free to add them here.
+                 */
+                if (label.equals("Invariant Initially Valid")
+                        || label.equals("Invariant Preserved and Used") // for loop scope invariant
+                        || label.equals("Body Preserves Invariant") || label.equals("Use Case")
+                        || label.equals("Show Axiom Satisfiability") || label.startsWith("Pre (")
+                        || label.startsWith("Exceptional Post (") // exceptional postcondition
+                        || label.startsWith("Post (") // postcondition of a method
+                        || label.contains("Normal Execution") || label.contains("Null Reference")
+                        || label.contains("Index Out of Bounds") || label.contains("Validity")
+                        || label.contains("Precondition") || label.contains("Usage")) {
+                    return label;
+                }
+            }
+            node = node.parent();
+        }
+        // if no label was found we have to prove the postcondition
+        return "Show Postcondition/Modifiable";
+    }
+}

key.ui/src/main/java/de/uka/ilkd/key/core/Main.java

@@ -448,25 +448,27 @@ private AbstractMediatorUserInterfaceControl createUserInterface(List<Path> file
     }
 
     public static void ensureExamplesAvailable() {
-        File examplesDir = getExamplesDir() == null ? ExampleChooser.lookForExamples()
-                : new File(getExamplesDir());
-        if (!examplesDir.exists()) {
+        Path examplesDir =
+            getExamplesDir() == null ? ExampleChooser.lookForExamples() : getExamplesDir();
+        if (!Files.exists(examplesDir)) {
             examplesDir = setupExamples();
         }
-        setExamplesDir(examplesDir.getAbsolutePath());
+        if (examplesDir == null) {
+            setExamplesDir(examplesDir.toAbsolutePath());
+        }
     }
 
-    private static File setupExamples() {
+    private static @Nullable Path setupExamples() {
         try {
             URL examplesURL = Main.class.getResource("/examples.zip");
             if (examplesURL == null) {
                 throw new IOException("Missing examples.zip in resources");
             }
 
-            File tempDir = createTempDirectory();
+            Path tempDir = Files.createTempDirectory("key-examples");
 
             if (tempDir != null) {
-                IOUtil.extractZip(examplesURL.openStream(), tempDir.toPath());
+                IOUtil.extractZip(examplesURL.openStream(), tempDir);
             }
             return tempDir;
         } catch (IOException e) {
@@ -524,9 +526,9 @@ private void preProcessInput()
         }
     }
 
-    private static String EXAMPLE_DIR = null;
+    private static Path EXAMPLE_DIR = null;
 
-    public static @Nullable String getExamplesDir() {
+    public static @Nullable Path getExamplesDir() {
         return EXAMPLE_DIR;
     }
 
@@ -537,7 +539,7 @@ private void preProcessInput()
      *
      * @param newExamplesDir The new examples directory to use.
      */
-    public static void setExamplesDir(String newExamplesDir) {
+    public static void setExamplesDir(Path newExamplesDir) {
         EXAMPLE_DIR = newExamplesDir;
     }
 }