obj SKDB;
obj Key;
obj Elem;

operation SortDB
    inputs:    d:SKDB, k:Key;
    outputs:   d':SKDB;
    pre:       ;
    post:      forall (i:integer) forall (j:integer)
                 if i<j then FindNth(d',i).k < FindNth(d',j).k;
    description: (* Sort a database *);

end SortDB;

operation FindNth
    inputs:d:SKDB, n:number;
    outputs: e:Elem;
    description: (* Find the DB element at position n. *);
end FindNth;