VerifyThis Exercise 2
Exercise 2 of the Viper Tutorial at VerifyThis 2018.
field val : Int
field left : Ref
field right : Ref
predicate Tree(t:Ref) {
t != null ==> acc(t.val) && acc(t.left) && acc(t.right) &&
Tree(t.left) && Tree(t.right)
}
function size(t:Ref) : Int
requires Tree(t)
ensures result >= 0
{
unfolding Tree(t) in
(t == null ? 0 : 1 + size(t.left) + size(t.right))
}
function lookup(t:Ref, i:Int) : Int
requires Tree(t) && 0 <= i && i < size(t)
{
unfolding Tree(t) in
(i < size(t.left) ? lookup(t.left,i) :
(i == size(t.left) ? t.val : lookup(t.right,i - size(t.left) - 1)))
}
method insertLeft(t:Ref, v:Int) returns (res: Ref)
requires Tree(t)
ensures Tree(res)
ensures size(res) == old(size(t)) + 1
ensures lookup(res,0) == v
ensures forall i:Int :: 0 < i && i < size(res) ==> lookup(res,i) == old(lookup(t,i-1))
{
if(t != null) {
var tmp : Ref // used to save result of method call
unfold Tree(t)
tmp := insertLeft(t.left,v)
t.left := tmp
fold Tree(t)
res := t
} else {
res := new(left,val,right)
res.left := null
res.right := null
res.val := v
fold Tree(res.left)
fold Tree(res.right)
fold Tree(res)
}
}
method insert(t:Ref, v:Int) returns (res: Ref, pos: Int)
requires Tree(t)
ensures Tree(res)
ensures size(res) == old(size(t)) + 1
ensures 0 <= pos && pos < size(res)
ensures lookup(res,pos) == v
ensures forall i:Int :: 0 <= i && i < pos ==> lookup(res,i) == old(lookup(t,i))
ensures forall i:Int :: pos < i && i < size(res) ==> lookup(res,i) == old(lookup(t,i-1))
{
if(t != null) {
var tmp : Ref // used to save results of method calls
unfold Tree(t)
// <-- fill in your code here
fold Tree(t)
res := t
} else {
res := new(left,val,right)
res.left := null
res.right := null
res.val := v
fold Tree(res.left)
fold Tree(res.right)
fold Tree(res)
pos := 0
}
}