Mercurial > hg > Papers > 2023 > soto-master

annotate Paper/src/bt_verif/invariant.agda.replaced @ 3:c28e8156a37b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add paper init~agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 20 Jan 2023 13:40:03 +0900
parents a72446879486
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 treeInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! Set
3
c28e8156a37b Add paper init~agda
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
2 treeInvariant leaf = !$\top$!
c28e8156a37b Add paper init~agda
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
3 treeInvariant (node key value leaf leaf) = !$\top$!
c28e8156a37b Add paper init~agda
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
4 treeInvariant (node key value leaf n@(node key!$\text{1}$! value!$\text{1}$! t!$\text{1}$! t!$\text{2}$!)) = (key < key!$\text{1}$!) !$\wedge$! treeInvariant n
1
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 treeInvariant (node key value n@(node key!$\text{1}$! value!$\text{1}$! t t!$\text{1}$!) leaf) = treeInvariant n !$\wedge$! (key < key!$\text{1}$!)
3
c28e8156a37b Add paper init~agda
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
6 treeInvariant (node key value n@(node key!$\text{1}$! value!$\text{1}$! t t!$\text{1}$!) m@(node key!$\text{2}$! value!$\text{2}$! t!$\text{2}$! t!$\text{3}$!)) = treeInvariant n !$\wedge$! (key < key!$\text{1}$!) !$\wedge$! (key!$\text{1}$! < key!$\text{2}$!) !$\wedge$! treeInvariant m
1
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 stackInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (stack : List (bt A)) !$\rightarrow$! Set n
3
c28e8156a37b Add paper init~agda
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
9 stackInvariant {_} {A} _ [] = Lift _ !$\top$!
1
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 stackInvariant {_} {A} tree (tree1 !$\text{::}$! [] ) = tree1 !$\equiv$! tree
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value leaf right !$\text{::}$! _) ) = (right !$\equiv$! x) !$\wedge$! stackInvariant tree tail
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value left leaf !$\text{::}$! _) ) = (left !$\equiv$! x) !$\wedge$! stackInvariant tree tail
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value left right !$\text{::}$! _ )) = ( (left !$\equiv$! x) !$\wedge$! stackInvariant tree tail) ∨ ( (right !$\equiv$! x) !$\wedge$! stackInvariant tree tail)
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 stackInvariant {_} {A} tree s = Lift _ !$\bot$!