Adding some modulo operations, Dafny immediately verifies most of the statements intended by lemmata L1 and L2:
ghost method Lemma3 (x:int,y:int)
requires x != 0;
ensures (y/x) * x + y%x == y;
{}
ghost method Lemma4 (x:int,y:int,m:int)
requires x != 0;
ensures m == y/x && y%x == 0 ==> m*x == y;
ensures m*x == y ==> (m == y/x <==> y%x == 0);
//ensures m*x == y ==> m == y/x && y%x == 0;
{}
However, Dafny fails to verify the (I believe) correct and much stronger postcondition I have commented out. (I am probably using an older version of Dafny (1.6.3.00320) and Z3.)
Dafny's definition of integer division apparently is the Euclidean one (in contrast to the floored and truncated versions), where the remainder is always greater or equal to 0, independently of the signs of numerator and denominator, as evidenced by the following
lemma, which Dafny proves immediately:
ghost method Lemma5 (x:int,y:int)
requires x != 0;
ensures y == x * (y/x) + y%x;
ensures 0 < x ==> 0 <= y%x < x;
ensures x < 0 ==> 0 <= y%x < x;
{}
But I believe the concrete results above hold in any of these versions.
Edgar
