Commit c5d55701 by Jean-Christophe Filliâtre

python: support for break in while loops

parent 20cdd188
 ... ... @@ -70,4 +70,8 @@ module Python requires { l <= u } ensures { l <= result <= u } val input () : int exception Break end
 from random import randint n = 42 a = [0] * n a[0] = randint(0, 100) i = 1 while i < n: #@ invariant 1 <= i #@ invariant forall i1, i2. 0 <= i1 <= i2 < i -> a[i1] <= a[i2] a[i] = a[i-1] + randint(0, 10) i = i + 1 #@ assert len(a) == n #@ assert forall i1, i2. 0 <= i1 <= i2 < len(a) -> a[i1] <= a[i2] print(a) v = input("quelle valeur cherchez-vous : ") l = 0 u = n-1 r = -1 while r == -1 and l <= u: #@ invariant 0 <= l and u < n #@ invariant -1 <= r < n #@ invariant if r >= 0 then a[r] == v else forall i. 0 <= i < n -> a[i] == v -> l <= i <= u #@ variant u-l m = (l + u) // 2 #@ assert l <= m and m <= u if a[m] < v: l = m+1 elif a[m] > v: u = m-1 else: #@ assert a[m] == v r = m break #@ assert -1 <= r < n #@ assert if r >= 0 then a[r] == v else forall i. 0 <= i < n -> a[i] != v
 a = input("entrez a : ") b = input("entrez b : ") #@ assume b >= 0 p = a q = b r = 0 while q > 0: #@ invariant 0 <= q and r + p * q == a * b #@ variant q if q % 2 == 1: r = r + p p = p + p q = q // 2 print(r) #@ assert r == a * b
 ... ... @@ -55,6 +55,7 @@ and stmt_desc = | Seval of expr | Sset of expr * expr * expr (* e1[e2] = e3 *) | Sassert of Ptree.assertion_kind * Ptree.term | Sbreak and block = stmt list ... ...
 ... ... @@ -28,7 +28,7 @@ "for", FOR; "in", IN; "and", AND; "or", OR; "not", NOT; "True", TRUE; "False", FALSE; "None", NONE; "from", FROM; "import", IMPORT; "from", FROM; "import", IMPORT; "break", BREAK; (* annotations *) "forall", FORALL; "exists", EXISTS; "then", THEN; "let", LET; ]; ... ...
 ... ... @@ -16,6 +16,7 @@ open Stdlib let debug = Debug.register_flag "python" ~desc:"mini-python plugin debug flag" let () = Debug.set_flag Dterm.debug_ignore_unused_var let mk_id ?(loc=Loc.dummy_position) name = { id_str = name; id_lab = []; id_loc = loc } ... ... @@ -42,6 +43,10 @@ let constant ~loc s = mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s))) let len ~loc = Qident (mk_id ~loc "len") let break ~loc = Qident (mk_id ~loc "Break") let catch_break ~loc = [break ~loc, None, mk_unit ~loc] let array_make ~loc n v = mk_expr ~loc (Eidapp (Qdot (Qident (mk_id ~loc "Array"), mk_id ~loc "make"), [n; v])) ... ... @@ -90,6 +95,15 @@ let loop_annotation env a = let add_loop_invariant i a = { a with loop_invariant = i :: a.loop_invariant } let rec has_break s = match s.Py_ast.stmt_desc with | Py_ast.Sbreak -> true | Py_ast.Sreturn _ | Py_ast.Sassign _ | Py_ast.Sprint _ | Py_ast.Seval _ | Py_ast.Sset _ | Py_ast.Sassert _ | Py_ast.Swhile _ -> false | Py_ast.Sif (_, bl1, bl2) -> has_breakl bl1 || has_breakl bl2 | Py_ast.Sfor (_, _, _, bl) -> has_breakl bl and has_breakl bl = List.exists has_break bl let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with | Py_ast.Enone -> mk_unit ~loc ... ... @@ -167,8 +181,11 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) = | Py_ast.Sassert (k, t) -> mk_expr ~loc (Eassert (k, deref env t)) | Py_ast.Swhile (e, ann, s) -> mk_expr ~loc (Ewhile (expr env e, loop_annotation env ann, block env ~loc s)) let loop = mk_expr ~loc (Ewhile (expr env e, loop_annotation env ann, block env ~loc s)) in if has_breakl s then mk_expr ~loc (Etry (loop, catch_break ~loc)) else loop | Py_ast.Sbreak -> mk_expr ~loc (Eraise (break ~loc, None)) | Py_ast.Sfor (id, e, inv, body) -> (* for x in e: s ... ...
 ... ... @@ -64,7 +64,7 @@ %token CMP %token IDENT %token DEF IF ELSE ELIF RETURN PRINT WHILE FOR IN AND OR NOT NONE TRUE FALSE %token FROM IMPORT %token FROM IMPORT BREAK %token EOF %token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE %token PLUS MINUS TIMES DIV MOD ... ... @@ -238,6 +238,8 @@ simple_stmt_desc: { Sassert (k, t) } | e = expr { Seval e } | BREAK { Sbreak } ; assertion_kind: ... ...
 ... ... @@ -2,7 +2,7 @@ from random import randint # def swap(a, i, j): # #@ requires 0 <= i < len(a) and 0 <= j < len(a) # # @ requires 0 <= i < len(a) and 0 <= j < len(a) # t = a[i] # a[i] = a[j] # a[j] = t ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!