Commit e237f563 authored by Sarah Grebing's avatar Sarah Grebing

Testcase for isclosable

parent ddc82c18
Pipeline #12490 failed with stage
in 1 minute and 40 seconds
package edu.kit.formal.interpreter;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
import org.antlr.v4.runtime.CharStreams;
import org.junit.Assert;
import org.junit.Before;
import org.junit.Test;
import java.io.File;
import java.io.IOException;
import java.io.InputStream;
import java.util.List;
/**
* Created by sarah on 8/2/17.
*/
public class KeYInterpreterTest {
KeYProofFacade facade;
@Before
public void init() {
facade = new KeYProofFacade();
}
public Interpreter<KeyData> execute(InputStream is) throws IOException {
List<ProofScript> scripts = Facade.getAST(CharStreams.fromStream(is));
InterpreterBuilder ib = facade.buildInterpreter();
Interpreter<KeyData> i = ib.build();
i.interpret(scripts.get(0));
return i;
}
@Test
public void testIsClosable() throws IOException, ProblemLoaderException {
facade.loadKeyFile(new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key"));
Interpreter<KeyData> i = execute(getClass().getResourceAsStream("contraposition/testIsClosable.kps"));
List<GoalNode<KeyData>> goals = i.getCurrentState().getGoals();
Assert.assertEquals(2, goals.size());
for (GoalNode<KeyData> goal : goals) {
Assert.assertEquals("Label for node " + goal.getData().getNode(), "impLeft // impRight // $$", goal.getData().getRuleLabel());
}
// Assert.assertEquals(10, i.getCurrentState().getGoals().size());
}
}
script t1(){
impRight;
impLeft;
cases{
case match isCloseable:{
impRight; //should not close proof
}
}
}
\ No newline at end of file
script t1(){
symbex;
cases{
case match isCloseable:{
andRight; //should not close proof
case match '.*x.*':{
auto;
}
// case match `T >= 0 ==> ` using[ ?T:int]:{
// auto;
// }
default{
auto;
}
}
}
script t1(){
symbex;
cases{
case match '.*x.*':{
auto;
case match isCloseable:{
andRight; //should not close proof
}
// case match `T >= 0 ==> ` using[ ?T:int]:{
// auto;
// }
default{
auto;
}
}
}
\ 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