From c60feb1b77a5601930e9a8bdca29b484f0448381 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Fri, 19 Jan 2018 10:34:08 +0100 Subject: [PATCH] coammdn help descriptions --- .../funchdl/MacroCommandHandler.java | 18 ++++++++++++ .../funchdl/ProofScriptCommandBuilder.java | 14 ++++----- .../kit/iti/formal/psdbg/commands/auto.html | 10 ------- .../formal/psdbg/commands/instantiate.html | 20 +++++++++++++ .../kit/iti/formal/psdbg/commands/macro.html | 0 .../edu/kit/iti/formal/psdbg/macros/auto.html | 17 +++++++++++ .../formal/psdbg/macros/autopilot-prep.html | 23 +++++++++++++++ .../iti/formal/psdbg/macros/autopilot.html | 26 +++++++++++++++++ .../psdbg/macros/infflow-autopilot.html | 29 +++++++++++++++++++ .../formal/psdbg/macros/nonsplit-prop.html | 19 ++++++++++++ .../kit/iti/formal/psdbg/macros/onestep.html | 18 ++++++++++++ .../iti/formal/psdbg/macros/simp-heap.html | 20 +++++++++++++ .../kit/iti/formal/psdbg/macros/simp-int.html | 19 ++++++++++++ .../kit/iti/formal/psdbg/macros/simp-upd.html | 19 ++++++++++++ .../iti/formal/psdbg/macros/split-prop.html | 18 ++++++++++++ .../kit/iti/formal/psdbg/macros/symbex.html | 19 ++++++++++++ .../kit/iti/formal/psdbg/macros/tryclose.html | 20 +++++++++++++ website/docs/index.md | 4 +-- 18 files changed, 292 insertions(+), 21 deletions(-) delete mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/macro.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/auto.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot-prep.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/infflow-autopilot.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/nonsplit-prop.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/onestep.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-heap.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-int.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-upd.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/split-prop.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/symbex.html create mode 100644 rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/tryclose.html diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java index 419e9226..7c891f25 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java @@ -13,10 +13,14 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import lombok.Getter; import lombok.RequiredArgsConstructor; +import org.apache.commons.io.IOUtils; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.key_project.util.collection.ImmutableList; +import java.io.IOException; +import java.net.URISyntaxException; +import java.net.URL; import java.util.Collection; import java.util.HashMap; import java.util.Map; @@ -86,4 +90,18 @@ public class MacroCommandHandler implements CommandHandler { LOGGER.debug("Execution of {} took {} ms", call.getCommand(), (System.currentTimeMillis() - startTime)); } } + + @Override + public String getHelp(CallStatement call) { + ProofMacro macro = macros.get(call.getCommand()); + URL res = getClass().getResource("/edu/kit/iti/formal/psdbg/macros/" + call.getCommand() + ".html"); + try { + return IOUtils.toString(res.toURI(), "utf-8"); + } catch (NullPointerException | IOException | URISyntaxException e) { + return "No Help found for " + call.getCommand(); + + } + + + } } diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java index 1df5264e..681e63a3 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java @@ -4,6 +4,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; +import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import edu.kit.iti.formal.psdbg.interpreter.Interpreter; @@ -14,14 +15,10 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import lombok.Getter; import lombok.RequiredArgsConstructor; -import org.apache.commons.io.IOUtils; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.key_project.util.collection.ImmutableList; -import java.io.IOException; -import java.net.URISyntaxException; -import java.net.URL; import java.util.Collection; import java.util.HashMap; import java.util.Iterator; @@ -107,16 +104,15 @@ public class ProofScriptCommandBuilder implements CommandHandler { @Override public String getHelp(CallStatement call) { ProofScriptCommand c = commands.get(call.getCommand()); - - URL res = getClass().getResource("/commands/" + call.getCommand() + ".html"); + /* URL res = getClass().getResource("/edu/kit/iti/formal/psdbg/commands/" + call.getCommand() + ".html"); try { return IOUtils.toString(res.toURI(), "utf-8"); } catch (NullPointerException | IOException | URISyntaxException e) { return "No Help found for " + call.getCommand(); - } + }*/ + - /* StringBuilder html = new StringBuilder(); @@ -168,6 +164,6 @@ public class ProofScriptCommandBuilder implements CommandHandler { html.append(""); return html.toString(); - */ + } } diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html deleted file mode 100644 index 566549bd..00000000 --- a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html +++ /dev/null @@ -1,10 +0,0 @@ - - - - - Title - - - - - \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html new file mode 100644 index 00000000..6b9f4b66 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html @@ -0,0 +1,20 @@ + + + + + Auto + + +

instantiate

+
+

Synopsis: instantiate formula=<TERM> var=<STRING> occ=<INT> with=<TERM>

+
+

Arguments:

+
    +
  • formula : TERM (R)null
    • +
  • var : STRING (R)null
    • +
  • occ : INT (R)null
    • +
  • with : TERM (R)null
    • +
+ + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/macro.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/macro.html new file mode 100644 index 00000000..e69de29b diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/auto.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/auto.html new file mode 100644 index 00000000..0bdd8baf --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/auto.html @@ -0,0 +1,17 @@ + + + + + Auto + + +

auto

+
+

Synopsis: auto;

+
+This macro invokes the automatic strategies of KeY. Ths maximal number of step can be set before using special +variables. +

Arguments:

+No arguments required. + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot-prep.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot-prep.html new file mode 100644 index 00000000..aa493d0b --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot-prep.html @@ -0,0 +1,23 @@ + + + + + autopilot-prep + + +

autopilot-prep

+
+

Synopsis: autopilot-prep;

+
+

Description:

+This macro performs the following steps: +
    +
  1. Finish symbolic execution +
  2. Separate proof obligations +
  3. Expand invariant definitions +
+

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot.html new file mode 100644 index 00000000..10e98189 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot.html @@ -0,0 +1,26 @@ + + + + + autopilot + + +

autopilot

+
+

Synopsis: autopilot;

+
+

Description:

+ +This macro performs the following steps: +
    +
  1. Finish symbolic execution +
  2. Separate proof obligations +
  3. Expand invariant definitions +
  4. Try to close all proof obligations +
+

Arguments:

+No arguments required + + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/infflow-autopilot.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/infflow-autopilot.html new file mode 100644 index 00000000..a27d1ce7 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/infflow-autopilot.html @@ -0,0 +1,29 @@ + + + + + infflow-autopilot + + +

infflow-autopilot

+
+

Synopsis: infflow-autopilot;

+
+

Description:

+This macro is tailored to information flow problems. +
    +
  1. Search exhaustively for applicable position, then +
  2. Start auxiliary computation +
  3. Finish symbolic execution +
  4. Try to close as many goals as possible +
  5. Apply macro recursively +
  6. Finish auxiliary computation +
  7. Use information flow contracts +
  8. Try to close as many goals as possible +
+ +

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/nonsplit-prop.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/nonsplit-prop.html new file mode 100644 index 00000000..7e033bde --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/nonsplit-prop.html @@ -0,0 +1,19 @@ + + + + + nonsplit-prop + + +

nonsplit-prop

+
+

Synopsis: nonsplit-prop;

+
+

Description:

+This macros applies rules to decompose propositional toplevel formulas without applying splitting rules. +In addition, formulas are simplified using one step simplifications. +

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/onestep.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/onestep.html new file mode 100644 index 00000000..ae137078 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/onestep.html @@ -0,0 +1,18 @@ + + + + + onestep + + +

onestep

+
+

Synopsis: onestep;

+
+

Description:

+This amcro applies one proof step. The applied proof rule is chosen from KeY's automatic startegies. +

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-heap.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-heap.html new file mode 100644 index 00000000..a8fd4f80 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-heap.html @@ -0,0 +1,20 @@ + + + + + simp-heap + + +

simp-heap

+
+

Synopsis: simp-heap;

+
+

Description:

+This macro performs simplification of Heap and LocSet terms. +It applies simplification rules (including the "unoptimized" select rules), +One Step Simplification, alpha, and delta rules. +

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-int.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-int.html new file mode 100644 index 00000000..afff915d --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-int.html @@ -0,0 +1,19 @@ + + + + + simp-int + + +

simp-int

+
+

Synopsis: simp-int;

+
+

Description:

+This macro performs simplification of integers and terms with integers. +It applies only non-splitting simplification rules. +

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-upd.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-upd.html new file mode 100644 index 00000000..d68fb733 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-upd.html @@ -0,0 +1,19 @@ + + + + + simp-upd + + +

simp-upd

+
+

Synopsis: simp-upd;

+
+

Description:

+This macro applies only update simplification rules, i.e., that simplify the update term. +

Arguments:

+No arguments required + + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/split-prop.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/split-prop.html new file mode 100644 index 00000000..a92a2dc3 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/split-prop.html @@ -0,0 +1,18 @@ + + + + + split-prop + + +

split-prop

+
+

Synopsis: split-prop;

+
+

Description:

+This macros applies rules to decompose propositional toplevel formulas and also applies splitting rules. +

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/symbex.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/symbex.html new file mode 100644 index 00000000..d73fde11 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/symbex.html @@ -0,0 +1,19 @@ + + + + + symbex + + +

symbex

+
+

Synopsis: symbex;

+
+

Description:

+Applies rules until there is no modality on the seuqent. +That is, this macro symbolically executes the program to prove. +

Arguments:

+No arguments required + + + \ No newline at end of file diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/tryclose.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/tryclose.html new file mode 100644 index 00000000..5f01bf46 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/tryclose.html @@ -0,0 +1,20 @@ + + + + + Auto + + +

tryclose

+
+

Synopsis: tryclose;

+
+

Description:

+Tries to close all open goals using KeY's automatic strategies. If not successful, the goal remains unchanged. +So Goals are either closed or left untouched. +

Arguments:

+No arguments required + + + + \ No newline at end of file diff --git a/website/docs/index.md b/website/docs/index.md index 27f9dfe4..6ac1c810 100644 --- a/website/docs/index.md +++ b/website/docs/index.md @@ -44,7 +44,7 @@ The proof script debugger is a prototypical implementation of an interaction concept for program verification systems that are rule based and use a program logic. The prototype is implemented on top of the interactive program verification system -[KeY](http://www.key-project.org. KeY is an interactive program verification +[KeY](http://www.key-project.org). KeY is an interactive program verification system for Java program annotated with the Java Modeling Language (JML). @@ -70,7 +70,7 @@ the analysis of failed proof attempts. ## Publications A full description of the language and debugging-concept -is published at [HVC 2017](hvc2017.pdf) +is published at [HVC 2017](http://rdcu.be/E4fF) ## Features -- GitLab