diff options
| author |  stefanheule <unknown> | 2012-02-25 03:50:05 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:50:05 -0800 |
| commit | f5094e7df835e2ea59d93041dfeffcc1f37348a2 (patch) | |
| tree | 22a8df6f5be70f204b0dc82b1d3efd47616aa4a3 /Chalice/tests/examples | |
| parent | ab61f647466f3cdc049041aa7d8f18968756a099 (diff) | |
| parent | af8a60c01d6be1a9dca3b0f111b796ebf1450bb0 (diff) | |
Semi-automatic merge.
Diffstat (limited to 'Chalice/tests/examples')
| -rw-r--r-- | Chalice/tests/examples/AVLTree.iterative.chalice | 227 | ||||
| -rw-r--r-- | Chalice/tests/examples/AVLTree.iterative.output.txt | 4 | ||||
| -rw-r--r-- | Chalice/tests/examples/AVLTree.nokeys.chalice | 609 | ||||
| -rw-r--r-- | Chalice/tests/examples/AVLTree.nokeys.output.txt | 4 |
4 files changed, 844 insertions, 0 deletions
diff --git a/Chalice/tests/examples/AVLTree.iterative.chalice b/Chalice/tests/examples/AVLTree.iterative.chalice new file mode 100644 index 00000000..4156a73f --- /dev/null +++ b/Chalice/tests/examples/AVLTree.iterative.chalice @@ -0,0 +1,227 @@ +class AVLTree{
+ var root : AVLTreeNode;
+
+ predicate valid{
+ acc(root,100)
+ && (root!=null ==> root.valid)
+ && (root!=null ==> acc(root.parent,100))
+ && (root!=null ==> root.parent==null)
+ && (root!=null ==> acc(root.root,50))
+ && (root!=null ==> root.root==root)
+ }
+
+ method init()
+ requires acc(root,100);
+ ensures valid;
+ {
+ root := null;
+ fold valid;
+ }
+
+ method has(k : int) returns (b : bool)
+ requires valid;
+ ensures valid;
+ {
+ unfold valid;
+ if (root==null){
+ b := false;
+ fold valid;
+ }else{
+ var n : AVLTreeNode := root;
+ b := false;
+ var end : bool := false;
+ fold n.udParentValid;
+ while (!end)
+ invariant acc(root,100);
+ invariant root != null && acc(root.parent,50);
+ invariant n!=null;
+ invariant n.valid;
+ invariant acc(n.root,40);
+ invariant n.udParentValid;
+ invariant unfolding n.valid in n.root==root;
+ invariant root!=null;
+ {
+ unfold n.valid;
+ unfold n.validRest;
+ if (n.key==k){
+ b := true;
+ fold n.validRest;
+ fold n.valid;
+ end := true;
+ }else{
+ if (n.key<k){
+ if (n.left==null){
+ end := true;
+ fold n.validRest;
+ fold n.valid;
+ }else{
+ var p : AVLTreeNode := n;
+ unfold p.leftValid;
+ n := p.left;
+ p.leftDown := true;
+ fold p.leftOpen;
+ fold p.udValid;
+ assert p.right!=p.left;
+ assert n.parent.left==n;
+ fold n.udParentValid;
+ }
+ }else{
+ if (n.right==null){
+ end := true;
+ fold n.validRest;
+ fold n.valid;
+ }else{
+ var p : AVLTreeNode := n;
+ unfold p.rightValid;
+ n := p.right;
+ p.leftDown := false;
+ fold p.rightOpen;
+ fold p.udValid;
+ fold n.udParentValid;
+ }
+ }
+ }
+ }
+
+ end := false;
+ while (!end)
+ invariant acc(root,100);
+ invariant root != null && acc(root.parent,50);
+ invariant n!=null;
+ invariant n.valid;
+ invariant n.udParentValid;
+ invariant acc(n.root,40);
+ invariant unfolding n.valid in n.root==root;
+ invariant root!=null;
+ invariant end==>unfolding n.udParentValid in n.parent==null;
+ {
+ unfold n.udParentValid;
+ var p : AVLTreeNode := n.parent;
+ if (p==null){
+ end := true;
+ fold n.udParentValid;
+ }else{
+ unfold p.udValid;
+ if (p.left==n){
+ unfold p.leftOpen;
+ fold p.leftValid;
+ }else{
+ unfold p.rightOpen;
+ fold p.rightValid;
+ }
+ fold p.validRest;
+ fold p.valid;
+ n:=p;
+ }
+ }
+ assert unfolding n.udParentValid in n==root;
+ assert acc(n.root,40);
+ unfold n.udParentValid;
+ assert acc(n.root,50);
+ fold valid;
+ }
+ }
+}
+
+class AVLTreeNode{
+ var key : int;
+ var left : AVLTreeNode;
+ var right : AVLTreeNode;
+ var parent : AVLTreeNode;
+
+ ghost var leftDown : bool;
+ ghost var root : AVLTreeNode;
+
+ predicate valid{
+ validRest
+ && leftValid
+ && rightValid
+ }
+
+ predicate validRest{
+ acc(key ,100)
+ && acc(root, 30)
+ && acc(left ,75)
+ && acc(right ,75)
+ && acc(leftDown,100)
+ && (right!=left || right==null)
+ }
+
+ predicate rightValid{
+ acc(right ,25)
+ && acc(root,10)
+ && (right!=null ==> right.valid)
+ && (right!=null ==> acc(right.parent,100))
+ && (right!=null ==> right.parent==this)
+ && (right!=null ==> acc(right.root,50))
+ && (right!=null ==> right.root==root)
+ }
+ predicate leftValid{
+ acc(left ,25)
+ && acc(root,10)
+ && (left!=null ==> left.valid)
+ && (left!=null ==> acc(left.parent,100))
+ && (left!=null ==> left.parent == this)
+ && (left!=null ==> acc(left.root,50))
+ && (left!=null ==> left.root == root)
+ }
+
+ predicate leftOpen{
+ acc(left ,25)
+ && acc(root,10)
+ && (left!=null ==> acc(left.parent,50))
+ && (left!=null ==> left.parent==this)
+ }
+
+ predicate rightOpen{
+ acc(right ,25)
+ && acc(root,10)
+ && (right!=null ==> acc(right.parent,50))
+ && (right!=null ==> right.parent==this)
+ }
+
+ predicate udParentValid {
+ acc(parent,50)
+ && acc(root,10)
+ && (parent!=null ==> parent.udValid)
+ && (parent!=null ==> acc(parent.leftDown,50))
+ && (parent!=null ==> acc(parent.left,50))
+ && (parent!=null ==> ( parent.leftDown<==>parent.left==this))
+ && (parent!=null ==> acc(parent.right,50))
+ && (parent!=null ==> (!parent.leftDown<==>parent.right==this))
+ && (parent!=null ==> acc(parent.root,50))
+ && (parent!=null ==> root==parent.root)
+ && (parent==null ==> root==this)
+ }
+
+ predicate udValid{
+ acc(key ,100)
+ && acc(leftDown,50)
+ && acc(left ,25)
+ && acc(right ,25)
+ && acc(root ,20)
+ && ( leftDown ==> rightValid)
+ && ( leftDown ==> leftOpen )
+ && (!leftDown ==> leftValid )
+ && (!leftDown ==> rightOpen )
+ && udParentValid
+ }
+
+ method init(k : int)
+ requires acc(key ,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(leftDown ,100);
+ requires acc(root, 100);
+ ensures valid;
+ {
+ left := null;
+ right := null;
+ key := k;
+
+ fold leftValid;
+ fold rightValid;
+ fold validRest;
+ fold valid;
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/AVLTree.iterative.output.txt b/Chalice/tests/examples/AVLTree.iterative.output.txt new file mode 100644 index 00000000..152260e3 --- /dev/null +++ b/Chalice/tests/examples/AVLTree.iterative.output.txt @@ -0,0 +1,4 @@ +Verification of AVLTree.iterative.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/AVLTree.nokeys.chalice b/Chalice/tests/examples/AVLTree.nokeys.chalice new file mode 100644 index 00000000..721541f2 --- /dev/null +++ b/Chalice/tests/examples/AVLTree.nokeys.chalice @@ -0,0 +1,609 @@ +class AVLTree{
+ var root : AVLTreeNode;
+
+ predicate valid{
+ acc(root,100)
+ && (root!=null ==> root.valid)
+ && (root!=null ==> acc(root.height ,50))
+ && (root!=null ==> acc(root.balanceFactor,50))
+ }
+
+ method init()
+ requires acc(root,100);
+ ensures valid;
+ {
+ root := null;
+ fold valid;
+ }
+
+ method insert(k : int)
+ requires valid;
+ ensures valid;
+ {
+ unfold valid;
+ if (root==null){
+ var n : AVLTreeNode := new AVLTreeNode;
+ call n.init(k);
+ root := n;
+ }else{
+ call r := root.insert(k);
+ root := r;
+ }
+ fold valid;
+ }
+
+ method remove(k : int)
+ requires valid;
+ ensures valid;
+ {
+ unfold valid;
+ if (root==null){
+ }else{
+ call r := root.remove(k);
+ root := r;
+ }
+ fold valid;
+ }
+
+ method has(k : int) returns (b : bool)
+ requires valid;
+ ensures valid;
+ {
+ unfold valid;
+ if (root==null){
+ b := false;
+ }else{
+ var bb : bool;
+ call bb:= root.has(k);
+ b := bb;
+ }
+ fold valid;
+ }
+}
+
+class AVLTreeNode{
+ var key : int;
+ var height : int;
+ var left : AVLTreeNode;
+ var right : AVLTreeNode;
+ ghost var balanceFactor : int;
+
+ predicate valid{
+ acc(key ,100)
+ && acc(height,50)
+ && acc(left ,100)
+ && acc(right ,100)
+ && acc(balanceFactor,50)
+ && (left!=null ==> left.valid)
+ && (left!=null ==> acc(left.height ,50))
+ && (left!=null ==> acc(left.balanceFactor,50))
+ && (left!=null ==> left.height > 0)
+ && (right!=null ==> right.valid)
+ && (right!=null ==> acc(right.height ,50))
+ && (right!=null ==> acc(right.balanceFactor,50))
+ && (right!=null ==> right.height > 0)
+ && height == ( (left==null?0:left.height)>(right==null?0:right.height) ? (left==null?0:left.height)+1 : (right==null?0:right.height)+1 )
+ && balanceFactor == (left==null?0:left.height) - (right==null?0:right.height)
+ && balanceFactor<= 1
+ && balanceFactor>=-1
+ && height > 0
+ }
+
+ method init(k : int)
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100)
+ ensures valid;
+ ensures acc(height,50);
+ ensures acc(balanceFactor,50);
+ ensures height == 1;
+ ensures balanceFactor == 0;
+ {
+ left := null;
+ right := null;
+ key := k;
+ call close();
+ }
+
+ method insert(k : int) returns ( r : AVLTreeNode )
+ requires valid;
+ requires acc(height,50);
+ requires acc(balanceFactor,50);
+ ensures r != null;
+ ensures r.valid;
+ ensures acc(r.height,50);
+ ensures acc(r.balanceFactor,50);
+ ensures ( r.height == old(height) ) || ( r.height == old(height) + 1 );
+ {
+ unfold valid;
+ if (key==k){
+ r := this;
+ call r.close();
+ }else{ //key!=k
+ if (k<key){ // insert left
+ var nl : AVLTreeNode;
+ if (left==null){
+ nl := new AVLTreeNode;
+ call nl.init(k);
+ }else{
+ call nl := left.insert(k);
+ }
+ left := nl;
+ var bf : int;
+ call bf := getBalanceFactorI();
+
+ if (bf==2){ //rebalance
+ call r:= rebalanceLeft();
+ }else{ //no rebalance
+ r := this;
+ call r.close();
+ }
+ }else{ // k>key -- insert right
+ var nr : AVLTreeNode;
+ if (right==null){
+ nr := new AVLTreeNode;
+ call nr.init(k);
+ }else{
+ call nr := right.insert(k);
+ }
+ right := nr;
+
+ var bf : int;
+ call bf := getBalanceFactorI();
+ if (bf==-2){ //rebalance
+ call r := rebalanceRight();
+ }else{//no rebalance
+ r := this;
+ call r.close();
+ }
+ }
+ }
+ }
+
+ method remove(k : int) returns ( r : AVLTreeNode )
+ requires valid;
+ requires acc(height,50);
+ requires acc(balanceFactor,50);
+ ensures r != null ==> r.valid;
+ ensures r != null ==> acc(r.height,50);
+ ensures r != null ==> acc(r.balanceFactor,50);
+ ensures old(height)>1 ==> r!=null;
+ ensures r != null ==> r.height==old(height) || r.height+1==old(height);
+ {
+ unfold valid;
+ if (key==k){
+ if (left==null || right==null){
+ if (left==null){ // replace with right
+ r := right;
+ }else{ // right==null
+ r := left;
+ }
+ }else{ // prune max/min of left/right
+ var bf : int;
+ var nl : AVLTreeNode := left;
+ var nr : AVLTreeNode := right;
+
+ call bf := getBalanceFactorI();
+ if (bf > 0 ){ // left larger - prune leftmax
+ call nl,r := left.pruneMax();
+ }else{ // right larger equal - prune rightmin
+ call nr,r := right.pruneMin();
+ }
+ unfold r.valid;
+ r.left := nl;
+ r.right := nr;
+ call r.close();
+ }
+ }else{ //key!=k
+ if (k<key){ // remove left
+ if (left!=null){
+ var nl : AVLTreeNode;
+ call nl := left.remove(k);
+ left := nl;
+
+ var bf : int;
+ call bf := getBalanceFactorI();
+
+ if (bf==-2){ // rebalance
+ call r:=rebalanceRight();
+ }else{ // no rebalance
+ call close();
+ r := this;
+ }
+ }else{
+ r := this;
+ call r.close();
+ }
+ }else{ // k>key -- remove right
+ if (right != null){
+ var nr : AVLTreeNode;
+ call nr := right.remove(k);
+ right := nr;
+
+ var bf : int;
+ call bf := getBalanceFactorI();
+ if (bf==2){ // rebalance
+ call r := rebalanceLeft();
+ }else{ // no rebalance
+ r := this;
+ call r.close();
+ }
+ }else{
+ r := this;
+ call r.close();
+ }
+ }
+ }
+ }
+
+ method pruneMax() returns ( r : AVLTreeNode, m : AVLTreeNode )
+ requires valid;
+ requires acc(height,50);
+ requires acc(balanceFactor,50);
+ ensures r != null ==> r.valid;
+ ensures r != null ==> acc(r.height,50);
+ ensures r != null ==> acc(r.balanceFactor,50);
+ ensures r != null ==> (r.height == old(height) || r.height+1 == old(height));
+ ensures old(height) >1 ==> r != null;
+ ensures old(height)==1 ==> r == null;
+ ensures old(height)==(r==null?0:r.height) || old(height)==(r==null?0:r.height)+1;
+ ensures m != null;
+ ensures m.valid;
+ ensures acc(m.height,50);
+ ensures acc(m.balanceFactor,50);
+ ensures m.height == 1;
+ {
+ unfold valid;
+ if (right==null){
+ r := left;
+ left := null;
+ call close();
+ m := this;
+ }else{
+ var nr : AVLTreeNode;
+ call nr,m := right.pruneMax();
+ right := nr;
+ var bf : int;
+ call bf := getBalanceFactorI();
+ if (bf == 2){
+ call r:=rebalanceLeft();
+ }else{
+ call close();
+ r := this;
+ }
+ }
+ }
+
+ method pruneMin() returns ( r : AVLTreeNode, m : AVLTreeNode )
+ requires valid;
+ requires acc(height,50);
+ requires acc(balanceFactor,50);
+ ensures r != null ==> r.valid;
+ ensures r != null ==> acc(r.height,50);
+ ensures r != null ==> acc(r.balanceFactor,50);
+ ensures r != null ==> (r.height == old(height) || r.height == old(height)-1);
+ ensures old(height) >1 ==> r != null;
+ ensures old(height)==1 ==> r == null;
+ ensures old(height)==(r==null?0:r.height) || old(height)==(r==null?0:r.height)+1;
+ ensures m != null;
+ ensures m.valid;
+ ensures acc(m.height,50);
+ ensures acc(m.balanceFactor,50);
+ ensures m.height == 1;
+ {
+ unfold valid;
+ if (left==null){
+ r := right;
+ right := null;
+ call close();
+ m := this;
+ assert r!=null ==> (r.height == old(height) || r.height == old(height)-1);
+ }else{
+ var nl : AVLTreeNode;
+ call nl,m := left.pruneMin();
+ left := nl;
+ var bf : int;
+ call bf := getBalanceFactorI();
+ if (bf == -2){
+ call r:=rebalanceRight();
+ assert r != null ==> (r.height == old(height) || r.height == old(height)-1);
+ }else{
+ call close();
+ r := this;
+ assert r != null ==> (r.height == old(height) || r.height == old(height)-1);
+ }
+ }
+ }
+
+ method has(k : int) returns (b : bool)
+ requires valid;
+ ensures valid;
+ {
+ unfold valid;
+ if (k==key){
+ b := true;
+ }else{ //k!=key
+ if (k < key){
+ if (left!=null){
+ call b := left.has(k);
+ }else{
+ b := false;
+ }
+ }else{ //k > key;
+ if (right!=null){
+ call b := right.has(k);
+ }else{
+ b := false;
+ }
+ }
+ }
+ fold valid;
+ }
+
+ method getBalanceFactor() returns ( bf : int )
+ requires valid;
+ requires rd(balanceFactor);
+
+ ensures valid;
+ ensures rd(balanceFactor);
+ ensures bf == balanceFactor;
+
+ ensures unfolding valid in bf>0 ==> left !=null;
+ ensures unfolding valid in bf<0 ==> right!=null;
+ {
+ unfold valid;
+ var lh : int := (left ==null ? 0 : left .height );
+ var rh : int := (right==null ? 0 : right.height );
+ bf := lh-rh;
+
+ fold valid;
+ }
+
+ //////////////////////////////////////////////////////////
+ method getBalanceFactorI() returns ( bf : int )
+ requires rd(left);
+ requires left!=null ==> left.valid;
+ requires left!=null ==> rd(left.height);
+ requires rd(right);
+ requires right!=null ==> right.valid;
+ requires right!=null ==> rd(right.height);
+ ensures rd(left);
+ ensures left!=null ==> left.valid;
+ ensures left!=null ==> rd(left.height);
+ ensures rd(right);
+ ensures right!=null ==> right.valid;
+ ensures right!=null ==> rd(right.height);
+ ensures bf == (left==null?0:left.height)-(right==null?0:right.height);
+ ensures bf>0 ==> left !=null;
+ ensures bf<0 ==> right!=null;
+ {
+ var lh : int := (left ==null ? 0 : left .height );
+ var rh : int := (right==null ? 0 : right.height );
+ bf := lh-rh;
+ assert right!=null ==> unfolding right.valid in right.height>0;
+ assert left !=null ==> unfolding left .valid in left .height>0;
+ assert lh>=0;
+ assert rh>=0;
+ }
+
+ method close()
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100);
+ requires left!=null ==> left.valid;
+ requires left!=null ==> acc(left.height ,50);
+ requires left!=null ==> acc(left.balanceFactor,50);
+ requires right!=null ==> right.valid;
+ requires right!=null ==> acc(right.height ,50);
+ requires right!=null ==> acc(right.balanceFactor,50);
+ requires ( left==null ? 0 : left.height )-( right==null ? 0 : right.height ) <= 1;
+ requires ( left==null ? 0 : left.height )-( right==null ? 0 : right.height ) >=-1;
+ ensures valid;
+ ensures acc(height ,50);
+ ensures acc(balanceFactor,50);
+ ensures height ==
+ ( ( old(left)==null ? 0 : old(left.height) )>( old(right)==null ? 0 : old(right.height) )
+ ?
+ ( old(left)==null ? 0 : old(left.height) )+1
+ :
+ ( old(right)==null ? 0 : old(right.height))+1
+ );
+ ensures balanceFactor ==
+ ( old(left)==null ? 0 : old(left.height) )-( old(right)==null ? 0 : old(right.height) );
+ {
+ var lh : int := (left ==null ? 0 : left .height );
+ var rh : int := (right==null ? 0 : right.height );
+
+ assert left !=null ==> unfolding left .valid in left .height>0;
+ assert right!=null ==> unfolding right.valid in right.height>0;
+ height := ( (( left==null ? 0 : left.height )>( right==null ? 0 : right.height )) ? ( left==null ? 0 : left.height )+1 : ( right==null ? 0 : right.height )+1);
+
+ balanceFactor := ( left==null ? 0 : left.height )-( right==null ? 0 : right.height );
+
+ fold valid;
+ }
+
+ method rebalanceLeft() returns ( r : AVLTreeNode )
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100);
+ requires left!=null;
+ requires left.valid;
+ requires acc(left.height ,50);
+ requires acc(left.balanceFactor,50);
+ requires right!=null ==> right.valid;
+ requires right!=null ==> acc(right.height ,50)
+ requires right!=null ==> acc(right.balanceFactor,50)
+ requires left.height-(right==null?0:right.height)==2;
+ ensures r != null && r.valid;
+ ensures acc(r.height ,50);
+ ensures acc(r.balanceFactor,50);
+ ensures r.height == old(left.height) || r.height == old(left.height)+1;
+ {
+ var lbf : int;
+ call lbf := left.getBalanceFactor();
+ if (lbf<0){
+ assert unfolding left.valid in lbf==-1;
+ call r := rebalanceRL();
+ }else{//lbf>=0
+ call r := rebalanceRR();
+ }
+ }
+
+ method rebalanceRL() returns ( r : AVLTreeNode )
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100);
+ requires left!=null;
+ requires left.valid;
+ requires acc(left.height ,50);
+ requires acc(left.balanceFactor,50);
+ requires right!=null ==> right.valid;
+ requires right!=null ==> acc(right.height ,50)
+ requires right!=null ==> acc(right.balanceFactor,50)
+ requires left.height-(right==null?0:right.height)==2;
+ requires left.balanceFactor==-1;
+ ensures r != null && r.valid;
+ ensures acc(r.height ,50);
+ ensures acc(r.balanceFactor,50);
+ ensures r.height == old(left.height);
+ {
+ unfold left.valid;
+ r := left.right;
+ unfold r.valid;
+
+ left.right := r.left;
+ call left.close();
+ r.left := left;
+ left := r.right;
+
+ call close();
+ r.right := this;
+ call r.close();
+ }
+
+ method rebalanceRR() returns ( r : AVLTreeNode )
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100);
+ requires left!=null;
+ requires left.valid;
+ requires acc(left.height ,50);
+ requires acc(left.balanceFactor,50);
+ requires right!=null ==> right.valid;
+ requires right!=null ==> acc(right.height ,50)
+ requires right!=null ==> acc(right.balanceFactor,50)
+ requires left.height - (right==null?0:right.height)==2;
+ requires left.balanceFactor>=0;
+ ensures r != null && r.valid;
+ ensures acc(r.height ,50);
+ ensures acc(r.balanceFactor,50);
+ ensures r.height == old(left.height) || r.height == old(left.height)+1;
+ {
+ unfold left.valid;
+ r := left;
+ left := r.right;
+ call close();
+ r.right := this;
+ call r.close();
+ }
+
+ method rebalanceRight() returns ( r : AVLTreeNode )
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100);
+ requires left!=null==>left.valid;
+ requires left!=null==>acc(left.height ,50);
+ requires left!=null==>acc(left.balanceFactor,50);
+ requires right!=null;
+ requires right.valid;
+ requires acc(right.height ,50)
+ requires acc(right.balanceFactor,50)
+ requires (left==null?0:left.height)-right.height==-2;
+ ensures r != null && r.valid;
+ ensures acc(r.height ,50);
+ ensures acc(r.balanceFactor,50);
+ ensures r.height == old(right.height) || r.height == old(right.height)+1;
+ {
+ var rbf : int;
+ call rbf := right.getBalanceFactor();
+ if (rbf>0){
+ assert unfolding right.valid in rbf==1;
+ call r := rebalanceLR();
+ }else{//rbf<=0
+ call r := rebalanceLL();
+ }
+ }
+
+ method rebalanceLR() returns ( r : AVLTreeNode )
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100);
+ requires left!=null==>left.valid;
+ requires left!=null==>acc(left.height ,50);
+ requires left!=null==>acc(left.balanceFactor,50);
+ requires right!=null;
+ requires right.valid;
+ requires acc(right.height ,50);
+ requires acc(right.balanceFactor,50);
+ requires (left==null?0:left.height)-right.height==-2;
+ requires right.balanceFactor==1;
+ ensures r != null && r.valid;
+ ensures acc(r.height ,50);
+ ensures acc(r.balanceFactor,50);
+ ensures r.height == old(right.height);
+ {
+ unfold right.valid;
+ r := right.left;
+ unfold r.valid;
+ right.left := r.right;
+ call right.close();
+ r.right := right;
+ right := r.left;
+ call close();
+ r.left := this;
+ call r.close();
+ }
+
+ method rebalanceLL() returns ( r : AVLTreeNode )
+ requires acc(key ,100);
+ requires acc(height,100);
+ requires acc(left ,100);
+ requires acc(right ,100);
+ requires acc(balanceFactor,100);
+ requires left!=null==>left.valid;
+ requires left!=null==>acc(left.height ,50);
+ requires left!=null==>acc(left.balanceFactor,50);
+ requires right!=null;
+ requires right.valid;
+ requires acc(right.height ,50);
+ requires acc(right.balanceFactor,50);
+ requires (left==null?0:left.height)-right.height==-2;
+ requires right.balanceFactor<=0;
+ ensures r != null && r.valid;
+ ensures acc(r.height ,50);
+ ensures acc(r.balanceFactor,50);
+ ensures r.height == old(right.height) || r.height == old(right.height)+1;
+ {
+ unfold right.valid;
+ r := right;
+ right := r.left;
+ call close();
+ r.left := this;
+ call r.close();
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/examples/AVLTree.nokeys.output.txt b/Chalice/tests/examples/AVLTree.nokeys.output.txt new file mode 100644 index 00000000..c9dc557a --- /dev/null +++ b/Chalice/tests/examples/AVLTree.nokeys.output.txt @@ -0,0 +1,4 @@ +Verification of AVLTree.nokeys.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
|