Sequence-related incompleteness, potentially trigger-related

[viper-admin]

Created by @mschwerhoff on 2016-02-15 20:15
Last updated on 2016-02-15 22:23

The postcondition of test02 fails in Silicon and Carbon if the assertion in the body is commented.

#!text

function zip(xs: Seq[Ref], ys: Seq[Ref]): Seq[Ref]
  requires |xs| == |ys| || |xs| == |ys| + 1
{
  (ys == Seq[Ref]())
     ? xs
     : Seq(xs[0], ys[0]) ++ zip(xs[1..], ys[1..])
}

method test02(xs: Seq[Ref], ys: Seq[Ref], x: Ref, y: Ref)
  requires xs == Seq(x)
  requires ys == Seq(y)
  ensures  Seq(x, y) == zip(xs, ys) // Fails w/o A1
{
  assert zip(xs, ys) == Seq(x, y) ++ zip(xs[1..], ys[1..])  // Required (A1)
  // assert zip(xs, ys) == Seq(x, y) ++ zip(Seq[Ref](), Seq[Ref]()) // Fails w/o A1
}

[viper-admin]

@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 
}