Induction; Miracles.

Feb 6, 2013 at 12:57 AM

I found that I needed Dafny to accept something that boiled down to

(C) (forall i:: 0<=i<n ==> false) ==> n<=0 ,

but (for me) it would not. I guess that it is a fact (about the integers) that one needs to prove by induction (with a ghost method for example).

---1 Is that correct?

Assuming induction is required, I decided to do that later and, for now, just state (C) as a "fact" and carry on. This I tried by introducing a method

method C(x: int) ensures x>0 ==> (exists i:: 0<=i<x);

without a body. Although I don't recall reading this in the documentation, it seems to work in the sense that without the {...} for a body, it accepts the method's "ensurances", no matter what they are.

--2 Is that correct?

Method C is of course (potentially) miraculous in the sense that it ensuring a fact about its (immutable) argument. But theory allows this, simply deferring the problem of its implementation.

However I ran into trouble when I tried to use this technique, and here's the example:

method A(x: int) ensures x==1;
method B(x: int) ensures x==2;
method C(x: int) ensures x>0 ==> (exists i:: 0<=i<x);

method Test() {
var l,m,n;
assert l==1;
assert m==2;
assert n>0 ==> (exists i:: 0<=i<n);

The output for this (abridged) is

% dafny Test1.dfy

Dafny program verifier version, Copyright (c) 2003-2013, Microsoft.
Test1.dfy(12,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon5_Then
(0,0): anon3
Dafny program verifier finished with 4 verified, 1 error

where it seems to have accepted the miraculous effects of methods A,B; but it won't do the same for C.

--3 What's going on?

And finally (cutting through all the above),

--4 What's the best approach to telling Dafny "Just believe (C) for now?"

=== Thanks.
Feb 6, 2013 at 4:57 AM
Furthermore :-)

I tried some even simpler experiments, viz.

method Test() {
var m: int;
assert exists m: int :: m>0;
assert m>0 ==> exists m: int :: m>0;
assert 1>0 ==> exists m: int :: m>0;

In this case, all three assertions fail.

There is probably something I'm missing about the way quantification is handled: would appreciate a pointer!
Feb 6, 2013 at 11:14 PM
Found "assume" in the Boogie section of the Marktoberdorf notes, which makes the use of the "make this true" method unnecessary. But still there is some strange behaviour with exists:

method Test() {
var x: int;
assume x==0;
assert x==0;
assume exists m: int :: m>0;
assert exists m: int :: m>0;


Dafny program verifier version, Copyright (c) 2003-2013, Microsoft.
/Users/jigger/Dropbox/Dafny/Examples/Longest Upsequence/Test4.dfy(6,10): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 1 verified, 1 error
Feb 9, 2013 at 6:36 AM
Using an assumption like (forall i :: 0 <= i < n ==> false) or discharging a proof obligation like (exists i :: 0 <= i < x) will prove futile with SMT solvers that handle quantifiers the way Z3 does. The SMT solver deals with universal quantifiers (which is what both examples in my previous sentence really work out to be, once the SMT solver has negated the proof goal and is searching for a satisfying assignment) by selectively instantiating them. Informally, the SMT solver looks around at terms it has sitting around, trying to work out what might be good instantiations. It does this using matching patterns known as triggers, and these triggers must include some user-defined (that is, so-called uninterpreted) functions, not just built-in (that is, so-called interpreted) functions. In the example above, the body of the quantifier contains only constants, variables, and built-in operators, which means there are no triggering patterns, which means the quantifier will never be instantiated, which means the assumption will in effect not be used (and the proof obligation will not be discharged).

(If you're interested in more details, see the SAC 2009 paper "Reasoning about Comprehensions with First-Order SMT Solvers" by Leino and Monahan. The matching patterns used by Z3 follows what was done in Simplify before then, only much more efficiently. And Simplify had been based on ideas from Greg Nelson's PhD thesis. One alternative technique of handling quantifiers is unification, which is what first-order resolution-based prover use.)

Luckily, most quantifiers we deal with do have some structure that involves function symbols, so matching patterns arise naturally. The example you have given is an exception. Although it's probably not helpful for your problem, the following example may give you some feeling for how the triggers work.
Feb 11, 2013 at 3:01 AM
Thanks Rustan,

Meanwhile I have been reading "Solving quantified verification conditions using SMT" (Ge et al) which, together with your email, has made things a lot clearer. Could I check the following (speculative) reasoning? I have three specific questions Q1--Q3 below.

The program

method Main() {
assert (exists x:: x>0) ==> (exists x:: x>0);
assume exists x:: x>0;
assert exists x:: x>0;


input(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
Dafny program verifier finished with 1 verified, 1 error

So there's a difference between "assert A==>A;" and "assume A; assert A;". In this case the former succeeds but the latter fails.

Why does assert A==>A succeed, in spite of there being no trigger? Is it because it is a -propositional- tautology whose negation is therefore easily refuted by the SAT solver, thus never needing to examine the quantifiers at all?
===Q1: Is that correct?

And why does assume A; assert A; fail? Here I will try to combine your email with what I read in Ge et al. In this case the two abstract literals are considered to be different, and so the DPLL state begins with

|| (exists x:: x>0), (forall x:: !(x>0))

the two literals treated (to repeat) as distinct. Then after UnitPropagate we have

(exists x:: x>0), (forall x:: !(x>0)) || (exists x:: x>0), (forall x:: !(x>0))

and then after exists-inst we have

(exists x:: x>0), (forall x:: !(x>0)) || (exists x:: x>0), (forall x:: !(x>0)), !(exists x:: x>0) || X>0

for a new Skolem constant X. Then UnitPropagate gives

(exists x:: x>0), (forall x:: !(x>0)), X>0 || (exists x:: x>0), (forall x:: !(x>0)), !(exists x:: x>0) || X>0 ,

and the whole thing -would- be finished off nicely by instantiating forall x to X --- but that does not happen because no sub-expression in the forall mentions X (as indeed it cannot, since X was fresh). And so we are stuck.
===Q2: Is that correct?

===Q3: This is the essential difference between asserting an implication, and assuming antecedent then asserting consequent, that in the latter case the SAT solver does not get a chance to notice that two literals are the same?