Bugfix labels

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java

 package edu.kit.formal.gui.controller;
 
-import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.proof.init.ProofInputException;
@@ -147,10 +146,12 @@ public class DebuggerMainWindowController implements Initializable {
             }
         });
 
+
         proofTreeController.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
             imodel.setCurrentInterpreterGoal(newValue);
             //also update the selected to be shown
             imodel.setSelectedGoalNodeToShow(newValue);
+            //System.out.println("Pos: "+newValue.getData().getNode().getNodeInfo().getActiveStatement().getPositionInfo());
         });
 
         proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> {
@@ -175,6 +176,7 @@ public class DebuggerMainWindowController implements Initializable {
 
         chosenContract.addListener(o -> {
             javaCode.set(Utils.getJavaCode(chosenContract.get()));
+
             showCodeDock(null);
         });
 

src/main/java/edu/kit/formal/gui/controller/Events.java

 package edu.kit.formal.gui.controller;
 
 import com.google.common.eventbus.EventBus;
+import de.uka.ilkd.key.rule.TacletApp;
 import edu.kit.formal.gui.controls.ScriptArea;
 import lombok.Data;
+import lombok.RequiredArgsConstructor;
 
 /**
  * See http://codingjunkie.net/guava-eventbus/ for an introduction.
@@ -25,11 +27,15 @@ public class Events {
     }
 
     @Data
+    @RequiredArgsConstructor
     public static class FocusScriptArea {
         private final ScriptArea scriptArea;
 
-        public FocusScriptArea(ScriptArea area) {
-            this.scriptArea = area;
-        }
+    }
+
+    @Data
+    @RequiredArgsConstructor
+    public static class TacletApplicationEvent {
+        private final TacletApp app;
     }
 }

src/main/java/edu/kit/formal/gui/controls/InspectionView.java

@@ -36,6 +36,7 @@ public class InspectionView extends BorderPane {
         });
         goalView.getSelectionModel().selectedItemProperty().addListener((o, a, b) -> {
             model.get().setSelectedGoalNodeToShow(b);
+            model.get().setCurrentInterpreterGoal(b);
         });
 
         model.get().currentInterpreterGoalProperty().addListener(
@@ -47,6 +48,7 @@ public class InspectionView extends BorderPane {
                         // TODO weigl: get marked lines of the program, and set it
                         model.get().highlightedJavaLinesProperty().get()
                                 .clear();
+
                     }
                 });
 

src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java

@@ -9,12 +9,15 @@ import de.uka.ilkd.key.pp.AbbrevMap;
 import de.uka.ilkd.key.pp.NotationInfo;
 import de.uka.ilkd.key.pp.PosInSequent;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.rule.BuiltInRule;
+import de.uka.ilkd.key.rule.RuleSet;
+import de.uka.ilkd.key.rule.Taclet;
+import de.uka.ilkd.key.rule.TacletApp;
 import edu.kit.formal.gui.controller.DebuggerMainWindowController;
+import edu.kit.formal.gui.controller.Events;
 import edu.kit.formal.interpreter.KeYProofFacade;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
-import javafx.scene.Node;
 import javafx.scene.control.ContextMenu;
 import javafx.scene.control.Menu;
 import javafx.scene.control.MenuItem;
@@ -40,6 +43,7 @@ import java.util.stream.Collectors;
 public class TacletContextMenu extends ContextMenu {
 
     private static final Set<Name> CLUTTER_RULESETS = new LinkedHashSet<Name>();
+    private static final Set<Name> CLUTTER_RULES = new LinkedHashSet<Name>();
 
     static {
         CLUTTER_RULESETS.add(new Name("notHumanReadable"));
@@ -48,8 +52,6 @@ public class TacletContextMenu extends ContextMenu {
         CLUTTER_RULESETS.add(new Name("pullOutQuantifierEx"));
     }
 
-    private static final Set<Name> CLUTTER_RULES = new LinkedHashSet<Name>();
-
     static {
         CLUTTER_RULES.add(new Name("cut_direct_r"));
         CLUTTER_RULES.add(new Name("cut_direct_l"));
@@ -132,6 +134,8 @@ public class TacletContextMenu extends ContextMenu {
      */
     private static ImmutableList<TacletApp> removeRewrites(
             ImmutableList<TacletApp> list) {
+        return list;
+        /*
         ImmutableList<TacletApp> result = ImmutableSLList.<TacletApp>nil();
         Iterator<TacletApp> it = list.iterator();
 
@@ -141,6 +145,32 @@ public class TacletContextMenu extends ContextMenu {
             result = (taclet instanceof RewriteTaclet ? result
                     : result.prepend(tacletApp));
         }
+        return result;*/
+    }
+
+    /**
+     * Sorts the TacletApps with the given TacletAppComparator.
+     *
+     * @param finds the list to sort (will not be changed)
+     * @param comp  the comparator
+     * @return the sorted list
+     */
+    public static ImmutableList<TacletApp> sort(ImmutableList<TacletApp> finds,
+                                                TacletAppComparator comp) {
+        ImmutableList<TacletApp> result = ImmutableSLList.<TacletApp>nil();
+
+        List<TacletApp> list = new ArrayList<TacletApp>(finds.size());
+
+        for (final TacletApp app : finds) {
+            list.add(app);
+        }
+
+        Collections.sort(list, comp);
+
+        for (final TacletApp app : list) {
+            result = result.prepend(app);
+        }
+
         return result;
     }
 
@@ -180,6 +210,29 @@ public class TacletContextMenu extends ContextMenu {
 
     }
 
+    /**
+     public TacletFilter getFilterForInteractiveProving() {
+     if(this.filterForInteractiveProving == null) {
+     this.filterForInteractiveProving = new TacletFilter() {
+     protected boolean filter(Taclet taclet) {
+     String[] var2 = JoinProcessor.SIMPLIFY_UPDATE;
+     int var3 = var2.length;
+
+     for(int var4 = 0; var4 < var3; ++var4) {
+     String name = var2[var4];
+     if(name.equals(taclet.name().toString())) {
+     return false;
+     }
+     }
+
+     return true;
+     }
+     };
+     }
+
+     return this.filterForInteractiveProving;
+     }*/
+
     /**
      * Creates menu items for all given taclets. A submenu for insertion of
      * hidden terms will be created if there are any, and rare rules will be in
@@ -232,29 +285,6 @@ public class TacletContextMenu extends ContextMenu {
 
     }
 
-    /**
-     public TacletFilter getFilterForInteractiveProving() {
-     if(this.filterForInteractiveProving == null) {
-     this.filterForInteractiveProving = new TacletFilter() {
-     protected boolean filter(Taclet taclet) {
-     String[] var2 = JoinProcessor.SIMPLIFY_UPDATE;
-     int var3 = var2.length;
-
-     for(int var4 = 0; var4 < var3; ++var4) {
-     String name = var2[var4];
-     if(name.equals(taclet.name().toString())) {
-     return false;
-     }
-     }
-
-     return true;
-     }
-     };
-     }
-
-     return this.filterForInteractiveProving;
-     }*/
-
     /**
      * Manages the visibility of all menu items dealing with abbreviations based
      * on if the given term already is abbreviated and if the abbreviation is
@@ -288,6 +318,9 @@ public class TacletContextMenu extends ContextMenu {
         mediator.getUI().getProofControl().selectedTaclet(
                 ((TacletMenuItem) event.getSource()).getTaclet(), goal,
                 pos.getPosInOccurrence());*/
+
+        System.out.println("event = [" + event + "]");
+        Events.fire(new Events.TacletApplicationEvent(event));
     }
 
     /**
@@ -439,30 +472,4 @@ public class TacletContextMenu extends ContextMenu {
             //  parentController.forceRefresh();
         }
     }
-
-    /**
-     * Sorts the TacletApps with the given TacletAppComparator.
-     *
-     * @param finds the list to sort (will not be changed)
-     * @param comp  the comparator
-     * @return the sorted list
-     */
-    public static ImmutableList<TacletApp> sort(ImmutableList<TacletApp> finds,
-                                                TacletAppComparator comp) {
-        ImmutableList<TacletApp> result = ImmutableSLList.<TacletApp>nil();
-
-        List<TacletApp> list = new ArrayList<TacletApp>(finds.size());
-
-        for (final TacletApp app : finds) {
-            list.add(app);
-        }
-
-        Collections.sort(list, comp);
-
-        for (final TacletApp app : list) {
-            result = result.prepend(app);
-        }
-
-        return result;
-    }
 }

src/main/java/edu/kit/formal/gui/controls/WelcomePane.java

@@ -33,10 +33,10 @@ public class WelcomePane extends AnchorPane {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
         proofScriptDebugger.openScript(
-                new File("src/test/resources/edu/kit/formal/interpreter/dbg.kps")
+                new File("src/test/resources/edu/kit/formal/interpreter/javaExample/test.kps")
         );
         proofScriptDebugger.openJavaFile(
-                new File("src/test/resources/edu/kit/formal/interpreter/javaExample/TwoWaySwap.java"));
+                new File("src/test/resources/edu/kit/formal/interpreter/javaExample/Test.java"));
     }
 
     public void loadHelpPage(ActionEvent event) {

src/main/java/edu/kit/formal/interpreter/Interpreter.java

@@ -22,6 +22,7 @@ import java.util.logging.Logger;
 
 /**
  * Main Class for interpreter
+ * Interpreter keeps a stack of states
  *
  * @author S.Grebing
  */
@@ -155,10 +156,14 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
     @Override
     public Object visit(IsClosableCase isClosableCase) {
         State<T> currentStateToMatch = peekState();
-        GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
-        enterScope(isClosableCase);
-        //executebody
+        State<T> currentStateToMatchCopy = peekState().copy(); //deepcopy
+        GoalNode<T> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
+        GoalNode<T> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
 
+        enterScope(isClosableCase);
+        executeBody(isClosableCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
+        State<T> stateafterIsClosable = peekState();
+        //check if state is closed
         exitScope(isClosableCase);
         return false;
     }
@@ -498,7 +503,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         }
     }
 
-
+    /**
+     * Peek current state
+     *
+     * @return state on top of state stack
+     */
     public State<T> getCurrentState() {
         try {
             return stateStack.peek();
@@ -508,6 +517,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         }
     }
 
+    /**
+     * Create new state containing goals and selected goal node an push to stack
+     * @param goals
+     * @param selected
+     * @return state that is pushed to stack
+     */
     public State<T> newState(List<GoalNode<T>> goals, GoalNode<T> selected) {
         if (selected != null && !goals.contains(selected)) {
             throw new IllegalStateException("selected goal not in list of goals");
@@ -515,14 +530,29 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         return pushState(new State<>(goals, selected));
     }
 
+    /**
+     * Cretae a ew state conatining the goals but without selected goal node and push to stack
+     * @param goals
+     * @return
+     */
     public State<T> newState(List<GoalNode<T>> goals) {
         return newState(goals, null);
     }
 
+    /**
+     * Cretae a new state containing only the selected goal node and push to stack
+     * @param selected
+     * @return reference to state on stack
+     */
     public State<T> newState(GoalNode<T> selected) {
         return newState(Collections.singletonList(selected), selected);
     }
 
+    /**
+     * Push state to stack and return reference to this state
+     * @param state
+     * @return
+     */
     public State<T> pushState(State<T> state) {
         if (stateStack.contains(state)) {
             throw new IllegalStateException("State is already on the stack!");
@@ -531,6 +561,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         return state;
     }
 
+    /**
+     * Remove top level state from stack and throw an Exception if state does not equal expected state
+     * @param expected
+     * @return
+     */
     public State<T> popState(State<T> expected) {
         State<T> actual = stateStack.pop();
         if (!expected.equals(actual)) {
@@ -539,15 +574,26 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         return actual;
     }
 
+    /**
+     * Remove top level state from stack
+     * @return
+     */
     private State<T> popState() {
         return stateStack.pop();
     }
 
-
+    /**
+     * Lookup state on the stack but do not remove it
+     * @return
+     */
     public State<T> peekState() {
         return stateStack.peek();
     }
 
+    /**
+     * Get goalnodes from current state
+     * @return
+     */
     public List<GoalNode<T>> getCurrentGoals() {
         return getCurrentState().getGoals();
     }

src/main/java/edu/kit/formal/interpreter/data/KeyData.java

@@ -66,7 +66,7 @@ public class KeyData {
         Node cur = getNode();
         do {
             try {
-                String section = projection.apply(getNode());
+                String section = projection.apply(cur);
                 if (section != null) {
                     sb.append(section);
                     sb.append(SEPARATOR);
@@ -97,7 +97,8 @@ public class KeyData {
     public String getProgramLinesLabel() {
         if (programLinesLabel == null) {
             programLinesLabel = constructLabel(n ->
-                    Integer.toString(n.getNodeInfo().getExecStatementPosition().getLine()));
+                    Integer.toString(n.getNodeInfo().getExecStatementPosition().getLine())
+            );
         }
         return programLinesLabel;
     }
@@ -105,8 +106,10 @@ public class KeyData {
     public String getProgramStatementsLabel() {
         if (programStatementsLabel == null) {
             programStatementsLabel = constructLabel(n ->
+                    // n.getNodeInfo().getActiveStatement().toString());
                     n.getNodeInfo().getFirstStatementString());
         }
+
         return programStatementsLabel;
     }
 

src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java

@@ -11,6 +11,7 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import javafx.application.Platform;
 import javafx.beans.property.*;
 import javafx.collections.FXCollections;
+import javafx.concurrent.Worker;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
@@ -230,6 +231,9 @@ public class ProofTreeController {
         }
 
         //create interpreter service and start
+        if (interpreterService.getState() == Worker.State.SUCCEEDED) {
+            interpreterService.reset();
+        }
         interpreterService.interpreterProperty().set(currentInterpreter);
         interpreterService.mainScriptProperty().set(mainScript);
         interpreterService.start();
@@ -306,11 +310,11 @@ public class ProofTreeController {
         return currentHighlightNode.get();
     }
 
-    public ObjectProperty<ASTNode> currentHighlightNodeProperty() {
-        return currentHighlightNode;
-    }
-
     public void setCurrentHighlightNode(ASTNode currentHighlightNode) {
         this.currentHighlightNode.set(currentHighlightNode);
     }
+
+    public ObjectProperty<ASTNode> currentHighlightNodeProperty() {
+        return currentHighlightNode;
+    }
 }

src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java

@@ -152,10 +152,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         return createBinaryExpression(ctx, ctx.expression(), findOperator(ctx.op.getText()));
     }
 
-    @Override
-    public Object visitExprSubs(ScriptLanguageParser.ExprSubsContext ctx) {
-        return null;
-    }
+
 
     private Operator findOperator(String n) {
         return findOperator(n, 2);
@@ -221,8 +218,15 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     }
 
     //TODO implement
+
+
+    @Override
+    public Object visitExprSubst(ScriptLanguageParser.ExprSubstContext ctx) {
+        return null;
+    }
+
     @Override
-    public Object visitSubstExpression(ScriptLanguageParser.SubstExpressionContext ctx) {
+    public Object visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) {
         return null;
     }
 

src/main/resources/edu/kit/formal/gui/intro.html

@@ -7,7 +7,45 @@
 <body>
 <h1>Language Constructs</h1>
 <h2>Proof Commands</h2>
+<h3>KeY Rules</h3>
 All KeY rules can be used as proof command.
+The following command structure is used to apply single KeY rules onto a selected goal node.
+<br>
+RULENAME
+
+<!--Apply a single rule onto the current sequent. As unnamed argument add
+the name of the taclet to be applied. If the taclet matches only once
+on the entire sequent, the rule is applied. If it matches more than
+once you need to specify more. In that case you can first specify the
+sequence formula and then the number of the occurrence in the formula
+or the specific subterm via the 'on' keyword.
+If a rule has schema variables which must be instantiated manually,
+such instantiations can be provided as arguments. A schema variable
+named sv can be instantiated by setting the argument sv="..." or by
+setting inst_sv="..." (the latter works also for conflict cases like
+inst_occ="...").
+
+Examples:
+rule andRight;
+# if there is only one matching spot on the sequent
+
+rule eqSymm formula="a=b";
+# changes sequent "a=b ==> c=d" to "b=a ==> c=d"
+# "rule eqSymm;" alone would have been ambiguous.
+
+rule eqSymm formula="a=b->c=d" occ=2;
+# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
+# occurrence number needed since there are
+# two possible applications on the formula
+
+rule eqSymm formula="a=b->c=d" on="c=d";
+# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
+# same as above, but using the option to specify a
+# subterm instead of an occurrence number.
+
+rule cut cutFormula="x > y";
+# almost the same as 'cut "x>y"'
+-->
 <!--A rule command has the following syntax:<br>
 RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")?
 <br>with:

src/main/resources/log4j2.properties

@@ -18,7 +18,6 @@ logger.file.name=guru.springframework.blog.log4j2properties
 logger.file.level = debug
 logger.file.appenderRefs = file
 logger.file.appenderRef.file.ref = LOGFILE
-
-rootLogger.level = debug
+rootLogger.level=info
 rootLogger.appenderRefs = stdout
 rootLogger.appenderRef.stdout.ref = STDOUT
\ No newline at end of file

src/test/resources/edu/kit/formal/interpreter/javaExample/Test.java

+public class Test{
+
+
+
+    /*@ public normal_behavior
+      @ requires x >= 0;
+      @ ensures \result >0;
+      @*/
+    public int foo(int x){
+        if(x > 0){
+            x--;
+        }else{
+            x++;
+        }
+        return x++;
+    }
+}
\ No newline at end of file

src/test/resources/edu/kit/formal/interpreter/javaExample/test.kps

+
+script t1(){
+    symbex;
+    
+}
+

src/test/resources/edu/kit/formal/interpreter/paperExample/Simple.java

-
-public final class Simple {
-
-    //@ ghost \seq c_seq;
-    //@ ghost \seq b_seq;
-
-    private /*@spec_public*/ static int[] barr;
-    private /*@spec_public*/ static int[] carr;
-
+ public final class Simple {
+ 
+ 
+    boolean b1;
+    boolean b2;
+    
     /*@ public normal_behavior
-      @ requires carr.length == barr.length;
-      @ requires aarr != barr && aarr != carr;
-      @ //requires c_seq == \dl_array2seq(carr);
-      @ //ensures \dl_array2seq(carr) == \dl_array2seq(barr);
-      @ ensures \dl_seqPerm(\dl_array2seq(barr), \dl_array2seq(carr));
+      @ ensures \dl_seqPerm(\dl_array2seq(\result), \old(\dl_array2seq(aarr)));
       @ assignable \everything;
      */
     public int[] transitive(int[] aarr){
-        aarr = Simple.copyArray(carr); // a=c && perm a,c
-
-
-        sort(aarr); //perm(a,c)
-        // --> result0@aftercopyArray perm result0@aftersort
-
-        barr = Simple.copyArray(aarr); //b = perm(a)
-        //carr@aftercopy2 = carr@aftercopy1
-        //carr@aftersort = carr@aftercopy2
-        //result0@aftersort = result1@aftercopyarray2
-        //barr@aftercopyarray2 = result0@aftersort
-
-
-        /*@ //set b_seq =  \dl_array2seq(barr);@*/
-
+        aarr = Simple.copyArray(aarr); 
+        sort(aarr); 
+        int[] barr = Simple.copyArray(aarr);
+        
+        if(b1){barr = Simple.copyArray(aarr);} 
+        if(b2){log(barr);}
         return barr;
     }
 
@@ -38,132 +22,20 @@ public final class Simple {
       @ ensures \dl_seqPerm(\dl_array2seq(a), \old(\dl_array2seq(a)));
       @ assignable a[*];
       */
-    public abstract void sort(int[] a);
+    public void sort(int[] a){};
 
     /*@ public normal_behavior
-      @ //ensures \dl_array2seq(input) == \dl_array2seq(\result);
-      @ // ensures (\forall int i; 0 <= i < input.length; input[i] == \result[i]) && \result.length == input.length;
+      @ ensures (\forall int i; 0 <= i < input.length; input[i] == \result[i]) 
+      @ && \result.length == input.length;
       @ ensures \fresh(\result);
       @ ensures \dl_seqPerm(\dl_array2seq(\result), \dl_array2seq(input));
       @ assignable \nothing;
       */
-    public /*@helper@*/ static int[] copyArray(int[] input){
-        int[] temp = new int[input.length];
-        /*@ loop_invariant 0 <= i && i <= temp.length && (\forall int j; 0 <= j < i; temp[j] == input[j]) ;
-          @ assignable temp[*];
-          @ decreases temp.length-i;
-          */
-        for (int i = 0; i < input.length; i++) {