Skip to content

P
ProofScriptParser
Commit c60feb1b authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

coammdn help descriptions

parent e1d0cfa4
Hide whitespace changes
Inline Side-by-side
Showing with 292 additions and 21 deletions
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java
View file @ c60feb1b
......@@ -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<KeyData> {
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();
}
}
}
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @ c60feb1b
......@@ -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<KeyData> {
@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<KeyData> {
html.append("</body></html>");
return html.toString();
*/
}
}
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html deleted 100644 → 0
View file @ e1d0cfa4
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>Title</title>
</head>
<body>
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>Auto</title>
</head>
<body>
<h2 id="instantiate">instantiate</h2>
<blockquote>
<p>Synopsis: <code>instantiate formula=&lt;TERM&gt; var=&lt;STRING&gt; occ=&lt;INT&gt; with=&lt;TERM&gt;</code></p>
</blockquote>
<p><strong>Arguments:</strong></p>
<ul>
<li><code>formula</code> : <em>TERM</em> (<em>R</em>)null</li>
<li><code>var</code> : <em>STRING</em> (<em>R</em>)null</li>
<li><code>occ</code> : <em>INT</em> (<em>R</em>)null</li>
<li><code>with</code> : <em>TERM</em> (<em>R</em>)null</li>
</ul>
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/auto.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>Auto</title>
</head>
<body>
<h2 id="auto">auto</h2>
<blockquote>
<p>Synopsis: <code>auto;</code></p>
</blockquote>
This macro invokes the automatic strategies of KeY. Ths maximal number of step can be set before using special
variables.
<p><strong>Arguments:</strong></p>
No arguments required.
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot-prep.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>autopilot-prep</title>
</head>
<body>
<h2 id="autopilot-prep">autopilot-prep</h2>
<blockquote>
<p>Synopsis: <code>autopilot-prep;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macro performs the following steps:
<ol>
<li>Finish symbolic execution
<li>Separate proof obligations
<li>Expand invariant definitions
</ol>
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/autopilot.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>autopilot</title>
</head>
<body>
<h2 id="simp-upd">autopilot</h2>
<blockquote>
<p>Synopsis: <code>autopilot;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macro performs the following steps:
<ol>
<li>Finish symbolic execution
<li>Separate proof obligations
<li>Expand invariant definitions
<li>Try to close all proof obligations
</ol>
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/infflow-autopilot.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>infflow-autopilot</title>
</head>
<body>
<h2 id="infflow-autopilot">infflow-autopilot</h2>
<blockquote>
<p>Synopsis: <code>infflow-autopilot;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macro is tailored to information flow problems.
<ol>
<li>Search exhaustively for applicable position, then
<li>Start auxiliary computation
<li>Finish symbolic execution
<li>Try to close as many goals as possible
<li>Apply macro recursively
<li>Finish auxiliary computation
<li>Use information flow contracts
<li>Try to close as many goals as possible
</ol>
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/nonsplit-prop.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>nonsplit-prop</title>
</head>
<body>
<h2 id="symbex">nonsplit-prop</h2>
<blockquote>
<p>Synopsis: <code>nonsplit-prop;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macros applies rules to decompose propositional toplevel formulas without applying splitting rules.
In addition, formulas are simplified using one step simplifications.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/onestep.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>onestep</title>
</head>
<body>
<h2 id="symbex">onestep</h2>
<blockquote>
<p>Synopsis: <code>onestep;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This amcro applies one proof step. The applied proof rule is chosen from KeY's automatic startegies.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-heap.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>simp-heap</title>
</head>
<body>
<h2 id="symbex">simp-heap</h2>
<blockquote>
<p>Synopsis: <code>simp-heap;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
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.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-int.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>simp-int</title>
</head>
<body>
<h2 id="symbex">simp-int</h2>
<blockquote>
<p>Synopsis: <code>simp-int;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macro performs simplification of integers and terms with integers.
It applies only non-splitting simplification rules.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/simp-upd.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>simp-upd</title>
</head>
<body>
<h2 id="simp-upd">simp-upd</h2>
<blockquote>
<p>Synopsis: <code>simp-upd;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macro applies only update simplification rules, i.e., that simplify the update term.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/split-prop.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>split-prop</title>
</head>
<body>
<h2 id="symbex">split-prop</h2>
<blockquote>
<p>Synopsis: <code>split-prop;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macros applies rules to decompose propositional toplevel formulas and also applies splitting rules.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/symbex.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>symbex</title>
</head>
<body>
<h2 id="symbex">symbex</h2>
<blockquote>
<p>Synopsis: <code>symbex;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
Applies rules until there is no modality on the seuqent.
That is, this macro symbolically executes the program to prove.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/macros/tryclose.html 0 → 100644
View file @ c60feb1b
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>Auto</title>
</head>
<body>
<h2 id="tryclose">tryclose</h2>
<blockquote>
<p>Synopsis: <code>tryclose;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
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.
<p><strong>Arguments:</strong></p>
No arguments required
</body>
</html>
\ No newline at end of file
website/docs/index.md
View file @ c60feb1b
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment