Commit f89faf74 by Jean-Christophe Filliatre

### programs: updated examples (array -> map)

parent 3400ed09
 ... ... @@ -17,13 +17,13 @@ module Algo63 use import int.Int use import module stdlib.Ref use import module stdlib.Array use import array.ArrayPermut use import module stdlib.ArrayPermut parameter partition : a : array int -> m:int -> n:int -> i:ref int -> j:ref int -> { m < n } unit writes a.contents i.contents j.contents { m <= j and j < i and i <= n and permut (old a) a m n and unit writes a i j { m <= j and j < i and i <= n and permut_sub (old a) a m n and exists x:int. (forall r:int. m <= r <= j -> a[r] <= x) and (forall r:int. j < r < i -> a[r] = x) and ... ...
 ... ... @@ -17,16 +17,20 @@ module Algo64 use import int.Int use import module stdlib.Ref use import module stdlib.Array use import array.ArrayPermut clone import array.ArraySorted with type elt = int, logic le = (<=) use import module stdlib.ArrayPermut logic sorted_sub (a: array int) (l u: int) (* clone import module stdlib.ArraySorted with type elt = int, logic le = (<=) *) (* Algorithm 63 *) parameter partition : a : array int -> m:int -> n:int -> i:ref int -> j:ref int -> a:array int -> m:int -> n:int -> i:ref int -> j:ref int -> { 0 <= m < n < length a } unit writes a.contents i.contents j.contents { m <= j < i <= n and permut (old a) a m n and unit writes a i j { m <= j < i <= n and permut_sub (old a) a m n and exists x:int. (forall r:int. m <= r <= j -> a[r] <= x) and (forall r:int. j < r < i -> a[r] = x) and ... ... @@ -43,12 +47,12 @@ module Algo64 partition a m n i j; label L1: quicksort a m !j; assert { permut (at a L1) a m n }; assert { permut_sub (at a L1) a m n }; label L2: quicksort a !i n; assert { permut (at a L2) a m n } assert { permut_sub (at a L2) a m n } end { permut (old a) a m n and sorted_sub a m n } { permut_sub (old a) a m n and sorted_sub a m n } end ... ...
 ... ... @@ -17,15 +17,15 @@ module Algo65 use import int.Int use import module stdlib.Ref use import module stdlib.Array use import array.ArrayPermut use import module stdlib.ArrayPermut (* algorithm 63 *) parameter partition : a : array int -> m:int -> n:int -> i:ref int -> j:ref int -> { 0 <= m < n < length a } unit writes a.contents i.contents j.contents { m <= j < i <= n and permut (old a) a m n and unit writes a i j { m <= j < i <= n and permut_sub (old a) a m n and exists x:int. (forall r:int. m <= r <= j -> a[r] <= x) and (forall r:int. j < r < i -> a[r] = x) and ... ... @@ -40,13 +40,13 @@ module Algo65 let j = ref 0 in label L1: partition a m n i j; assert { permut (at a L1) a m n }; assert { permut_sub (at a L1) a m n }; label L2: if k <= !j then find a m !j k; assert { permut (at a L2) a m n }; assert { permut_sub (at a L2) a m n }; if !i <= k then find a !i n k end { permut (old a) a m n and { permut_sub (old a) a m n and (forall r:int. m <= r <= k -> a[r] <= a[k]) and (forall r:int. k <= r <= n -> a[k] <= a[r]) } ... ...
 ... ... @@ -4,12 +4,11 @@ module M use import module stdlib.Refint use import array.ArrayLength use import module stdlib.Array parameter a : array int logic inv (a : map int) = logic inv (a : array int) = a[0] = 0 and length a = 11 and forall k:int. 1 <= k <= 10 -> 0 < a[k] parameter loop1 : ref int ... ... @@ -44,11 +43,11 @@ end module ARM use export int.Int use export array.Array use export map.Map use export module stdlib.Ref (* memory *) parameter mem : ref (t int int) parameter mem : ref (map int int) parameter mem_ldr : a:int -> {} int reads mem.contents { result = mem[a] } parameter mem_str : a:int -> v:int -> {} int writes mem.contents { mem = (old mem)[a <- v] } ... ... @@ -115,10 +114,10 @@ module InsertionSortExample (* stack and data segment do not overlap *) logic separation (fp : int) = a+10 < fp-24 logic inv (mem : t int int) = logic inv (mem: map int int) = mem[a] = 0 and forall k:int. 1 <= k <= 10 -> 0 < mem[a + k] logic inv_l2 (mem : t int int) (fp : int) (l4 : int) = logic inv_l2 (mem: map int int) (fp : int) (l4 : int) = 2 <= mem[fp - 16] <= 11 and l4 = mem[fp-16] - 2 and inv mem let path_init_l2 () = ... ...
 ... ... @@ -3,7 +3,7 @@ module M use import int.Int use import module stdlib.Ref use import array.Array use import map.Map type pointer ... ...
 ... ... @@ -118,7 +118,7 @@ module ArrayEq logic array_eq_sub (a1 a2: array 'a) (l u: int) = map_eq_sub a1.elts a2.elts l u logic array_eq (a1 a2 : array 'a) = logic array_eq (a1 a2: array 'a) = a1.length = a2.length and array_eq_sub a1 a2 0 a1.length ... ... @@ -129,10 +129,10 @@ module ArrayPermut use import module Array clone import map.MapPermut as M logic permut_sub (a1 a2 : array 'a) (l u: int) = logic permut_sub (a1 a2: array 'a) (l u: int) = M.permut_sub a1.elts a2.elts l u logic permut (a1 a2 : array 'a) = logic permut (a1 a2: array 'a) = a1.length = a2.length and M.permut_sub a1.elts a2.elts 0 a1.length end ... ...
 ... ... @@ -419,7 +419,7 @@ end = struct | Tarrow ([], c) -> c | v -> let ty = trans_type_v v in let ty = trans_type_v ~pure:true v in { c_result_type = v; c_effect = E.empty; c_pre = f_true; ... ... @@ -503,15 +503,12 @@ end = struct let print_pre fmt f = fprintf fmt "@[{ %a }@]" Pretty.print_fmla f and print_post fmt ((v,q), _) = fprintf fmt "@[{%a | %a}@]" Pretty.print_vs v Pretty.print_fmla q let print_post fmt ((v, q), el) = let print_exn_post fmt (l, (v, q)) = fprintf fmt "@[| %a %a->@ {%a}@]" print_ls l (print_option print_vs) v print_fmla q in fprintf fmt "@[{%a | %a}@ %a@]" print_vs v print_fmla q fprintf fmt "@[{%a | %a}@ %a@]" print_vsty v print_fmla q (print_list space print_exn_post) el let rec print_type_v fmt = function ... ...
 ... ... @@ -187,8 +187,8 @@ and specialize_type_c ~loc htv c = { dc_result_type = specialize_type_v ~policy:Region_ret ~loc htv c.c_result_type; dc_effect = specialize_effect ~loc htv c.c_effect; dc_pre = specialize_fmla ~loc htv c.c_pre; dc_post = specialize_post ~loc htv c.c_post; } dc_pre = specialize_fmla ~loc htv c.c_pre; dc_post = specialize_post ~loc htv c.c_post; } and specialize_binder ~loc htv v = let id = { ... ... @@ -282,9 +282,7 @@ let dueffect env e = e.Ptree.pe_raises; } let dpost uc (q, ql) = let dexn (id, l) = let s, _, _ = dexception uc id in s, l in let dexn (id, l) = let s, _, _ = dexception uc id in s, l in q, List.map dexn ql let add_local_top env x tyv = ... ... @@ -814,7 +812,7 @@ let post env ((ty, f), ql) = let v_result = create_vsymbol (id_fresh id_result) ty in Some v_result, Mstr.add id_result v_result env in (ls, (v, Denv.fmla env f)) ls, (v, Denv.fmla env f) in let ty = Denv.ty_of_dty ty in let v_result = create_vsymbol (id_fresh id_result) ty in ... ... @@ -825,7 +823,7 @@ let iterm env l = let t = dterm env.i_denv l in Denv.term env.i_pures t (* TODO: should we admit an instsance of a polymorphic order relation *) (* TODO: should we admit an instance of a polymorphic order relation? *) let ivariant env (t, ps) = let loc = t.pp_loc in let t = iterm env t in ... ... @@ -1029,6 +1027,39 @@ let ipattern env p = in ipattern env p (* pretty-printing (for debugging) *) open Pp open Pretty let print_iregion = R.print let rec print_iexpr fmt e = match e.iexpr_desc with | IElogic t -> print_term fmt t | IElocal v -> fprintf fmt "" print_vs v.i_impure | IEglobal ({ ps_kind = PSvar v }, _) -> fprintf fmt "" print_vs v.pv_effect | IEglobal ({ ps_kind = PSfun v } as ps, _) -> fprintf fmt "" print_ls ps.ps_impure T.print_type_v v | IEapply (e, v) -> fprintf fmt "@[((%a) %a)@]" print_iexpr e print_vs v.i_impure | IEapply_var (e, v) -> fprintf fmt "@[((%a) )@]" print_iexpr e print_vs v.i_impure | IEapply_glob (e, v) -> fprintf fmt "@[((%a) )@]" print_iexpr e print_vs v.pv_effect | IEfun (_, (_,e,_)) -> fprintf fmt "@[fun _ ->@ %a@]" print_iexpr e | IElet (v, e1, e2) -> fprintf fmt "@[let %a = %a in@ %a@]" print_vs v.i_impure print_iexpr e1 print_iexpr e2 | IEif (e1, e2, e3) -> fprintf fmt "@[if %a then %a else %a@]" print_iexpr e1 print_iexpr e2 print_iexpr e3 | _ -> fprintf fmt "" (* [iexpr] translates dexpr into iexpr [env : vsymbol Mstr.t] maps strings to vsymbols for local variables *) ... ... @@ -1212,39 +1243,6 @@ and itriple gl env (p, e, q) = let q = iupost env ty q in (p, e, q) (* pretty-printing (for debugging) *) open Pp open Pretty let print_iregion = R.print let rec print_iexpr fmt e = match e.iexpr_desc with | IElogic t -> print_term fmt t | IElocal v -> fprintf fmt "" print_vs v.i_impure | IEglobal ({ ps_kind = PSvar v }, _) -> fprintf fmt "" print_vs v.pv_effect | IEglobal ({ ps_kind = PSfun _ } as ps, _) -> fprintf fmt "" print_ls ps.ps_impure | IEapply (e, v) -> fprintf fmt "@[((%a) %a)@]" print_iexpr e print_vs v.i_impure | IEapply_var (e, v) -> fprintf fmt "@[((%a) )@]" print_iexpr e print_vs v.i_impure | IEapply_glob (e, v) -> fprintf fmt "@[((%a) )@]" print_iexpr e print_vs v.pv_effect | IEfun (_, (_,e,_)) -> fprintf fmt "@[fun _ ->@ %a@]" print_iexpr e | IElet (v, e1, e2) -> fprintf fmt "@[let %a = %a in@ %a@]" print_vs v.i_impure print_iexpr e1 print_iexpr e2 | IEif (e1, e2, e3) -> fprintf fmt "@[if %a then %a else %a@]" print_iexpr e1 print_iexpr e2 print_iexpr e3 | _ -> fprintf fmt "" (* phase 3: effect inference **********) let rec ty_effect ef ty = match ty.ty_node with ... ... @@ -1483,7 +1481,7 @@ and expr_desc gl env loc ty = function (* if Sreg.exists (fun r -> occur_type_v r e1.expr_type_v) vs.pv_regions then *) (* errorm ~loc "this application would create an alias"; *) let c = apply_type_v_var e1.expr_type_v vs in (* printf "c = %a@." print_type_c c; *) (* printf "c = %a@." print_type_c c; *) make_apply loc e1 ty c | IEapply_glob (e1, v) -> let e1 = expr gl env e1 in ... ...
 (** module M type pointer model int ... ... @@ -9,8 +11,8 @@ module M let foo () = f null end **) (*** module TestRef use import int.Int ... ... @@ -59,6 +61,7 @@ module Array end (** module TestArray use import int.Int ... ... @@ -72,6 +75,7 @@ module TestArray { x[1] = 2 and x.length = 2 } end **) module Q ... ... @@ -81,7 +85,6 @@ module Q end ***) (* Local Variables: ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!