Commit 2bb39b6d authored by Sarah Grebing's avatar Sarah Grebing

interim

parent ffd9f954
......@@ -4,9 +4,9 @@
# Execute this in this folder.
# Set to key/key/deployment/components/
#COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
#COMPONENTS=$HOME/work/key/key/deployment/components/
COMPONENTS=lib/components/
#COMPONENTS=lib/components/
......
......@@ -74,6 +74,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
}
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
......
package edu.kit.iti.formal.psdbg.examples.java.bubbleSort;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class BubbleSortExample extends JavaExample {
public BubbleSortExample() {
setName("Bubble Sort");
setJavaFile(this.getClass().getResource("Bubblesort.java"));
defaultInit(getClass());
System.out.println(this);
}
}
......@@ -170,8 +170,14 @@ public class InspectionView extends BorderPane {
public void activate(PTreeNode<KeyData> node, State<KeyData> lastState) {
InspectionModel im = model.get();
im.getGoals().setAll(lastState.getGoals()); //TODO nullcheck
im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
if (lastState != null && lastState.getGoals() != null) {
im.getGoals().setAll(lastState.getGoals());
im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
} else {
lastState = node.getStepInvOver().getStateBeforeStmt();
im.getGoals().setAll(lastState.getGoals());
im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
}
//Experimental
List<PTreeNode<KeyData>> ctxn = node.getContextNodes();
......
......@@ -3,4 +3,5 @@ edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample
edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
\ No newline at end of file
edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
\ No newline at end of file
script test(){
impRight;
andLeft;
notLeft;
repeat { andLeft; }
exLeft;
andLeft;
eqSymm formula = `agatha = butler`;
nnf_imp2or formula=`\foral S w6;(hates(agatha,w6) -> hates(butler,w6))`;
}
script SolveAgathaRiddle_1() {
impRight;
andLeft;
......
class Bubblesort {
/*@
@ public normal_behaviour
@ requires arr != null;
@ requires arr.length > 0;
@ ensures (\forall int i, j; 0 <= i && i < j && j < arr.length; arr[i] <= arr[j]);
@ assignable arr[*];
@*/
public int[] bubbleSort(int[] arr) {
int temp = 0;
/*@
@ loop_invariant 0 <= i && i <= arr.length;
@ loop_invariant (\forall int a,b; a >= arr.length - i && b <= arr.length && a < b && i > 0; arr[a] <= arr[b]);
@ assignable arr[*], temp;
@ decreases arr.length - i;
@*/
for(int i=0; i < arr.length; i++){
/*@
@ loop_invariant 1 <= j && j <= arr.length - i + 1;
@ assignable arr[*], temp;
@ decreases arr.length - i - j;
@*/
for(int j=1; j < (arr.length-i); j++){
if(arr[j-1] > arr[j]){
//swap elements
temp = arr[j-1];
arr[j-1] = arr[j];
arr[j] = temp;
}
}
}
return arr;
}
/*@ public normal_behaviour
@ requires arr != null;
@ requires arr.length > 0;
@ ensures true;
@*/
public boolean test(int[] arr) {
arr = bubbleSort(arr);
for(int i = 0; i < arr.length - 1; i++) {
if(arr[i] > arr[i+1]) {
return false;
}
}
return true;
}
}
\ No newline at end of file
script bubbleSort_1(){
symbex;
cases{
default:
}
}
\ No newline at end of file
......@@ -311,6 +311,6 @@
.context-menu {
-fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin";
-fx-font-family: sans-serif;
-fx-font-size: 12pt;
-fx-font-size: 9pt;
//-fx-font-size: 9pt;
}
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