diff options
Diffstat (limited to 'Chalice/tests/examples/AVLTree.iterative.chalice')
| -rw-r--r-- | Chalice/tests/examples/AVLTree.iterative.chalice | 227 |
1 files changed, 0 insertions, 227 deletions
diff --git a/Chalice/tests/examples/AVLTree.iterative.chalice b/Chalice/tests/examples/AVLTree.iterative.chalice deleted file mode 100644 index 4156a73f..00000000 --- a/Chalice/tests/examples/AVLTree.iterative.chalice +++ /dev/null @@ -1,227 +0,0 @@ -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 |