python: division and modulus, fixed for loop

modules/python.mlw

@@ -34,11 +34,38 @@ module Python
     ensures  { A.length result = u - l }
     ensures  { forall i. l <= i < u -> result[i] = i }
 
-  (* TODO: specify division and modulus according to
+  (* Python's division and modulus according are neither Euclidean division,
+     nor computer division, but something else defined in
      https://docs.python.org/3/reference/expressions.html *)
-  function div int int : int
-  function mod int int : int
 
+  use import int.Abs
+  use int.EuclideanDivision as E
+
+  function div (x y: int) : int =
+    let q = E.div x y in
+    if y >= 0 then q else if E.mod x y > 0 then q-1 else q
+  function mod (x y: int) : int =
+    let r = E.mod x y in
+    if y >= 0 then r else if r > 0 then r+y else r
+
+  lemma div_mod:
+    forall x y:int. y <> 0 -> x = y * div x y + mod x y
+  lemma mod_bounds:
+    forall x y:int. y <> 0 -> 0 <= abs (mod x y) < abs y
+  lemma mod_sign:
+    forall x y:int. y <> 0 -> if y < 0 then mod x y <= 0 else mod x y >= 0
+
+  let (//) (x y: int) : int
+    requires { y <> 0 }
+    ensures  { result = div x y }
+  = div x y
+
+  let (%) (x y: int) : int
+    requires { y <> 0 }
+    ensures  { result = mod x y }
+  = mod x y
+
+  (* random.randint *)
   val randint (l u: int) : int
     requires { l <= u }
     ensures  { l <= result <= u }

plugins/python/py_ast.ml

@@ -50,7 +50,7 @@ and stmt_desc =
   | Sassign of ident * expr
   | Sprint of expr
   | Swhile of expr * Ptree.loop_annotation * block
-  | Sfor of ident * expr *  Ptree.loop_annotation * block
+  | Sfor of ident * expr * Ptree.invariant * block
   | Seval of expr
   | Sset of expr * expr * expr (* e1[e2] = e3 *)
   | Sassert of Ptree.assertion_kind * Ptree.term

plugins/python/py_main.ml

@@ -123,7 +123,7 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
   | Py_ast.Ecall (id, el) ->
     mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
   | Py_ast.Elist _el ->
-    assert false
+    assert false (*TODO*)
   | Py_ast.Eget (e1, e2) ->
     mk_expr ~loc (Eidapp (mixfix ~loc "[]", [expr env e1; expr env e2]))
 
@@ -152,33 +152,32 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
   | Py_ast.Swhile (e, ann, s) ->
     mk_expr ~loc
       (Ewhile (expr env e, loop_annotation env ann, block env ~loc s))
-  | Py_ast.Sfor (id, e, ann, body) ->
-    (* for x in e: s
-                             is translated to
+  | Py_ast.Sfor (id, e, inv, body) ->
+    (* for x in e:
+         s
+
+    is translated to
+
        let l = e in
-       let i = ref 0 in
-       while !i < len(e) do
-         invariant 0 <= !i (and user invariants)
-         let x = l[!i] in
-         s;
-         i := !i + 1
+       for i = 0 to len(l)-1 do
+         user invariants
+         let x = l[i] in
+         s
        done
     *)
     let i, l, env = for_vars ~loc env in
     let e = expr env e in
-    let env = add_var env id in
     mk_expr ~loc (Elet (l, Gnone, e, (* evaluate e only once *)
-    mk_expr ~loc (Elet (i, Gnone, mk_ref ~loc (constant ~loc "0"),
+    let lb = constant ~loc "0" in
     let lenl = mk_expr ~loc (Eidapp (len ~loc, [mk_var ~loc l])) in
-    let test =
-      mk_expr ~loc (Eidapp (infix ~loc "<", [deref_id ~loc i; lenl])) in
-    mk_expr ~loc (Ewhile (test, loop_annotation env ann,
+    let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [lenl;constant ~loc "1"])) in
+    mk_expr ~loc (Efor (i, lb, To, ub, List.map (deref env) inv,
     let li = mk_expr ~loc
-      (Eidapp (mixfix ~loc "[]", [mk_var ~loc l; deref_id ~loc i])) in
+      (Eidapp (mixfix ~loc "[]", [mk_var ~loc l; mk_var ~loc i])) in
     mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc li,
-    mk_expr ~loc (Esequence (block env body,
-    mk_expr ~loc (Eidapp (Qident (mk_id ~loc "incr"), [mk_var ~loc i])))
-    )))))))))
+    let env = add_var env id in
+    block env body
+    ))))))
 
 and block env ?(loc=Loc.dummy_position) = function
   | [] ->

plugins/python/py_parser.mly

@@ -152,7 +152,7 @@ stmt_desc:
 | WHILE e = expr COLON b=loop_body
     { let a, l = b in Swhile (e, a, l) }
 | FOR x = ident IN e = expr COLON b=loop_body
-    { let a, l = b in Sfor (x, e, a, l) }
+    { let a, l = b in Sfor (x, e, a.loop_invariant, l) }
 ;
 
 loop_body:

plugins/python/test.py

@@ -23,18 +23,20 @@ while i < 10:
   l[i] = 0
   i = i+1
 
+sum = 0
 for x in l:
+  #@ invariant sum >= 0
   print(x)
+  #@ assert x >= 0
+  sum = sum+x
 
-# # arithmetic
-# # Python's division is not *Euclidean* division
-# q = -4 // 3
-# #@ assert q == -2
-# r = -4 % 3
-# #@ assert r == 2
-# #@ assert 4 // -3 == -2
-# #@ assert 4 % -3 == -2
+# Python's division is neither Euclidean division, nor computer division
+#@ assert  4 //  3 ==  1 and  4 %  3 ==  1
+#@ assert -4 //  3 == -2 and -4 %  3 ==  2
+#@ assert  4 // -3 == -2 and  4 % -3 == -2
+#@ assert -4 // -3 ==  1 and -4 % -3 == -1
 
 # Local Variables:
 # compile-command: "make -C ../.. && why3 prove -P alt-ergo test.py"
 # End:
+