Commit 51b45a17 authored by Alexander Weigl's avatar Alexander Weigl

add test case for Quicksort and ScriptTree construction

parent 213ed260
Pipeline #30545 passed with stages
in 1 minute and 4 seconds
...@@ -177,7 +177,7 @@ public class KeYProofFacade { ...@@ -177,7 +177,7 @@ public class KeYProofFacade {
* Build the KeYInterpreter that handles the execution of the loaded key problem sourceName * Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
*/ */
public InterpreterBuilder buildInterpreter() { public InterpreterBuilder buildInterpreter() {
assert readyToExecute.getValue(); //weigl: duplicate with next line: assert readyToExecute.getValue();
assert getEnvironment() != null && getProof() != null : "No proof loaded"; assert getEnvironment() != null && getProof() != null : "No proof loaded";
InterpreterBuilder interpreterBuilder = new InterpreterBuilder(); InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
interpreterBuilder interpreterBuilder
......
...@@ -4,6 +4,8 @@ import de.uka.ilkd.key.proof.Proof; ...@@ -4,6 +4,8 @@ import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain; import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import javafx.beans.value.ChangeListener; import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue; import javafx.beans.value.ObservableValue;
import lombok.Getter;
import lombok.Setter;
import org.apache.commons.io.IOUtils; import org.apache.commons.io.IOUtils;
import java.io.*; import java.io.*;
...@@ -11,26 +13,18 @@ import java.net.URL; ...@@ -11,26 +13,18 @@ import java.net.URL;
import java.nio.charset.Charset; import java.nio.charset.Charset;
/** /**
* Under construction!!!!!!
* @author Alexander Weigl * @author Alexander Weigl
*/ */
public class JavaExample extends Example { public class JavaExample extends Example {
@Getter
@Setter
private URL projectFile;
public void setJavaFile(URL javaFile) {
this.javaFile = javaFile;
}
//public void setProjectFile(URL projectFile){this.projectFile = projectFile;}
protected URL javaFile; protected URL javaFile;
@Getter
@Setter
protected URL settingsFile; protected URL settingsFile;
@Getter
public void setSettingsFile(URL settingsFile) { @Setter
this.settingsFile = settingsFile; private URL projectFile;
}
@Override @Override
public void open(DebuggerMain debuggerMain) { public void open(DebuggerMain debuggerMain) {
......
package edu.kit.iti.formal.psdbg.gui.controls; package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.base.Strings; import com.google.common.base.Strings;
import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter; import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder; import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework; import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.Facade; import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.scene.control.TreeItem; import javafx.scene.control.TreeItem;
...@@ -21,13 +24,11 @@ import java.util.List; ...@@ -21,13 +24,11 @@ import java.util.List;
public class ProofTreeTest { public class ProofTreeTest {
private KeYProofFacade facade; private KeYProofFacade facade;
private List<ProofScript> scripts;
private Interpreter<KeyData> interpreter;
private static void printTree(TreeItem<TreeNode> rootItem, int level) { private static void printTree(TreeItem<TreeNode> rootItem, int level) {
System.out.format("%s* %s%n", Strings.repeat(" ", level * 4), rootItem.getValue().label); System.out.format("%s* %s%n", Strings.repeat(" ", level * 4), rootItem.getValue().label);
rootItem.getChildren().forEach(item -> { rootItem.getChildren().forEach(item -> {
printTree(item, level+1); printTree(item, level + 1);
}); });
} }
...@@ -37,7 +38,9 @@ public class ProofTreeTest { ...@@ -37,7 +38,9 @@ public class ProofTreeTest {
} }
@Test @Test
public void testScriptTree() throws IOException, ProblemLoaderException { public void testScriptTreeContraPosition() throws IOException, ProblemLoaderException {
List<ProofScript> scripts;
Interpreter<KeyData> interpreter;
File keyProblem = new File(getClass().getResource("contraposition.key").getFile()); File keyProblem = new File(getClass().getResource("contraposition.key").getFile());
facade.loadKeyFileSync(keyProblem); facade.loadKeyFileSync(keyProblem);
scripts = Facade.getAST(CharStreams.fromStream(getClass().getResourceAsStream("proofTreeScript.kps"))); scripts = Facade.getAST(CharStreams.fromStream(getClass().getResourceAsStream("proofTreeScript.kps")));
...@@ -65,5 +68,31 @@ public class ProofTreeTest { ...@@ -65,5 +68,31 @@ public class ProofTreeTest {
} }
@Test
public void testScriptTreeQuicksort() throws IOException, ProblemLoaderException, ProofInputException {
QuickSort qs = new QuickSort();
File javaFile = new File(qs.getJavaFile().getFile());
List<Contract> contracts = facade.getContractsForJavaFile(javaFile);
Contract c = contracts.get(0);
facade.activateContract(c);
System.out.println("Contract: '" + c.getName() + "' activated!");
List<ProofScript> scripts = Facade.getAST(
CharStreams.fromStream(qs.getScriptFile().openStream()));
System.out.println("Script loaded.");
InterpreterBuilder ib = facade.buildInterpreter();
KeyInterpreter interpreter = ib.build();
DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, scripts.get(0));
System.out.println("Interpreter ready! Start proofing...");
interpreter.interpret(scripts.get(0));
System.out.println("Script successfully finished!");
System.out.println("Begin construction of the tree...");
ScriptTreeGraph stg = new ScriptTreeGraph();
stg.createGraph(df.getPtreeManager().getStartNode(), facade.getProof().root());
System.out.println("stg = " + stg);
}
} }
\ No newline at end of file
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