Векторы и последовательности в буги-вуги

Question

Просматривая тесты, поставляемые с Boogie, я заметил, что существует два типа коллекций:Seq TиVec T. Примеры:

      type {:builtin "Seq"} Seq _;
function {:builtin "seq.empty"} empty(): Seq int;
function {:builtin "seq.len"} len(a: Seq int): int;
function {:builtin "seq.++"} append(a: Seq int, b: Seq int): Seq int;
function {:builtin "seq.unit"} unit(v: int): Seq int;
function {:builtin "seq.nth"} nth(a: Seq int, i: int): int;

procedure test()
{
  var s: Seq int;

  s ≔  append(unit(1),unit(2));
  assert nth(s,0) == 1;
  assert nth(s,1) == 2;
  assert len(s) == 2;
}

Вышеприведенное иллюстрирует использование последовательностей, тогда как для векторов это будет:

      procedure test()
{
  var s: Vec int;

  s ≔  Vec_Append(Vec_Empty(),1);
  s ≔  Vec_Append(s,2);
  assert Vec_Nth(s,0) == 1;
  assert Vec_Nth(s,1) == 2;
  assert Vec_Len(s) == 2;
}

(Это должно быть скомпилировано с -lib)

Поиск внутри файлаCore/LibraryDefinitions.bplЯ понимаюVecопределяется не так, какSeq.

Мой вопрос: Какая разница здесь?