Interesting behaviour of Sequence slicing

Aug 27, 2013 at 3:29 PM
Edited Aug 27, 2013 at 3:58 PM
Hi All,

I have this simple dafny program using sequence slicing:
method Main() {
  var s := [1, 2, 3];
  var p := s[..3];
  
  assert 2 in p;   // fail to verify
}
I know provide a witness that above the failed assertion will do the trick, e.g.
assert p[1] == 2;
Interestingly, if I 'drop first n element'(i.e. [i..]), it is fine, e.g.
method Main() {
  var s := [1, 2, 3];
  var p := s[0..];
  
  assert 1 in p;
}
My guess is that in the Dafny prelude, the following axiom knot Seq#Drop() with Seq#Build():
axiom (forall<T> s: Seq T, v: T, n: int ::
    0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
But Seq#Build() is a stranger to Seq#Take(). Thus, I put the following axioms in DafnyPrelude.bpl, to ask Seq#Take() be friend with Seq#Build():
axiom (forall<T> s: Seq T, v: T, n: int ::
    0 <= n && n <= Seq#Length(s) ==> Seq#Take(Seq#Build(s, v), n) == Seq#Take(s, n)) ;  
axiom (forall<T> s: Seq T, v: T, n: int ::
    n == Seq#Length(Seq#Build(s, v)) ==> Seq#Take(Seq#Build(s, v), n) == Seq#Build(s, v)) ;
Could someone comment on the issue? for example, might be there is soundness/efficiency concern of not doing so?

One more question, The following Boogie attribute looks interesting in the Dafny prelude. May I ask what does it do?
{:weight 25}
Regards,
Zheng