diff --git a/src/pureVerify.sh b/src/pureVerify.sh new file mode 100755 index 00000000..321b93ce --- /dev/null +++ b/src/pureVerify.sh @@ -0,0 +1,35 @@ +#!/bin/bash +printf "bst-find\n" +krun -cMainClass="ListItem(\"bst\")" --prove verification/bst-find-spec.k bst.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "bst-insert\n" + krun -cMainClass="ListItem(\"bst\")" --prove verification/bst-insert-spec.k bst.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "bst-delete(assertionError)\n" + krun -cMainClass="ListItem(\"bst\")" --prove verification/bst-delete-spec.k bst.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "avl-find\n" + krun -cMainClass="ListItem(\"avl\")" --prove verification/avl-find-spec.k avl.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "avl-insert(this one takes more than a thousand steps to prove, may need ulimit -c unlimited before starting Java)\n" + krun -cMainClass="ListItem(\"avl\")" --prove verification/avl-insert-spec.k avl.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "avl-delete(assertionError)\n" + krun -cMainClass="ListItem(\"avl\")" --prove verification/avl-delete-spec.k avl.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "rbt-find\n" + krun -cMainClass="ListItem(\"rbt\")" --prove verification/rbt-find-spec.k rbt.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "rbt-insert\n" + krun -cMainClass="ListItem(\"rbt\")" --prove verification/rbt-insert-spec.k rbt.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "rbt-delete\n" + krun -cMainClass="ListItem(\"rbt\")" --prove verification/rbt-delete-spec.k rbt.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "reverse\n" + krun -cMainClass="ListItem(\"listNode\")" --prove verification/reverse-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "append\n" + krun -cMainClass="ListItem(\"listNode\")" --prove verification/append-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "bubble-sort\n" + krun -cMainClass="ListItem(\"listNode\")" --prove verification/bubble-sort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "insertion-sort\n" + krun -cMainClass="ListItem(\"listNode\")" --prove verification/insertion-sort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "quick-sort\n" + krun -cMainClass="ListItem(\"listNode\")" --prove verification/quicksort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "merge-sort\n" + krun -cMainClass="ListItem(\"listNode\")" --prove verification/merge-sort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "sum\n" +krun -cMainClass="ListItem(\"sum\")" --prove verification/sum-iterative-spec.k sum.java.pkast --smt_prelude ../../k/k-distribution/include/z3/basic.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" +printf "min\n" +krun -cMainClass="ListItem(\"min\")" --prove verification/min-spec.k min.java.pkast --smt_prelude ../../k/k-distribution/include/z3/basic.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" diff --git a/src/run12.sh b/src/run12.sh new file mode 100644 index 00000000..44f908d6 --- /dev/null +++ b/src/run12.sh @@ -0,0 +1,50 @@ +#!/bin/bash -x + + + + rm -rf prep/java-prep-kompiled exec/java-exec-kompiled && kjkompile.sh + + + + rm -f bst.java.pkast && kjrun.sh verification/bst.java + + rm -f avl.java.pkast && kjrun.sh verification/avl.java + + rm -f listNode.java.pkast && kjrun.sh verification/listNode.java + + + + ( cd verification && rm -rf java-verification-kompiled && kompile java-verification.k ) + + + + krun -cMainClass="ListItem(\"bst\")" --prove verification/bst-find-spec.k bst.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"bst\")" --prove verification/bst-insert-spec.k bst.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"bst\")" --prove verification/bst-delete-spec.k bst.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + + + krun -cMainClass="ListItem(\"avl\")" --prove verification/avl-find-spec.k avl.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"avl\")" --prove verification/avl-insert-spec.k avl.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"avl\")" --prove verification/avl-delete-spec.k avl.java.pkast --smt_prelude ../../k/k-distribution/include/z3/search_tree.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + + + krun -cMainClass="ListItem(\"listNode\")" --prove verification/reverse-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"listNode\")" --prove verification/append-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + + + krun -cMainClass="ListItem(\"listNode\")" --prove verification/bubble-sort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"listNode\")" --prove verification/insertion-sort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"listNode\")" --prove verification/quicksort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + + krun -cMainClass="ListItem(\"listNode\")" --prove verification/merge-sort-spec.k listNode.java.pkast --smt_prelude ../../k/k-distribution/include/z3/sorted_list.smt2 -v --debug -d verification --symbolic-execution --statistics on --parser "cat" -cDissolveAllExceptOut="false" + diff --git a/src/verification/java-verification.k b/src/verification/java-verification.k index 85f2e559..2ce62069 100644 --- a/src/verification/java-verification.k +++ b/src/verification/java-verification.k @@ -1,5 +1,6 @@ require "../exec/java-exec.k" require "tree_pattern.k" +require "rbt_pattern.k" require "int_set.k" require "list_pattern.k" require "int_list.k" @@ -8,5 +9,6 @@ module JAVA-VERIFICATION imports JAVA-EXEC imports TREE-PATTERN imports LIST-PATTERN + imports RBT-PATTERN endmodule diff --git a/src/verification/rbt-delete-spec.k b/src/verification/rbt-delete-spec.k new file mode 100644 index 00000000..8f9a7e7c --- /dev/null +++ b/src/verification/rbt-delete-spec.k @@ -0,0 +1,184 @@ +require "java-verification.k" + +module RBT-INSERT-SPEC + imports JAVA-VERIFICATION +//proved +rule + + + + (class String2Id(".rbt")).String2Id("color"):Id((TP:RawRefVal)::(class String2Id(".rbt"))) + => + ctree_color(T)::int + ... + .Map + ... + + + + CLASSES:Bag + 0 + .K + ExecutionPhase + ... .Map => ?_:Map ... + .Set + I:Int => ?_:Int + ... ctree(TP)(T:CTree) ... +ensures ctree_color(T) ==K 1 orBool ctree_color(T) ==K 0 +//proved +rule + + + + (class String2Id(".rbt")).String2Id("find_min"):Id((TP:RawRefVal)::(class String2Id(".rbt"))) + + => + ?M:Int::int + ... + .Map +... + + + + CLASSES:Bag + 0 + .K + ExecutionPhase + ... .Map => ?_:Map ... + .Set + I:Int => ?_:Int + + ... ctree(TP)(T:CTree) ... +requires rbt(T) andBool TP =/=K null +ensures (?M inIntSet ctree_keys(T)) andBool ({ ?M } <=IntSet ctree_keys(T)) andBool ?M >=Int -2147483648 andBool ?M <=Int 2147483647 + +rule + + + + (class String2Id(".rbt")).String2Id("left_remove_fixup"):Id(objectRef(?P1:Int, class String2Id(".rbt"))::(class String2Id(".rbt"))) + => + objectRef(?P2:Int, class String2Id(".rbt"))::(class String2Id(".rbt")) + ... + .Map +... + + + + CLASSES:Bag + 0 + .K + ExecutionPhase + ... .Map => ?_:Map ... + .Set + I:Int => ?_:Int +... ( + + ?P1 + + + class String2Id(".rbt") + + + + class String2Id(".rbt") + + + String2Id("value") |-> I1:Int :: int + String2Id("color") |-> C1:Int :: int + String2Id("left") |-> L1:RawRefVal :: class String2Id(".rbt") + String2Id("right") |-> objectRef(R1:Int, class String2Id(".rbt")) :: class String2Id(".rbt") + + + noValue + + + + + class String2Id("java.lang.Object") + + + .Map + + + noValue + + + + + + R1 + + + class String2Id(".rbt") + + + + class String2Id(".rbt") + + + String2Id("value") |-> RT1:Int :: int + String2Id("color") |-> RC1:Int :: int + String2Id("left") |-> RL1:RawRefVal :: class String2Id(".rbt") + String2Id("right") |-> RR1:RawRefVal :: class String2Id(".rbt") + + + noValue + + + + + class String2Id("java.lang.Object") + + + .Map + + + noValue + + + + ctree(L1)(TL1:CTree) + ctree(RL1)(TRL1:CTree) + ctree(RR1)(TRR1:CTree) + => + + + ?P2 + + + class String2Id(".rbt") + + + + class String2Id(".rbt") + + + String2Id("value") |-> ?I2:Int :: int + String2Id("color") |-> ?C2:Int :: int + String2Id("left") |-> ?L2:RawRefVal :: class String2Id(".rbt") + String2Id("right") |-> ?R2:RawRefVal :: class String2Id(".rbt") + + + noValue + + + + + class String2Id("java.lang.Object") + + + .Map + + + noValue + + + + ctree(?L2)(?TL2:CTree) + ctree(?R2)(?TR2:CTree) + ) (.Bag => ?_:Bag) +... +//not finished +endmodule + diff --git a/src/verification/rbt-find-spec.k b/src/verification/rbt-find-spec.k new file mode 100644 index 00000000..86e2f5af --- /dev/null +++ b/src/verification/rbt-find-spec.k @@ -0,0 +1,32 @@ +require "java-verification.k" + +module RBT-FIND-SPEC + imports JAVA-VERIFICATION + +rule + + + + + (class String2Id(".rbt")).String2Id("find"):Id(V:Int::int, (TP:RawRefVal)::(class String2Id(".rbt"))) + => + ?B:Bool::bool + ... + .Map +... + + + + CLASSES:Bag + 0 + .K + ExecutionPhase + ... .Map => ?_:Map ... + .Set + I:Int => ?_:Int + + ... ctree(TP)(T:CTree) ... +requires rbt(T) andBool V >=Int -2147483648 andBool V <=Int 2147483647 +ensures (?B) ==K (V inIntSet ctree_keys(T)) +endmodule + diff --git a/src/verification/rbt-insert-spec.k b/src/verification/rbt-insert-spec.k new file mode 100644 index 00000000..8b0a2063 --- /dev/null +++ b/src/verification/rbt-insert-spec.k @@ -0,0 +1,137 @@ +require "java-verification.k" + +module RBT-INSERT-SPEC + imports JAVA-VERIFICATION +//only color rule got proved +rule + + + + (class String2Id(".rbt")).String2Id("color"):Id((TP:RawRefVal)::(class String2Id(".rbt"))) + => + ctree_color(T)::int + ... + .Map + ... + + + + CLASSES:Bag + 0 + .K + ExecutionPhase + ... .Map => ?_:Map ... + .Set + I:Int => ?_:Int + ... ctree(TP)(T:CTree) ... +ensures ctree_color(T) ==K 1 orBool ctree_color(T) ==K 0 + +rule + + + + (class String2Id(".rbt")).String2Id("insert_aux"):Id(V:Int::int, (TP1:RawRefVal)::(class String2Id(".rbt"))) + => + objectRef(?P:Int, class String2Id(".rbt"))::(class String2Id(".rbt")) + ... + .Map + ... + + + + CLASSES:Bag + 0 + .K + ExecutionPhase + ... .Map => ?_:Map ... + .Set + I0:Int => ?_:Int + ... (ctree(TP1)(T1:CTree) => + + + ?P + + + class String2Id(".rbt") + + + + class String2Id(".rbt") + + + String2Id("value") |-> ?I2:Int :: int + String2Id("color") |-> ?C2:Int :: int + String2Id("left") |-> ?L2:RawRefVal :: class String2Id(".rbt") + String2Id("right") |-> ?R2:RawRefVal :: class String2Id(".rbt") + + + noValue + + + + + class String2Id("java.lang.Object") + + + .Map + + + noValue + + + + ctree(?L2)(?TL2:CTree) + ctree(?R2)(?TR2:CTree) + ) (.Bag => ?_:Bag) +... +requires rbt(T1) andBool V >=Int -2147483648 andBool V <=Int 2147483647 +ensures rbt(?TL2) andBool rbt(?TR2) + andBool ctree_keys(?TL2) + + + (class String2Id(".rbt")).String2Id("insert"):Id(V:Int::int, (TP:RawRefVal)::(class String2Id(".rbt"))) + + => + ?TP1:RawRefVal::(class String2Id(".rbt")) + ... + .Map +... + + + + CLASSES:Bag + 0 + .K + ExecutionPhase + ... .Map => ?_:Map ... + .Set + I:Int => ?_:Int + + ... ctree(TP)(T:CTree) => ctree(?TP1)(?T1:CTree) ... +requires rbt(T) andBool V >=Int -2147483648 andBool V <=Int 2147483647 andBool ctree_height(T) >=Int -2147483648 andBool ctree_height(T) <=Int 2147483646 +ensures rbt(?T1) andBool ctree_keys(?T1) ==K ctree_keys(T) U {V} + andBool ctree_height(T) <=Int ctree_height(?T1) + andBool ctree_height(?T1) <=Int ctree_height(T) +Int 1 + andBool ctree_height(?T1) >=Int -2147483648 andBool ctree_height(?T1) <=Int 2147483647 +endmodule + diff --git a/src/verification/rbt.java b/src/verification/rbt.java new file mode 100644 index 00000000..b8eb0fe4 --- /dev/null +++ b/src/verification/rbt.java @@ -0,0 +1,292 @@ +public class rbt { + int value; + int color;// RED=0, BLACK=1 + rbt left; + rbt right; + + rbt (int value) + { + this.value = value; + this.color = 0; + this.left = null; + this.right = null; + } + + public static void main(String[] args) { + rbt node1 = new rbt (2); + rbt node2 = new rbt (1); + rbt node3 = new rbt (3); + node1.left = node2; + node1.right = node3; + printTree(node1); + System.out.println("\n"); + printTree(insert(6, node1)); + System.out.println("\n"); + printTree(remove(3, node1)); + System.out.println("\n"); + ref ctx = new ref(); + ctx.fixed = 0; + printTree(remove_aux(ctx, 1, node1)); + + } + + static void printTree(rbt nr) { + if (nr != null) + { + System.out.print(nr.value +","); + printTree(nr.left); + printTree(nr.right); + } + } + + static int color(rbt t) + { + return t != null ? t.color : 1; // BLACK + } + + static int find_min(rbt t) + { + if (t.left == null) + return t.value; + else + return find_min(t.left); + } + + static rbt left_rotate(rbt x) + { + rbt y = x.right; + x.right = y.left; + y.left = x; + return y; + } + + static rbt right_rotate(rbt x) + { + rbt y = x.left; + x.left = y.right; + y.right = x; + return y; + } + +// Find + + static boolean find(int v, rbt t) + { + if (t == null) + return false; + else if (v == t.value) + return true; + else if (v < t.value) + return find(v, t.left); + else + return find(v, t.right); + } + + +// Insert + + static rbt insert_aux(int value, rbt tree) + { + if (tree == null) { + return new rbt(value); + } + if (value < tree.value) { + tree.left = insert_aux(value, tree.left); + if (color(tree.left) != 1 /* RED */) { + if (color(tree.right) != 1 /* RED */) { // case 3 + if (color(tree.left.left) != 1 /* RED */ || color(tree.left.right) != 1 /* RED */) { + tree.left.color = 1 /* BLACK */; + tree.right.color = 1 /* BLACK */; + tree.color = 0 /* RED */; + } + } + else { + if (color(tree.left.right) != 1 /* RED */) { // case 4 + tree.left = left_rotate(tree.left); + } + if (color(tree.left.left) != 1 /* RED */) { // case 5; case 4 falls through + tree = right_rotate(tree); + tree.color = 1 /* BLACK */; + tree.right.color = 0 /* RED */; + } + } + } + } + else if (value > tree.value) { + tree.right = insert_aux(value, tree.right); + if (color(tree.right) != 1 /* RED */) { + if (color(tree.left) != 1 /* RED */) { + if (color(tree.right.right) != 1 /* RED */ || color(tree.right.left) != 1 /* RED */) { // case 3 + tree.right.color = 1 /* BLACK */; + tree.left.color = 1 /* BLACK */; + tree.color = 0 /* RED */; + } + } + else { + if (color(tree.right.left) != 1 /* RED */) { // case 4 + tree.right = right_rotate(tree.right); + } + if (color(tree.right.right) != 1 /* RED */) { // case 5; case 4 falls through + tree = left_rotate(tree); + tree.color = 1 /* BLACK */; + tree.left.color = 0 /* RED */; + } + } + } + } + return tree; + } + + static rbt insert(int value, rbt tree) + { + tree = insert_aux(value, tree); + if (color(tree) != 1 /* RED */) { + tree.color = 1 /* BLACK */; + } + return tree; + } + + +// Remove + + static rbt left_remove_fixup(ref ctx, rbt tree) + { + if (color(tree.right) != 1 /* RED */) { // case 2 + tree = left_rotate(tree); + tree.color = 1 /* BLACK */; + tree.left.color = 0 /* RED */; + tree.left = left_remove_fixup(ctx, tree.left); + ctx.fixed = 1; + } + else { + if (color(tree.right.left) == 1 /* BLACK */ && + color(tree.right.right) == 1 /* BLACK */) { // case 3 & 4 + if (color(tree) == 1 /* BLACK */) { // case 3 + ctx.fixed = 0; // {left,right}_remove_fixup will be called again later + } else { // case 4 + ctx.fixed = 1; + } + tree.right.color = 0 /* RED */; + tree.color = 1 /* BLACK */; + } + else { + if (color(tree.right.right) == 1 /* BLACK */) { // case 5 + tree.right = right_rotate(tree.right); + tree.right.color = 1 /* BLACK */; + tree.right.right.color = 0 /* RED */; + } + // case 6; case 5 falls through + tree = left_rotate(tree); + tree.color = color(tree.left); + tree.left.color = 1 /* BLACK */; + tree.right.color = 1 /* BLACK */; + ctx.fixed = 1; + } + } + return tree; + } + + static rbt right_remove_fixup(ref ctx, rbt tree) + { + if (color(tree.left) != 1 /* RED */) { + tree = right_rotate(tree); + tree.color = 1 /* BLACK */; + tree.right.color = 0 /* RED */; + tree.right = right_remove_fixup(ctx, tree.right); + ctx.fixed = 1; + } + else { + if (color(tree.left.right) == 1 /* BLACK */ && + color(tree.left.left) == 1 /* BLACK */) { + if (color(tree) == 1 /* BLACK */) { // case 3 + ctx.fixed = 0; // {left,right}_remove_fixup will be called again later + } else { // case 4 + ctx.fixed = 1; + } + tree.left.color = 0 /* RED */; + tree.color = 1 /* BLACK */; + } + else { + if (color(tree.left.left) == 1 /* BLACK */) { + tree.left = left_rotate(tree.left); + tree.left.color = 1 /* BLACK */; + tree.left.left.color = 0 /* RED */; + } + tree = right_rotate(tree); + tree.color = color(tree.right); + tree.right.color = 1 /* BLACK */; + tree.left.color = 1 /* BLACK */; + ctx.fixed = 1; + } + } + return tree; + } + + static rbt remove_aux(ref ctx, int value, rbt tree) + { + if (tree == null) { + ctx.fixed = 1; + return null; + } + if (value == tree.value) { + if (tree.left == null) { + if (color(tree.right) != 1 /* RED */) { + tree.right.color = 1 /* BLACK */; + ctx.fixed = 1; + } + else { + if (color(tree) == 1 /* BLACK */) { + ctx.fixed = 0; // {left,right}_remove_fixup will be called again later + } else { // case 4 + ctx.fixed = 1; + } + } + return tree.right; + } + else if (tree.right == null) { + if (color(tree.left) != 1 /* RED */) { + tree.left.color = 1 /* BLACK */; + ctx.fixed = 1; + } + else { + if (color(tree) == 1 /* BLACK */) { + ctx.fixed = 0; // {left,right}_remove_fixup will be called again later + } else { // case 4 + ctx.fixed = 1; + } + } + return tree.left; + } + else { + tree.value = find_min(tree.right); + tree.right = remove_aux(ctx, tree.value, tree.right); + if (ctx.fixed != 1) { + tree = right_remove_fixup(ctx, tree); + } + } + } + else if (value < tree.value) { + tree.left = remove_aux(ctx, value, tree.left); + if (ctx.fixed != 1) { + tree = left_remove_fixup(ctx, tree); + } + } + else { + tree.right = remove_aux(ctx, value, tree.right); + if (ctx.fixed != 1) { + tree = right_remove_fixup(ctx, tree); + } + } + return tree; + } + + static rbt remove(int value, rbt tree) + { + ref ctx = new ref(); + ctx.fixed = 0; + tree = remove_aux(ctx, value, tree); + return tree; + } +} + +class ref {int fixed;} diff --git a/src/verification/rbt_pattern.k b/src/verification/rbt_pattern.k new file mode 100644 index 00000000..745aa67b --- /dev/null +++ b/src/verification/rbt_pattern.k @@ -0,0 +1,87 @@ +// Copyright (c) 2014-2015 K Team. All Rights Reserved. + +module RBT-PATTERN + imports MAP + imports JAVA-EXEC + imports INT-SET + + syntax CTree ::= "cnode" "(" Int ", "Int", " CTree "," CTree ")"// Red=0, Black=1 + | "cleaf" + + syntax IntSet ::= "ctree_keys" "(" CTree ")" [function, smtlib(smt_ctree_keys)] + rule ctree_keys(cnode(I:Int, _, TL:CTree, TR:CTree)) + => { I } U (ctree_keys(TL) U ctree_keys(TR)) + rule ctree_keys(cleaf) => .IntSet + syntax Int ::= "ctree_height" "(" CTree ")" [function, smtlib(smt_ctree_height)] + + rule ctree_height(cnode(_, C:Int, TL:CTree, TR:CTree)) => C +Int maxInt(ctree_height(TL), ctree_height(TR)) + rule ctree_height(cleaf) => 0 + + rule ctree_height(T:CTree) >=Int 0 => true [smt-lemma] + + syntax Int ::= "ctree_color" "(" CTree ")" [function, smtlib(smt_ctree_color)] + rule ctree_color(cnode(_, C:Int, _, _)) => C + rule ctree_color(cleaf) => 1 + + rule ( ctree_color(T:CTree) ==K 1 orBool ctree_color(T) ==K 0 ) => true [smt-lemma] + + syntax Bool ::= "rbt" "(" CTree ")" [function, smtlib(smt_rbt)] + rule rbt(cnode(I:Int, C:Int, TL:CTree, TR:CTree)) + => rbt(TL) andBool rbt(TR) + andBool ctree_keys(TL) true + + syntax Bag ::= "ctree" "(" RawRefVal ")" "(" CTree ")" [pattern(1)] + rule ... + ctree(objectRef(P:Int, C:ClassType))(cnode(I:Int, Cl:Int, TL:CTree, TR:CTree)) + => + + P + + + C + + + + C + + + String2Id("value") |-> I :: int + String2Id("color") |-> Cl :: int + String2Id("left") |-> ?PL:RawRefVal :: C + String2Id("right") |-> ?PR:RawRefVal :: C + + + noValue + + + + + class String2Id("java.lang.Object") + + + .Map + + + noValue + + + + ctree(?PL)(TL) + ctree(?PR)(TR) + ... + + ensures I >=Int -2147483648 andBool I <=Int 2147483647 andBool + ctree_color(cnode(I, Cl, TL, TR)) >=Int -2147483648 andBool ctree_color(cnode(I, Cl, TL, TR)) <=Int 2147483647 + [pattern] + rule ... ctree(null)(cleaf) => .Bag ... [pattern] + + +endmodule