What Dafny knows about sequences

Mar 12, 2013 at 11:24 AM
Hi Rustan,

This code

ghost method z1(ss: seq<int>, l: int, m: int, h: int)
requires 0<=l<=m<h<=|ss|;
ensures ss[m] in ss[l..h];

does not go through: it gets

input(4,3): Error BP5003: A postcondition might not hold on this return path.
input(3,16): Related location: This is the postcondition that might not hold.

What's the best assertion (or whatever) to stick in there?
Apr 25, 2013 at 12:44 AM
The "x in sq" construction is defined as:
exists i :: 0 <= i < |sq| && sq[i] == x
Such an existential quantifier often stumps the SMT solver, so you have to supply a hint that points out the witness. To us, an "obvious" witness is i:=m witness, and therefore we may expect the postcondition to be proved automatically. However, the actual witness that is needed is a index into ss[l..h], not an index into ss. So, if you stick in the assertion
assert ss[l..h][m - l] == ss[m];
the verifier will be happy.