Function body needs to be asserted manually
Closed this issue · 2 comments
dnezam commented
Consider the following Viper program:
domain Unit {
function unit(): Unit
}
function Asserting(b: Bool): Unit
requires b
{ unit() }
function Flatten(xs: Seq[Seq[Int]]): Seq[Int]
decreases xs
{
(|xs| == 0 ?
Seq[Int]() :
xs[0] ++ Flatten(xs[1..]))
}
function FlattenSingleton(xs: Seq[Int]): Unit
ensures Flatten(Seq(xs)) == xs
{
// Does not work:
// unit()
// Does not work:
// Asserting(|Seq(xs)| != 0)
// Does not work:
// let _ == (Flatten(Seq(xs))) in unit()
// This works:
Asserting(Flatten(Seq(xs)) == (|Seq(xs)| == 0 ?
Seq[Int]() :
Seq(xs)[0] ++ Flatten(Seq(xs)[1..])))
}
Why does this only verify if the body of Flatten
is manually asserted? Shouldn't it already be available from Flatten(Seq(xs))
in the postcondition?
marcoeilers commented
This is not the function body being unavailable but the (intended!) incompleteness of recursive functions. Flatten
's definition is unfolded once for every argument for which you use it.
So by default, when you talk about Flatten(Seq(xs))
, the verifier knows that it is equal to its body, but it does not unfold the recursive call Flatten(Seq(xs)[1..])
. If you mention that call manually, its definition will be unfolded and you can prove your postcondition:
method m(xs: Seq[Int]) {
assert Flatten(Seq(xs)[1..]) == Seq() // this line is needed to make the next one pass
assert Flatten(Seq(xs)) == xs
}
dnezam commented
That completely slipped my mind. Thank you for the clarification!