
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!!!



I don't know if this will help, but you could try something like ensures multiset(a[..]) == multiset(old(a)[..]);



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..];
}






Thank you very much!

