Dafny

Unique.dfy

method Unique(a: seq<int>) returns (b: seq<int>)
  ensures forall k :: 0 <= k < |a| ==> a[k] in b
  ensures forall i, j :: 0 <= i < j < |b| ==> b[i] != b[j]
{
  var index := 0;
  b := [];
  while index < |a|
    invariant index <= |a|
    invariant forall i, j :: 0 <= i < j < |b| ==> b[i] != b[j]
    invariant forall k :: 0 <= k < index ==> a[k] in b
  {
    if (a[index] !in b) {
      b := b + [a[index]];
    }
    assert a[index] in b;
    index := index + 1;
  }
  return b;
}

//https://rise4fun.com/Dafny/3K7p