python: support for 'for x in range(i,j)'

parent 3c54dbd3
...@@ -208,19 +208,29 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) = ...@@ -208,19 +208,29 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
mk_expr ~loc (Eraise (break ~loc, None)) mk_expr ~loc (Eraise (break ~loc, None))
| Py_ast.Slabel _ -> | Py_ast.Slabel _ ->
mk_unit ~loc (* ignore lonely marks *) mk_unit ~loc (* ignore lonely marks *)
| Py_ast.Sfor (id, e, inv, body) -> (* make a special case for
(* for x in e: for id in range(e1, e2):
s *)
| Py_ast.Sfor (id, {expr_desc=Ecall ({id_str="range"}, [e1;e2])},
is translated to inv, body) ->
let inv = List.map (deref env) inv in
mk_expr ~loc (Efor (id, expr env e1, To, expr env e2, inv,
mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc (mk_var ~loc id),
let env = add_var env id in
block ~loc env body))))
(* otherwise, translate
for id in e:
#@ invariant inv
body
to
let l = e in let l = e in
for i = 0 to len(l)-1 do for i = 0 to len(l)-1 do
user invariants invariant { let id = l[i] in I }
let x = l[i] in let id = ref l[i] in
s body
done done
*) *)
| Py_ast.Sfor (id, e, inv, body) ->
let i, l, env = for_vars ~loc env in let i, l, env = for_vars ~loc env in
let e = expr env e in let e = expr env e in
mk_expr ~loc (Elet (l, Gnone, e, (* evaluate e only once *) mk_expr ~loc (Elet (l, Gnone, e, (* evaluate e only once *)
...@@ -264,6 +274,8 @@ let spec env sp = ...@@ -264,6 +274,8 @@ let spec env sp =
sp_pre = List.map (deref env) sp.sp_pre; sp_pre = List.map (deref env) sp.sp_pre;
sp_post = List.map (post env) sp.sp_post } sp_post = List.map (post env) sp.sp_post }
let no_params ~loc = [loc, None, false, Some (PTtuple [])]
(* f(x1,...,xn): body (* f(x1,...,xn): body
let f x1 ... xn = let f x1 ... xn =
...@@ -281,16 +293,14 @@ let def inc (id, idl, sp, bl) = ...@@ -281,16 +293,14 @@ let def inc (id, idl, sp, bl) =
mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc (mk_var ~loc id), bl)) in mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc (mk_var ~loc id), bl)) in
let body = List.fold_left local body idl in let body = List.fold_left local body idl in
let param id = id.id_loc, Some id, false, None in let param id = id.id_loc, Some id, false, None in
let params = List.map param idl in let params = if idl = [] then no_params ~loc else List.map param idl in
let fd = (params, None, body, sp) in let fd = (params, None, body, sp) in
let d = Dfun (id, Gnone, fd) in let d = Dfun (id, Gnone, fd) in
inc.new_pdecl id.id_loc d inc.new_pdecl id.id_loc d
let translate ~loc inc (dl, s) = let translate ~loc inc (dl, s) =
List.iter (def inc) dl; List.iter (def inc) dl;
let params = [loc, None, false, Some (PTtuple [])] in let fd = (no_params ~loc, None, block empty_env ~loc s, empty_spec) in
let env = empty_env in
let fd = (params, None, block env ~loc s, empty_spec) in
let main = Dfun (mk_id ~loc "main", Gnone, fd) in let main = Dfun (mk_id ~loc "main", Gnone, fd) in
inc.new_pdecl loc main inc.new_pdecl loc main
......
from random import randint from random import randint
# def testat():
# x = 0
# #@ label L
# x = x+1
# #@ assert at(x,L) == 0
def f(x): def f(x):
#@ ensures result > x #@ ensures result > x
return x+1 return x+1
...@@ -18,10 +12,12 @@ def swap(a, i, j): ...@@ -18,10 +12,12 @@ def swap(a, i, j):
a[i] = a[j] a[i] = a[j]
a[j] = t a[j] = t
def foo(x): def t10():
for k in range(0, 10): s = 0
#@ invariant 0 <= k <= 10 for i in range(0, 10):
print(k) #@ invariant 2 * s == i * (i-1)
s = s + i
#@ assert s == 55
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