diff --git a/modules/python.mlw b/modules/python.mlw index 42799aa2fa0abb67dea3c5cd6b263de4c8982734..0b0c68d81c57db0ed009882cad75041d8d6d9490 100644 --- a/modules/python.mlw +++ b/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 } diff --git a/plugins/python/py_ast.ml b/plugins/python/py_ast.ml index 7da0690120165cb10a09f1f1451334b145b0be30..6abfa12a686ca74ad59d4570388cb0ff9c6ed477 100644 --- a/plugins/python/py_ast.ml +++ b/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 diff --git a/plugins/python/py_main.ml b/plugins/python/py_main.ml index 88522557680c84a7a71a9ff8fa4c4fe94983ac39..ba858572e41899439b464e6c7dbd4d6d22945454 100644 --- a/plugins/python/py_main.ml +++ b/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 | [] -> diff --git a/plugins/python/py_parser.mly b/plugins/python/py_parser.mly index 67ef15971f9d2cd9212e310c76d79d09d3889b87..8ae3d88bde5aba0602e374120481ebb1af3706f8 100644 --- a/plugins/python/py_parser.mly +++ b/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: diff --git a/plugins/python/test.py b/plugins/python/test.py index 8ba78453a85b19cddddd02c9531c0fa599dd2995..8c17c46db6be016391dd32eb78bab31e3a52576e 100644 --- a/plugins/python/test.py +++ b/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: +