merge

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

@@ -149,6 +149,8 @@ BOOL: 'bool' ;
 TERMTYPE : 'term' ;*/
 FOREACH : 'foreach' ;
 THEONLY : 'theonly' ;
+CLOSED_BY : 'closed_by';
+DERIVABLE : 'derivable';
 INDENT : '{' ;
 DEDENT : '}' ;
 SEMICOLON : ';' ;

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

@@ -4,7 +4,6 @@ import edu.kit.formal.gui.model.InspectionModel;
 import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.KeyData;
 import javafx.beans.Observable;
-import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.ReadOnlyObjectProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.fxml.FXML;
@@ -20,18 +19,15 @@ import javafx.scene.layout.BorderPane;
  * @author S. Grebing
  */
 public class InspectionView extends BorderPane {
+    private final ReadOnlyObjectProperty<InspectionModel> model = new SimpleObjectProperty<>(
+            new InspectionModel()
+    );
     public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
-
     @FXML
     private SequentView sequentView;
-
     @FXML
     private ListView<GoalNode<KeyData>> goalView;
 
-    private ObjectProperty<InspectionModel> model = new SimpleObjectProperty<>(
-            new InspectionModel()
-    );
-
     public InspectionView() {
         Utils.createWithFXML(this);
 
@@ -42,7 +38,7 @@ public class InspectionView extends BorderPane {
             model.get().setSelectedGoalNodeToShow(b);
         });
 
-        model.get().selectedGoalNodeToShowProperty().addListener(
+        model.get().currentInterpreterGoalProperty().addListener(
                 (observable, oldValue, newValue) -> {
                     goalView.getSelectionModel().select(newValue);
                     if (newValue != null && newValue.getData() != null) {
@@ -57,6 +53,10 @@ public class InspectionView extends BorderPane {
         model.get().goalsProperty().bindBidirectional(goalView.itemsProperty());
         getGoalView().setCellFactory(GoalNodeListCell::new);
 
+        Utils.addDebugListener(model.get().goalsProperty());
+        Utils.addDebugListener(model.get().selectedGoalNodeToShowProperty());
+        Utils.addDebugListener(model.get().currentInterpreterGoalProperty());
+
         /*TODO redefine CSS bases on selected mode
         mode.addListener(o -> {
             getStyleClass().removeAll(
@@ -118,4 +118,4 @@ public class InspectionView extends BorderPane {
             setText(text);
         }
     }
-}
+}
\ No newline at end of file

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

@@ -31,7 +31,7 @@ import java.nio.charset.Charset;
 import java.util.*;
 
 /**
- * A controller for manageing the open script files in the dock nodes.
+ * A controller for managing the open script files in the dock nodes.
  *
  * @author Sarah Grebing
  */
@@ -185,14 +185,14 @@ public class ScriptController {
         return mainScript.get();
     }
 
-    public ObjectProperty<MainScriptIdentifier> mainScriptProperty() {
-        return mainScript;
-    }
-
     public void setMainScript(MainScriptIdentifier mainScript) {
         this.mainScript.set(mainScript);
     }
 
+    public ObjectProperty<MainScriptIdentifier> mainScriptProperty() {
+        return mainScript;
+    }
+
     private ScriptArea findEditor(ASTNode node) {
         File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName());
         return findEditor(f);

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

@@ -21,7 +21,6 @@ public class WelcomePane extends AnchorPane {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
         proofScriptDebugger.openScript(
-        //        new File("src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps")
                 new File("src/test/resources/edu/kit/formal/interpreter/contraposition/wo_branching.kps")
         );
 

src/main/java/edu/kit/formal/gui/model/InspectionModel.java

@@ -17,15 +17,10 @@ import javafx.scene.paint.Color;
  * @author Alexander Weigl
  */
 public class InspectionModel {
-    enum Mode {
-        LIVING, DEAD, POSTMORTEM,
-    }
-
-    private final ObjectProperty<ASTNode> node = new SimpleObjectProperty<>();
-    private final ListProperty<GoalNode<KeyData>> goals = new SimpleListProperty<>();
-    private final ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShow = new SimpleObjectProperty<>();
-    private final ObjectProperty<GoalNode<KeyData>> currentInterpreterGoal = new SimpleObjectProperty<>();
-
+    private final ObjectProperty<ASTNode> node = new SimpleObjectProperty<>(this, "node");
+    private final ListProperty<GoalNode<KeyData>> goals = new SimpleListProperty<>(this, "goals");
+    private final ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShow = new SimpleObjectProperty<>(this, "selectedGoalNodeToShow");
+    private final ObjectProperty<GoalNode<KeyData>> currentInterpreterGoal = new SimpleObjectProperty<>(this, "currentInterpreterGoal");
     private final MapProperty<GoalNode, Color> colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap());
     //private final StringProperty javaString = new SimpleStringProperty();
     private final SetProperty<Integer> highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet());
@@ -33,79 +28,78 @@ public class InspectionModel {
     private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty();
     private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
 
-
     public GoalNode<KeyData> getCurrentInterpreterGoal() {
         return currentInterpreterGoal.get();
     }
 
-    public ObjectProperty<GoalNode<KeyData>> currentInterpreterGoalProperty() {
-        return currentInterpreterGoal;
-    }
-
     public void setCurrentInterpreterGoal(GoalNode<KeyData> currentInterpreterGoal) {
         this.currentInterpreterGoal.set(currentInterpreterGoal);
     }
 
-    public Mode getMode() {
-        return mode.get();
+    public ObjectProperty<GoalNode<KeyData>> currentInterpreterGoalProperty() {
+        return currentInterpreterGoal;
     }
 
-    public ObjectProperty<Mode> modeProperty() {
-        return mode;
+    public Mode getMode() {
+        return mode.get();
     }
 
     public void setMode(Mode mode) {
         this.mode.set(mode);
     }
 
-    public ASTNode getNode() {
-        return node.get();
+    public ObjectProperty<Mode> modeProperty() {
+        return mode;
     }
 
-    public ObjectProperty<ASTNode> nodeProperty() {
-        return node;
+    public ASTNode getNode() {
+        return node.get();
     }
 
     public void setNode(ASTNode node) {
         this.node.set(node);
     }
 
-    public ObservableList<GoalNode<KeyData>> getGoals() {
-        return goals.get();
+    public ObjectProperty<ASTNode> nodeProperty() {
+        return node;
     }
 
-    public ListProperty<GoalNode<KeyData>> goalsProperty() {
-        return goals;
+    public ObservableList<GoalNode<KeyData>> getGoals() {
+        return goals.get();
     }
 
     public void setGoals(ObservableList<GoalNode<KeyData>> goals) {
         this.goals.set(goals);
     }
 
-    public GoalNode getSelectedGoalNodeToShow() {
-        return selectedGoalNodeToShow.get();
+    public ListProperty<GoalNode<KeyData>> goalsProperty() {
+        return goals;
     }
 
-    public ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShowProperty() {
-        return selectedGoalNodeToShow;
+    public GoalNode getSelectedGoalNodeToShow() {
+        return selectedGoalNodeToShow.get();
     }
 
     public void setSelectedGoalNodeToShow(GoalNode selectedGoalNodeToShow) {
         this.selectedGoalNodeToShow.set(selectedGoalNodeToShow);
     }
 
-    public ObservableMap<GoalNode, Color> getColorofEachGoalNodeinListView() {
-        return colorofEachGoalNodeinListView.get();
+    public ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShowProperty() {
+        return selectedGoalNodeToShow;
     }
 
-    public MapProperty<GoalNode, Color> colorofEachGoalNodeinListViewProperty() {
-        return colorofEachGoalNodeinListView;
+    public ObservableMap<GoalNode, Color> getColorofEachGoalNodeinListView() {
+        return colorofEachGoalNodeinListView.get();
     }
 
     public void setColorofEachGoalNodeinListView(ObservableMap<GoalNode, Color> colorofEachGoalNodeinListView) {
         this.colorofEachGoalNodeinListView.set(colorofEachGoalNodeinListView);
     }
 
+    public MapProperty<GoalNode, Color> colorofEachGoalNodeinListViewProperty() {
+        return colorofEachGoalNodeinListView;
+    }
+
     /*
         public String getJavaString() {
             return javaString.get();
@@ -123,35 +117,39 @@ public class InspectionModel {
         return highlightedJavaLines.get();
     }
 
-    public SetProperty<Integer> highlightedJavaLinesProperty() {
-        return highlightedJavaLines;
-    }
-
     public void setHighlightedJavaLines(ObservableSet<Integer> highlightedJavaLines) {
         this.highlightedJavaLines.set(highlightedJavaLines);
     }
 
-    public boolean isClosable() {
-        return closable.get();
+    public SetProperty<Integer> highlightedJavaLinesProperty() {
+        return highlightedJavaLines;
     }
 
-    public BooleanProperty closableProperty() {
-        return closable;
+    public boolean isClosable() {
+        return closable.get();
     }
 
     public void setClosable(boolean closable) {
         this.closable.set(closable);
     }
 
+    public BooleanProperty closableProperty() {
+        return closable;
+    }
+
     public boolean isIsInterpreterTab() {
         return isInterpreterTab.get();
     }
 
+    public void setIsInterpreterTab(boolean isInterpreterTab) {
+        this.isInterpreterTab.set(isInterpreterTab);
+    }
+
     public BooleanProperty isInterpreterTabProperty() {
         return isInterpreterTab;
     }
 
-    public void setIsInterpreterTab(boolean isInterpreterTab) {
-        this.isInterpreterTab.set(isInterpreterTab);
+    enum Mode {
+        LIVING, DEAD, POSTMORTEM,
     }
 }

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

@@ -21,14 +21,13 @@ public class KeyData {
     private static final String SEPARATOR = " // ";
     private final KeYEnvironment env;
     private final Proof proof;
+    private Node node;
 
     private String branchingLabel,
             ruleLabel,
             programLinesLabel,
             programStatementsLabel,
             nameLabel;
-
-    private Node node;
     private Goal goal;
 
     public KeyData(KeyData data, Goal node) {
@@ -117,6 +116,7 @@ public class KeyData {
     }
 
     public Node getNode() {
-        return getGoal().node();
+        return node;
+        //return getGoal().node();
     }
 }

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

 
-public class Simple {
-    /*@ public invariant log != null && log.length == 100; @*/
-    public int[] log = new int[100];
-
-    /*@ public invariant n >= 0; @*/
-    public int n;
-  
-  /*@ public normal_behavior
-  @	requires log != null;
-  @	ensures n == 0 && log != null;
-  @*/
-
-    public void init() {
-        for (int i = 0; i < log.length; i++) {
-            log[i] = 0;
-        }
-        n = 0;
-    }
+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 normal_behavior
-      @	requires n < 100;
-      @	ensures log[n] == x+y;
-      @ assignable log.*;
-      @*/
-    public void logging(int x, int y) {
-        if (n < 100) {
-            log[n] = x + y;
-        }
+      @ 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));
+      @ 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);@*/
+
+        return barr;
     }
 
     /*@ public normal_behavior
-      @	requires x >= 0 && y >= 0 && n <100;
-      @	ensures \result >=0;
-      @ assignable log.*;
-      @*/
-    public int example(int x, int y) {
-
-
-        if (log[n] == 0) {
-            logging(x, y);
-            return x + y;
-        } else {
-            return x + y;
+      @ ensures \dl_seqPerm(\dl_array2seq(a), \old(\dl_array2seq(a)));
+      @ assignable a[*];
+      */
+    public abstract 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 \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++) {
+            temp[i] = input[i];
         }
+        return temp;
 
     }
-    /*@ public normal_behavior
-      @	requires a != null && b != null && (\forall int i; 0 <= i < a.length; a[i] != b[i]);
-      @	ensures (\forall int i; 0 <= i < a.length; a[i] != b[i]) && \old(a) == \result;
-      @*/
 
-    public int[] compare(int[] a, int[] b){
 
-        return a;
+//    /*@ public normal_behavior
+//      @ requires c.length == b.length;
+//      @ ensures  \dl_seqPerm(\dl_array2seq(\result), \dl_array2seq(c));
+//      @ assignable b[*];
+//     */
+//    public int[] foo(int[] a){
+//        a = Simple.copyArray(c);
+////hier weiß ich: \dl_array2seq(c) == \dl_array2seq(a);
+//
+//        /*@ loop_invariant 0 <= i && i <= a.length && (\forall int j; 0 <= j < i; a[j] == b[j]) ;
+//          @ assignable b[*];
+//          @ decreases a.length -i;
+//          */
+//        for (int i = 0; i < a.length; i++) {
+//            b[i]= a[i];
+//        }
+//        //hier sollte ich wissen a = b
+//        sort(a);
+//        //hier sollte ich wissen permutation a,b
+//        return b;
+//    }
+
+
+
+
+    /*@ public normal_behavior
+      @ requires a[0] >= 0;
+      @ ensures \result > 0;
+      @ assignable \nothing;
+     */
+    public int getter(int[] a){
+        int test = a[0];
+        a[0] = a[1];
+        a[1] = test;
+        int ret = test+1;
+        return test;
     }
+    /*@ public normal_behavior
+      @ requires a[1] >= 0;
+      @ ensures \result > 0;
+      @ assignable \nothing;
+     */
+    public int getter2(int[] a){
+         int test = a[1];
+        a[1] = a[0];
+        a[0] = test;
+        int ret = test+1;
+        return test;
+    }
+//    /*@ public invariant log != null && log.length == 100; @*/
+//    public int[] log = new int[100];
+//
+//    /*@ public invariant n >= 0; @*/
+//    public int n;
+//
+//  /*@ public normal_behavior
+//  @	requires log != null;
+//  @	ensures n == 0 && log != null;
+//  @*/
+//
+//    public void init() {
+//        for (int i = 0; i < log.length; i++) {
+//            log[i] = 0;
+//        }
+//        n = 0;
+//    }
+//
+//    /*@ public normal_behavior
+//      @	requires n < 100;
+//      @	ensures log[n] == x+y;
+//      @ assignable log.*;
+//      @*/
+//    public void logging(int x, int y) {
+//        if (n < 100) {
+//            log[n] = x + y;
+//        }
+//
+//    }
+//
+//    /*@ public normal_behavior
+//      @	requires x >= 0 && y >= 0 && n <100;
+//      @	ensures \result >=0;
+//      @ assignable log.*;
+//      @*/
+//    public int example(int x, int y) {
+//
+//
+//        if (log[n] == 0) {
+//            logging(x, y);
+//            return x + y;
+//        } else {
+//            return x + y;
+//        }
+//
+//    }
+//    /*@ public normal_behavior
+//      @	requires a != null && b != null && (\forall int i; 0 <= i < a.length; a[i] != b[i]);
+//      @	ensures (\forall int i; 0 <= i < a.length; a[i] != b[i]) && \old(a) == \result;
+//      @*/
+//
+//    public int[] compare(int[] a, int[] b){
+//
+//        return a;
+//    }
+
 }
\ No newline at end of file