Hi Nunibad,
Here is a solution to the problem:
http://rise4fun.com/Dafny/sFC5J (There may be simpler solutions.) For the reverse problem--proving that the range property (the second precondition in your example) and onto implies injectivity--see Test/VSComp2010/Problem2-Invert.dfy in the Dafny test
suite.
As for your question about should you even be here :), my suggestion would be to use multisets, if your application allows for it. That is, if you're trying to show that something is a permutation of something else, then say that its multiset of elements stays
the same. There are some examples of this in Test/dafny4, and also see Test/dafny3/GenericSort.dfy.
My solution does a number of things, which may be helpful in other situations as well. Let me highlight a few of them.
One difficulty with the example is the existential quantifier in the postcondition. Actually, the problem is not so much the existential as it is the fact that the existential sits inside a universal quantifier whose bound variable (
b
) does not
have any good trigger. Therefore, even a proof attempt like this:
assume forall b:: 0<=b<A.Length ==> exists a:: 0<=a<A.Length && A[a]==b;
assert forall b:: 0<=b<A.Length ==> exists a:: 0<=a<A.Length && A[a]==b;
does not go through. To solve this, one needs to trick Dafny into seeing the connection between the two universal quantifiers--that is, that one is used to prove the other. As described in other posts (like your
Using pointless Id to help instantiation), you could introduce some dummy function and let the automatically inferred triggers take care of it. In this example, however, you can do essentially
that, but at the same time making the text more readable. I suggest:
assume forall b :: 0 <= b < A.Length ==> InRange(A, b);
assert forall b :: 0 <= b < A.Length ==> InRange(A, b);
It is nice to write set comprehensions in the program text. But these are also tricky for the verifier, especially the most general form,
set x | R(x) :: T(x)
, which says to form the set consisting of terms like
T(x)
where
x
ranges over values satisfying
R(x)
. Even the simpler and more common form,
set x | P(x)
, which says to form the set consisting of those values
x
that satisfy
P(x)
, can be difficult. The reason for this is that, behind the scenes, such set comprehensions are turned into named functions that return the desired set. The names of these functions are generated to be different for each
textual occurrence of a set comprehension in the program. Therefore--especially if these happen to sit inside quantifiers--it can happen that different textual occurrences of the seemingly same set comprehension are not necessarily recognized as being the
same.
In my program above, I solved this problem by introducing a function for a common form of set comprehension, namely a set consisting of consecutive integers:
function IntSet(lo: int, hi: int): set<int>
{
set i | lo <= i < hi
}
This made several of the proof obligations go through, and at the same time--I think--improved the readability of the program text.
If you're writing a property involving the equality of two sets, where one set is a set comprehension, it can sometimes be advantageous to write, say,
forall b :: b in R && b in m ==> false
instead of
R * (set b | b in m) == {}
However, in my solution to the problem, either of these worked fine.
Here are several other things to note about my program:
- I wrote
lemma
instead of ghost method
, but these are essentially synonyms.
- The lemma uses a loop to compute the inverse-of-
A
map m
. There's nothing wrong with a loop inside a lemma. :)
- The
forall
statement at the end uses an unbounded range for
b
. That's fine (since we're inside a ghost context anyway). - When the body of a
forall
statement (without an explicit ensures
clause) is a
calc
, then the "exported" conclusion of the calculation automatically gets placed in an
ensures
clause for the forall
. If you're using the Dafny IDE in Visual Studio, you can hover the mouse over the
forall
keyword to see the auto-generated ensures
clause.
- The expression
b in m
, where m
is a map says that
b
is in the domain of m
. This seemed convenient at the time maps were introduced in Dafny, but I think I will change this in the future to instead provide names for the domain and range of maps. Perhaps one will then write something
like b in m.Domain
instead. - During the development of this proof, I had introduced many more proof lines than in this final version. The experience I've had with this before (and that others seem to have, too) is that with all that extra proof stuff lying around, verification times
are longer. But once I got the whole proof into place, I discovered, by trial and error, that Dafny didn't need nearly as many hints as I had supplied. Extra proof lines can be nice for the human reader, and if they are, it may be nice to keep them in the
final version. However, in this case, I thought the extra proof lines I had introduced were mostly noise, so I deleted (most of) them.
Rustan