python: lists

parent 013e16e1
......@@ -5,18 +5,29 @@ module Python
use import ref.Ref
use seq.Seq as S
(* Python's lists are resizable arrays *)
type list 'a = ref (S.seq 'a)
function ([]) (l: list 'a) (i: int) : 'a =
S.([]) !l i
S.get !l i
function len (l: list 'a) : int =
S.length !l
let ([]) (l: list 'a) (i: int) : 'a
requires { 0 <= i < S.length !l }
ensures { result = l[i] }
= S.([]) !l i
= S.get !l i
let ([]<-) (l: list 'a) (i: int) (v: 'a) : unit
requires { 0 <= i < S.length !l }
writes { l }
ensures { !l = S.set (old !l) i v }
= l := S.set !l i v
val range (l u: int) : list int
requires { l <= u }
ensures { S.length !result = u - l }
ensures { forall i. l <= i < u -> result[i] = i }
end
......@@ -122,8 +122,9 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
block env ~loc [s]
| Py_ast.Sfor (_id, _e, _s) ->
assert false (*TODO*)
| Py_ast.Sset (_e1, _e2, _e3) ->
assert false (*TODO*)
| Py_ast.Sset (e1, e2, e3) ->
mk_expr ~loc (Eidapp (mixfix ~loc "[]<-",
[expr env e1; expr env e2; expr env e3]))
| Py_ast.Sassert t ->
mk_expr ~loc (Eassert (Aassert, deref env t))
......
......@@ -215,6 +215,8 @@ term_:
| q=quant l=comma_list1(ident) DOT t=term
{ let var id = id.id_loc, Some id, false, None in
Tquant (q, List.map var l, [], t) }
| id=ident LEFTPAR l=separated_list(COMMA, term) RIGHTPAR
{ Tidapp (Qident id, l) }
quant:
| FORALL { Tforall }
......
......@@ -11,6 +11,15 @@ while b < 100:
a = b-a
l = range(0, 10)
## assert forall i. 0 <= i < 10 -> l[i] >= 0
l[2] = 42
## assert l[2] == 42
i = 0
while i < 10:
## invariant 0 <= i
## invariant forall j. 0 <= j < i -> l[j] == 0
## invariant len(l) == 10
l[i] = 0
i = i+1
# Local Variables:
# compile-command: "make -C ../.. && why3 ide test.py"
......
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