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 419e9226f77364b6daeba590774d287525d2b0a6..7c891f25b27c22607ab5764e74cefdc39f820670 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 1df5264e5f466f2d8ad0f4565760ef2e813e5d51..681e63a3f302fba2ff9252e968ade1655c656ab0 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 566549bdf8fae810809c1a81066000687cb338f6..0000000000000000000000000000000000000000 --- 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 0000000000000000000000000000000000000000..6b9f4b6661cee2a76d298ccd6fd14c48b1d17d06 --- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..0bdd8baf5348875d7b61562c90778a5a90993b92 --- /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 0000000000000000000000000000000000000000..aa493d0b49a87e57473f8f9b808b92b63744d361 --- /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 0000000000000000000000000000000000000000..10e98189de22424554f087fa7a09b799bf395db4 --- /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 0000000000000000000000000000000000000000..a27d1ce78c219acea28ad6e5953129824191cd8c --- /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 0000000000000000000000000000000000000000..7e033bdefdf8b32db5ea92420588bd4984e6f210 --- /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 0000000000000000000000000000000000000000..ae137078132526f61a1eb525f9a33ea30470c59c --- /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 0000000000000000000000000000000000000000..a8fd4f80aeda35f11d968d392f5656c8f8a18eb3 --- /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 0000000000000000000000000000000000000000..afff915d6d16748040ca74f1f73f82cd1b106cb5 --- /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 0000000000000000000000000000000000000000..d68fb73399c631f49ea819ece31441f905ee2b41 --- /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 0000000000000000000000000000000000000000..a92a2dc361eba571d51637d7dfc150fc67d7ab40 --- /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 0000000000000000000000000000000000000000..d73fde115f231295d3653eb3a12a25ecbe42367a --- /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 0000000000000000000000000000000000000000..5f01bf465aa510de9c5cc30c27344cb13861f71b --- /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 27f9dfe4184696b3b7a752fd26026ad012263fa0..6ac1c810f8c61d57f852f203d2273feca4c32bd5 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