Num_of in Dafny?

Oct 2, 2014 at 5:02 PM
Hello! I'm trying to specify in Dafny something like this:

ensures forall h :: 0 <= h && h < a.length ==> (num_of k :: 0 <= k && k < a.Length; a[k] == a[h]) == (num_of m :: 0 <= m && m < old(a).Length; old(a)[m] == a[h]);

I need to count the occurrences of a element, but I don´t find the num_of primitive in dafny. It is possible write something like that in dafny? But without a auxiliar function?

Thanks!!!
Oct 2, 2014 at 7:53 PM
I don't know if this will help, but you could try something like ensures multiset(a[..]) == multiset(old(a)[..]);
Oct 2, 2014 at 8:01 PM
I found an example in the Dafny tests.

If you look in this test case for dafny you can see an example of a swap method for arrays that is specified using the construction I suggested above. So if you are trying to verify some kind of sort (which I guess you are) then you could perhaps use this swap method to build your sort method.
method test7(a: array<int>, i: int, j: int)
  requires a != null && 0 <= i < j < a.Length;
  modifies a;
  ensures old(multiset(a[..])) == multiset(a[..]);
  ensures a[j] == old (a[i]) && a[i] == old(a[j]);
  ensures forall k :: 0 <= k < a.Length && k !in {i, j} ==> a[k] == old(a[k]);
{
  ghost var s := a[..i] + [a[i]] + a[i+1 .. j] + [a[j]] + a[j+1..];
  assert a[..] == s;
  a[i], a[j] := a[j], a[i];
  assert a[..] == a[..i] + [a[i]] + a[i+1 .. j] + [a[j]] + a[j+1..];
  assert s == a[..i] + [old(a[i])] + a[i+1 .. j] + [old(a[j])] + a[j+1..];
}
Oct 2, 2014 at 8:06 PM
And here is a full array sort example that uses old(multiset(a[..])) == multiset(a[..])

https://dafny.codeplex.com/SourceControl/latest#Test/dafny3/GenericSort.dfy
Oct 3, 2014 at 5:56 PM
Thank you very much!