Commit 972e934f authored by Sarah Grebing's avatar Sarah Grebing

webpage and simpleJava example

parent 841fa46f
Pipeline #13755 failed with stage
in 2 minutes and 14 seconds
package edu.kit.iti.formal.psdbg.interpreter.funchdl; package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
import de.uka.ilkd.key.proof.Goal;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.parser.ast.Parameters; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral; import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import org.key_project.util.collection.ImmutableList;
import java.util.Collection; import java.util.Collection;
import java.util.HashMap; import java.util.HashMap;
...@@ -21,8 +25,9 @@ import java.util.Map; ...@@ -21,8 +25,9 @@ import java.util.Map;
* @version 1 (21.05.17) * @version 1 (21.05.17)
*/ */
@RequiredArgsConstructor @RequiredArgsConstructor
public class MacroCommandHandler implements CommandHandler { public class MacroCommandHandler implements CommandHandler<KeyData> {
@Getter private final Map<String, ProofMacro> macros; @Getter
private final Map<String, ProofMacro> macros;
public MacroCommandHandler() { public MacroCommandHandler() {
macros = new HashMap<>(); macros = new HashMap<>();
...@@ -40,20 +45,35 @@ public class MacroCommandHandler implements CommandHandler { ...@@ -40,20 +45,35 @@ public class MacroCommandHandler implements CommandHandler {
} }
@Override @Override
public void evaluate(Interpreter interpreter, public void evaluate(Interpreter<KeyData> interpreter,
CallStatement call, CallStatement call,
VariableAssignment params) { VariableAssignment params) {
//ProofMacro m = macros.get(call.getCommand()); //ProofMacro m = macros.get(call.getCommand());
Parameters p = new Parameters(); ProofMacro macro = KeYApi.getMacroApi().getMacro(call.getCommand());
p.put(new Variable("#2"), new StringLiteral(call.getCommand())); ProofMacroFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro,
CallStatement macroCall = new CallStatement("macro", p); interpreter.getCurrentState().getSelectedGoalNode().getData().getProof());
macroCall.setRuleContext(call.getRuleContext());
VariableAssignment newParam = new VariableAssignment(null); State<KeyData> state = interpreter.getCurrentState();
newParam.declare("#2", SimpleType.STRING); GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
newParam.assign("#2", Value.from(call.getCommand()));
//macro proofscript command
interpreter.getFunctionLookup().callCommand(interpreter, macroCall, newParam); try {
//uiControl.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0));
//TODO change MacroCommand.Parameters to public synchronized (macro) {
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
info = macro.applyTo(uiControl, expandedNode.getData().getNode(), null, uiControl);
ImmutableList<Goal> ngoals = expandedNode.getData().getProof().getSubtreeGoals(expandedNode.getData().getNode());
state.getGoals().remove(expandedNode);
for (Goal g : ngoals) {
KeyData kdn = new KeyData(expandedNode.getData(), g.node());
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode()));
}
}
} catch (InterruptedException e) {
e.printStackTrace();
} catch (Exception e) {
e.printStackTrace();
}
} }
} }
...@@ -48,7 +48,9 @@ public class WelcomePane extends AnchorPane { ...@@ -48,7 +48,9 @@ public class WelcomePane extends AnchorPane {
proofScriptDebugger.getWelcomePaneDock().close(); proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null); proofScriptDebugger.showActiveInspector(null);
Examples.loadExamples().forEach(example -> { Examples.loadExamples().forEach(example -> {
if (example.getName().equals("Transitive Permutation")) // if (example.getName().equals("Transitive Permutation"))
if (example.getName().equals("Simple Java Example"))
example.open(proofScriptDebugger); example.open(proofScriptDebugger);
}); });
......
...@@ -2,7 +2,7 @@ script t(){ ...@@ -2,7 +2,7 @@ script t(){
symbex; symbex;
cases{ cases{
case match `?X = 0 ==>`: case match `?X = 0 ==>`:
eqSymm on=`?X=0`[?X/?X]; eqSymm on=`?X=0`[];
} }
......
...@@ -13,7 +13,7 @@ ...@@ -13,7 +13,7 @@
.column>div{ .column>div{
float: left; float: left;
width: 33%; width: 33%;
text-align: center; text-align: left;
} }
.column img { .column img {
...@@ -63,63 +63,44 @@ A full description of the language and debugging-concept is published at <a href ...@@ -63,63 +63,44 @@ A full description of the language and debugging-concept is published at <a href
<div class="column"> <div class="column">
<div > <div >
<!--<img src="https://placeimg.com/150/150/any" />--> <h3>Inspection of different parts of the proof state</h3>
<h3>Stepping back and forth in Proof Script</h3>
<p> <p>
</p> The different parts of the proof state can be inspected:
<ul>
<li>list of open goals</li>
<li>sequent of selected open goal</li>
<li>path through program (if existing) for selected open goal</li>
</ul>
</p>
</div> </div>
<div > <div >
<!-- <img src="https://placeimg.com/150/150/any" /> --> <h3>Adjustable view on list of open goals</h3>
<h3>Different views onto one proof state</h3> <img src="img/simpleJavaGoalList.png" style="width:304px;height:228px;" />
</div> </div>
<div > <div >
<!-- <img src="https://placeimg.com/150/150/any" />--< <h3>Explore the proof tree of KeY</h3>
<h3>Run To Breakpoints in Script-Evaluation</h3>
</div> </div>
</div> </div>
<div style="clear: both;"/> <div style="clear: both;"/>
<div class="column"> <div class="column">
<div > <div >
<img src="https://placeimg.com/150/150/any" /> <h3>Stepwise evaluation of the proof script</h3>
<h3>Inspect proof State</h3>
<p> <p>
The proof script can be evaluated stepwise and by running to a set breakpoint.
</p> </p>
</div> </div>
<div > <div >
<img src="https://placeimg.com/150/150/any" /> <h3>Set a breakpoint and run execution to breakpoint</h3>
<h3>Feature 2</h3> <img src="img/simpleJava2.png" style="width:304px;height:228px;"/>
</div> </div>
<div >
<div > <h3> Step forward and step backward</h3>
<img src="https://placeimg.com/150/150/any" /> <img src="img/simpleJavaStep.png" style="width:304px;height:228px;" />
<h3>Feature 3</h3>
</div> </div>
</div> </div>
<div style="clear: both;"/> <div style="clear: both;"/>
<p>
<footer style="border-top: #ccc 1px solid">
<footer style="border-top: #ccc 1px solid">
Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a> Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
</footer> </footer>
</p> </p>
<!-- <h2>Getting Started</h2>
<h2>Downloads</h2>
<ul>
<li>Version 1.0
<p>
<a href="#">psdb-0.9-alpha.jar</a>
</p>
</li>
</ul>
-->
\ No newline at end of file
...@@ -2,4 +2,4 @@ ...@@ -2,4 +2,4 @@
mkdocs build --clean mkdocs build --clean
rsync --delete -vr site/ i57adm.ira.uka.de:htdocs/grebing/psdbg/ #rsync --delete -vr site/ i57adm.ira.uka.de:htdocs/grebing/psdbg/
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