Commit 820c7bbd authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

python: fixed for loop

parent d1798364
...@@ -36,6 +36,8 @@ let mk_unit ~loc = ...@@ -36,6 +36,8 @@ let mk_unit ~loc =
mk_expr ~loc (Etuple []) mk_expr ~loc (Etuple [])
let mk_var ~loc id = let mk_var ~loc id =
mk_expr ~loc (Eident (Qident id)) mk_expr ~loc (Eident (Qident id))
let mk_tvar ~loc id =
mk_term ~loc (Tident (Qident id))
let mk_ref ~loc e = let mk_ref ~loc e =
mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e])) mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e]))
let deref_id ~loc id = let deref_id ~loc id =
...@@ -225,7 +227,12 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) = ...@@ -225,7 +227,12 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
let lb = constant ~loc "0" in let lb = constant ~loc "0" in
let lenl = mk_expr ~loc (Eidapp (len ~loc, [mk_var ~loc l])) in let lenl = mk_expr ~loc (Eidapp (len ~loc, [mk_var ~loc l])) in
let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [lenl;constant ~loc "1"])) in 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 invariant inv =
let loc = inv.term_loc in
let li = mk_term ~loc
(Tidapp (mixfix ~loc "[]", [mk_tvar ~loc l; mk_tvar ~loc i])) in
mk_term ~loc (Tlet (id, li, deref env inv)) in
mk_expr ~loc (Efor (i, lb, To, ub, List.map invariant inv,
let li = mk_expr ~loc let li = mk_expr ~loc
(Eidapp (mixfix ~loc "[]", [mk_var ~loc l; mk_var ~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 (Elet (id, Gnone, mk_ref ~loc li,
......
from random import randint from random import randint
def testat(): # def testat():
x = 0 # x = 0
#@ label L # #@ label L
x = x+1 # x = x+1
#@ assert at(x,L) == 0 # #@ assert at(x,L) == 0
def f(x): def f(x):
#@ ensures result > x #@ ensures result > x
...@@ -18,6 +18,11 @@ def swap(a, i, j): ...@@ -18,6 +18,11 @@ def swap(a, i, j):
a[i] = a[j] a[i] = a[j]
a[j] = t a[j] = t
def foo(x):
for k in range(0, 10):
#@ invariant 0 <= k <= 10
print(k)
i = randint(0, 10) i = randint(0, 10)
#@ assert 0 <= i <= 10 #@ assert 0 <= i <= 10
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment