diff --git a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 index 82002884d5b876512b94149dbac7a46fea4e80d8..08e75dacbd482b230b6cff322ed909a820e58a6a 100644 --- a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 +++ b/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 : ';' ; diff --git a/src/main/java/edu/kit/formal/gui/controls/InspectionView.java b/src/main/java/edu/kit/formal/gui/controls/InspectionView.java index ef9eac30480c25edfc283854a0fdbdc38c3a38c8..5cc5f58ef7b86fc857e05fea36e7356ce5ebb1ec 100644 --- a/src/main/java/edu/kit/formal/gui/controls/InspectionView.java +++ b/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 model = new SimpleObjectProperty<>( + new InspectionModel() + ); public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu(); - @FXML private SequentView sequentView; - @FXML private ListView> goalView; - private ObjectProperty 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 diff --git a/src/main/java/edu/kit/formal/gui/controls/ScriptController.java b/src/main/java/edu/kit/formal/gui/controls/ScriptController.java index 48a441d91075b5b8020fc54575307084a1cc7ffa..71e0bf2705ddda6850e7fa91d70f20794cd52d3a 100644 --- a/src/main/java/edu/kit/formal/gui/controls/ScriptController.java +++ b/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 mainScriptProperty() { - return mainScript; - } - public void setMainScript(MainScriptIdentifier mainScript) { this.mainScript.set(mainScript); } + public ObjectProperty mainScriptProperty() { + return mainScript; + } + private ScriptArea findEditor(ASTNode node) { File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName()); return findEditor(f); diff --git a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java b/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java index 4f77570e8dd3967ac8bfd1c22ba9eab9d64ca3b1..dc18a07c25af01f3bae4c3f05c1e9bd4ac6aee71 100644 --- a/src/main/java/edu/kit/formal/gui/controls/WelcomePane.java +++ b/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") ); diff --git a/src/main/java/edu/kit/formal/gui/model/InspectionModel.java b/src/main/java/edu/kit/formal/gui/model/InspectionModel.java index b33b3f5670103fdc9080bbe7cdff2f08fe906b4f..fa15c3387631faf2b3cb538b522c7b829483e2f7 100644 --- a/src/main/java/edu/kit/formal/gui/model/InspectionModel.java +++ b/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 node = new SimpleObjectProperty<>(); - private final ListProperty> goals = new SimpleListProperty<>(); - private final ObjectProperty> selectedGoalNodeToShow = new SimpleObjectProperty<>(); - private final ObjectProperty> currentInterpreterGoal = new SimpleObjectProperty<>(); - + private final ObjectProperty node = new SimpleObjectProperty<>(this, "node"); + private final ListProperty> goals = new SimpleListProperty<>(this, "goals"); + private final ObjectProperty> selectedGoalNodeToShow = new SimpleObjectProperty<>(this, "selectedGoalNodeToShow"); + private final ObjectProperty> currentInterpreterGoal = new SimpleObjectProperty<>(this, "currentInterpreterGoal"); private final MapProperty colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap()); //private final StringProperty javaString = new SimpleStringProperty(); private final SetProperty highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet()); @@ -33,79 +28,78 @@ public class InspectionModel { private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty(); private ObjectProperty mode = new SimpleObjectProperty<>(); - public GoalNode getCurrentInterpreterGoal() { return currentInterpreterGoal.get(); } - public ObjectProperty> currentInterpreterGoalProperty() { - return currentInterpreterGoal; - } - public void setCurrentInterpreterGoal(GoalNode currentInterpreterGoal) { this.currentInterpreterGoal.set(currentInterpreterGoal); } - public Mode getMode() { - return mode.get(); + public ObjectProperty> currentInterpreterGoalProperty() { + return currentInterpreterGoal; } - public ObjectProperty 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 modeProperty() { + return mode; } - public ObjectProperty nodeProperty() { - return node; + public ASTNode getNode() { + return node.get(); } public void setNode(ASTNode node) { this.node.set(node); } - public ObservableList> getGoals() { - return goals.get(); + public ObjectProperty nodeProperty() { + return node; } - public ListProperty> goalsProperty() { - return goals; + public ObservableList> getGoals() { + return goals.get(); } public void setGoals(ObservableList> goals) { this.goals.set(goals); } - public GoalNode getSelectedGoalNodeToShow() { - return selectedGoalNodeToShow.get(); + public ListProperty> goalsProperty() { + return goals; } - public ObjectProperty> selectedGoalNodeToShowProperty() { - return selectedGoalNodeToShow; + public GoalNode getSelectedGoalNodeToShow() { + return selectedGoalNodeToShow.get(); } public void setSelectedGoalNodeToShow(GoalNode selectedGoalNodeToShow) { this.selectedGoalNodeToShow.set(selectedGoalNodeToShow); } - public ObservableMap getColorofEachGoalNodeinListView() { - return colorofEachGoalNodeinListView.get(); + public ObjectProperty> selectedGoalNodeToShowProperty() { + return selectedGoalNodeToShow; } - public MapProperty colorofEachGoalNodeinListViewProperty() { - return colorofEachGoalNodeinListView; + public ObservableMap getColorofEachGoalNodeinListView() { + return colorofEachGoalNodeinListView.get(); } public void setColorofEachGoalNodeinListView(ObservableMap colorofEachGoalNodeinListView) { this.colorofEachGoalNodeinListView.set(colorofEachGoalNodeinListView); } + public MapProperty colorofEachGoalNodeinListViewProperty() { + return colorofEachGoalNodeinListView; + } + /* public String getJavaString() { return javaString.get(); @@ -123,35 +117,39 @@ public class InspectionModel { return highlightedJavaLines.get(); } - public SetProperty highlightedJavaLinesProperty() { - return highlightedJavaLines; - } - public void setHighlightedJavaLines(ObservableSet highlightedJavaLines) { this.highlightedJavaLines.set(highlightedJavaLines); } - public boolean isClosable() { - return closable.get(); + public SetProperty 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, } } diff --git a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java b/src/main/java/edu/kit/formal/interpreter/data/KeyData.java index a411dc676abccc8c52b7a07276aa2986ce2b98f8..31ad086f030b273aa51d4c4e5db9faf803be4e93 100644 --- a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java +++ b/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(); } } diff --git a/src/test/resources/edu/kit/formal/interpreter/paperExample/Simple.java b/src/test/resources/edu/kit/formal/interpreter/paperExample/Simple.java index b9f8b892c1b3052ce85b9581e8ab01d237962fdb..cfce316d96504e9db2453bb05854949059fbfa20 100644 --- a/src/test/resources/edu/kit/formal/interpreter/paperExample/Simple.java +++ b/src/test/resources/edu/kit/formal/interpreter/paperExample/Simple.java @@ -1,58 +1,169 @@ -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