Dafny has support for multisets, which are really useful for reasoning about programs that permute, or otherwise deal with permutations, of sequences or arrays.
predicate Subpermutation(xs:seq, ys:seq)
ensures Subpermutation(xs,ys) ==> forall x :: x in xs ==> x in ys;
{
assert forall x :: x in xs ==> x in multiset(xs);
multiset(xs) <= multiset(ys)
}
// THEOREM
lemma SubpermutationIsSmaller(xs:seq, ys:seq)
requires Subpermutation(xs,ys);
ensures |xs| <= |ys|;
{
assert |multiset(xs)| == |xs|;
assert |multiset(ys)| == |ys|;
var xs',ys' := xs,ys;
var XS',YS' := multiset(xs),multiset(ys);
var XS'',YS'' := multiset{},multiset{};
while(|XS'|>0)
invariant Subpermutation(xs',ys');
invariant XS' == multiset(xs');
invariant YS' == multiset(ys');
invariant XS' + XS'' == multiset(xs);
invariant YS' + YS'' == multiset(ys);
invariant XS'' == YS'';
invariant XS' <= YS';
{
assert RemoveFromSequenceReducesMultiSet(xs,multiset(xs),multiset(xs[1..]));
var x := xs'[0];
xs' := Remove(x,xs');
ys' := Remove(x,ys');
XS' := XS'[x := XS'[x] - 1];
XS'' := XS''[x := XS''[x] + 1];
YS' := YS'[x := YS'[x] - 1];
YS'' := YS''[x := YS''[x] + 1];
}
}
// SUPPORTING DEFINITIONS
// following is a function lemma
predicate RemoveFromSequenceReducesMultiSet(xs:seq<T>, XS:multiset<T>, XS':multiset<T>)
requires xs != [];
requires XS' == multiset(xs[1..]);
ensures XS' == multiset(xs)[xs[0] := multiset(xs)[xs[0]] - 1];
ensures RemoveFromSequenceReducesMultiSet(xs,XS,XS');
{
assert [xs[0]]+xs[1..] == xs;
assert multiset([xs[0]]+xs[1..]) == multiset(xs);
true
}
function Remove(x:T, xs:seq<T>) :seq<T>
requires x in xs;
ensures multiset(Remove(x,xs)) == multiset(xs)[x := multiset(xs)[x] - 1];
ensures |Remove(x,xs)|+1 == |xs|;
{
assert RemoveFromSequenceReducesMultiSet(xs,multiset(xs),multiset(xs[1..]));
if xs[0]==x
then xs[1..]
else [xs[0]] + Remove(x,xs[1..])
} |