From c7ef53e3d517226f73badb8983e4c6d1e6a3f641 Mon Sep 17 00:00:00 2001 From: yuwen2 Date: Tue, 15 Mar 2016 23:42:50 -0500 Subject: [PATCH 1/7] rbt --- src/verification/rbt.java | 273 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 273 insertions(+) create mode 100644 src/verification/rbt.java diff --git a/src/verification/rbt.java b/src/verification/rbt.java new file mode 100644 index 00000000..cebe47b5 --- /dev/null +++ b/src/verification/rbt.java @@ -0,0 +1,273 @@ +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; + } + + // Basics + + static rbt make_node(int v) + { + rbt node = new rbt (v); + return node; + } + + static int color(rbt t) + { + return t ? 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(x) + { + rbt y = x.right; + x.right = y.left; + y.left = x; + return y; + } + + static rbt right_rotate(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 make_node(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;} From be3a11f535a80aac6080bf58ec0ff7be49d1e0f6 Mon Sep 17 00:00:00 2001 From: yuwen2 Date: Wed, 16 Mar 2016 17:04:51 -0500 Subject: [PATCH 2/7] rbt find --- src/verification/rbt-find-spec.k | 32 ++++++++++++ src/verification/rbt_pattern.k | 87 ++++++++++++++++++++++++++++++++ 2 files changed, 119 insertions(+) create mode 100644 src/verification/rbt-find-spec.k create mode 100644 src/verification/rbt_pattern.k 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_pattern.k b/src/verification/rbt_pattern.k new file mode 100644 index 00000000..d5b69289 --- /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") |-> ctree_color(cnode(I, Cl, TL, TR)) :: 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 From 82ba0befbe2fe092cec1f48cf9ffd2240a5e3422 Mon Sep 17 00:00:00 2001 From: yuwen2 Date: Wed, 16 Mar 2016 17:10:01 -0500 Subject: [PATCH 3/7] add verification script --- src/pureVerify.sh | 31 +++++++++++++++++++++++++++++ src/run12.sh | 50 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+) create mode 100755 src/pureVerify.sh create mode 100644 src/run12.sh diff --git a/src/pureVerify.sh b/src/pureVerify.sh new file mode 100755 index 00000000..ef123e7f --- /dev/null +++ b/src/pureVerify.sh @@ -0,0 +1,31 @@ +#!/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 "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" + From 0076e60771f8493d291edc846eb576d251f006b9 Mon Sep 17 00:00:00 2001 From: yuwen2 Date: Wed, 16 Mar 2016 17:13:53 -0500 Subject: [PATCH 4/7] import pattern to java-verification.k --- src/verification/java-verification.k | 2 ++ src/verification/rbt.java | 26 +++++++++++++------------- 2 files changed, 15 insertions(+), 13 deletions(-) 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.java b/src/verification/rbt.java index cebe47b5..15d09233 100644 --- a/src/verification/rbt.java +++ b/src/verification/rbt.java @@ -11,29 +11,29 @@ public class rbt { this.left = null; this.right = null; } - - // Basics - static rbt make_node(int v) - { - rbt node = new rbt (v); - return node; + public static void main(String[] args) { + rbt node1 = new rbt (0); + rbt node2 = new rbt (0); + rbt node3 = new rbt (0); + node1.left = node2; + node1.right = node3; } static int color(rbt t) { - return t ? t.color : 1; // BLACK + return t != null ? t.color : 1; // BLACK } static int find_min(rbt t) { - if (t.left === null) + if (t.left == null) return t.value; else return find_min(t.left); } - static rbt left_rotate(x) + static rbt left_rotate(rbt x) { rbt y = x.right; x.right = y.left; @@ -41,7 +41,7 @@ static rbt left_rotate(x) return y; } - static rbt right_rotate(x) + static rbt right_rotate(rbt x) { rbt y = x.left; x.left = y.right; @@ -53,9 +53,9 @@ static rbt right_rotate(x) static boolean find(int v, rbt t) { - if (t === null) + if (t == null) return false; - else if (v === t.value) + else if (v == t.value) return true; else if (v < t.value) return find(v, t.left); @@ -69,7 +69,7 @@ else if (v < t.value) static rbt insert_aux(int value, rbt tree) { if (tree == null) { - return make_node(value); + return new rbt(value); } if (value < tree.value) { tree.left = insert_aux(value, tree.left); From 96e62b7e55d7a38e7ebb81b5b06c39066add6887 Mon Sep 17 00:00:00 2001 From: yuwen2 Date: Thu, 17 Mar 2016 21:29:33 -0500 Subject: [PATCH 5/7] rbt-spec --- src/pureVerify.sh | 4 + src/verification/rbt-delete-spec.k | 184 +++++++++++++++++++++++++++++ src/verification/rbt-insert-spec.k | 137 +++++++++++++++++++++ src/verification/rbt.java | 9 +- 4 files changed, 330 insertions(+), 4 deletions(-) create mode 100644 src/verification/rbt-delete-spec.k create mode 100644 src/verification/rbt-insert-spec.k diff --git a/src/pureVerify.sh b/src/pureVerify.sh index ef123e7f..321b93ce 100755 --- a/src/pureVerify.sh +++ b/src/pureVerify.sh @@ -13,6 +13,10 @@ 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" 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-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 index 15d09233..36b2e2cb 100644 --- a/src/verification/rbt.java +++ b/src/verification/rbt.java @@ -13,11 +13,12 @@ public class rbt { } public static void main(String[] args) { - rbt node1 = new rbt (0); - rbt node2 = new rbt (0); - rbt node3 = new rbt (0); + rbt node1 = new rbt (2); + rbt node2 = new rbt (1); + rbt node3 = new rbt (3); node1.left = node2; node1.right = node3; + insert_aux(5, node1); } static int color(rbt t) @@ -165,7 +166,7 @@ static rbt left_remove_fixup(ref ctx, rbt tree) } } return tree; - } + }gi static rbt right_remove_fixup(ref ctx, rbt tree) { From 2459e097ecf28376fa37706d4df40ed161b0cf4e Mon Sep 17 00:00:00 2001 From: yuwen2 Date: Thu, 17 Mar 2016 22:10:06 -0500 Subject: [PATCH 6/7] update pattern --- src/verification/rbt_pattern.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/verification/rbt_pattern.k b/src/verification/rbt_pattern.k index d5b69289..745aa67b 100644 --- a/src/verification/rbt_pattern.k +++ b/src/verification/rbt_pattern.k @@ -54,7 +54,7 @@ module RBT-PATTERN String2Id("value") |-> I :: int - String2Id("color") |-> ctree_color(cnode(I, Cl, TL, TR)) :: int + String2Id("color") |-> Cl :: int String2Id("left") |-> ?PL:RawRefVal :: C String2Id("right") |-> ?PR:RawRefVal :: C From 852f9b08ac5980994a48be33808ac6d5dcfea910 Mon Sep 17 00:00:00 2001 From: yuwen2 Date: Fri, 18 Mar 2016 20:41:11 -0500 Subject: [PATCH 7/7] temporal change to rbt.java in case tests are needed --- src/verification/rbt.java | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/src/verification/rbt.java b/src/verification/rbt.java index 36b2e2cb..b8eb0fe4 100644 --- a/src/verification/rbt.java +++ b/src/verification/rbt.java @@ -18,7 +18,25 @@ public static void main(String[] args) { rbt node3 = new rbt (3); node1.left = node2; node1.right = node3; - insert_aux(5, node1); + 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) @@ -166,7 +184,7 @@ static rbt left_remove_fixup(ref ctx, rbt tree) } } return tree; - }gi + } static rbt right_remove_fixup(ref ctx, rbt tree) {