
http://rise4fun.com/Dafny/bVR
It has been simplified to just show the problem that the assert after the recursive call to the lemma should be satisfied, it is the induction hypothesis.


Sep 24, 2015 at 4:41 PM
Edited Sep 24, 2015 at 4:43 PM






Sep 25, 2015 at 1:52 PM
Edited Sep 25, 2015 at 3:45 PM

Hi, as far as I remember, Dafny translates to Boogie, and Boogie has syntax for div and mod operator, but their operational semantics are not complete (since their operation semantics various from language to language, e.g. when negative numbers are involved).
So in general I think because of this level of incompleteness, when proof involves these operators, the user might need to help the verifier a little bit, e.g. give more information, rewrite the proof obligation to be simpler or expand/rewrite the definition
of these operator. I find this is quite common during my experience with Dafny or Boogie.
There are probably other reasons behind why your second example does not verified (and I am really interested in knowing ;) ). But I find the trick of help Dafny with more information of mod and div operator still applies:
http://rise4fun.com/Dafny/iTz3
Cheers, Zheng



Hi Zheng,
>>>>> Back to your second example, correct me if I am wrong, I do not think it is provable, since (n/m)*m != n, e.g. (1/2) * 2 == 0
Of course, it is not provable in general, but
(n/m)*m != n <==> n%m==0.
So, I used it as a trick to avoid the use of the mod operator.
Thanks,
Paqui
De: zcheng [email removed]
Enviado el: viernes, 25 de septiembre de 2015 15:52
Para: [email removed]
Asunto: Re: Induction hypothesis doesn't work? [dafny:644665]
From: zcheng
Hi, as far as I remember, Dafny translates to Boogie, and Boogie has syntax for div and mod operator, but their operational semantics are not complete (since their operation semantics various from language to language,
e.g. when negative numbers are involved, or whether 1/2 == 0).
Because of this level of incompleteness, when trivial lemma involve these operators, the user might need to help the verifier a little bit, e.g. rewrite the proof obligation to be simpler or expand/rewrite the definition of these operator. I find this is quite
common during my experience with Dafny or Boogie.
Back to your second example, correct me if I am wrong, I do not think it is provable, since (n/m)*m != n, e.g. (1/2) * 2 == 0
Cheers, Zheng



Hi Zheng,
Back to your second example, correct me if I am wrong, I do not think it is provable, since (n/m)*m != n, e.g. (1/2) * 2 == 0
Of course, it is not provable in general, but (n/m)*m != n <==> n%m==0.
So, I used it as a trick to avoid the use of the mod operator.
Thanks,
Paqui

