Open viper-admin opened 8 years ago
@mschwerhoff commented on 2016-02-15 22:23
#!text
function zip(xs: Seq[Ref], ys: Seq[Ref]): Seq[Ref]
requires |xs| == |ys| || |xs| == |ys| + 1
{
(ys == Seq[Ref]())
? xs
: Seq(xs[0]) ++ zip(ys, xs[1..])
}
method lemma_zip_over_append_left(a: Ref, as: Seq[Ref], bs: Seq[Ref])
requires |as| == |bs| || |as| == |bs| + 1
ensures zip(Seq(a) ++ bs, as) == Seq(a) ++ zip(as, bs)
{
assert (Seq(a) ++ bs)[1..] == bs // Required to prove the postcondition
}
The postcondition of
test02
fails in Silicon and Carbon if the assertion in the body is commented.