why3doc index index
(* BactrackArray.mlw : provide support for a backtracking table. Idea : you have an infinite number of stack,initially empty, and you add elements with time. Moreover, you sometime need to undo some events. Primitive: 1) create () : t 'a : create an initially empty table. 2) add (i:int) (b:'a) (tb:t 'a) : unit : add an element b on a stack top i, and advance the time counter. 3) get (i:int) (tb:t 'a) : list 'a : get the stack i at the current time. 4) stamp (tb:t 'a) : timestamp 'a : current timestamp. 5) backtrack (t:timestamp) (tb:t 'a) : unit : If the instant t is a past instant or the current instant, go back to the instant t. *) module Types use int.Int use array.Array use list.List use Functions.Func use Predicates.Pred type timestamp 'a = { time : int ; size : int ; ghost table : int -> list 'a ; } type t 'a = { (* (-1) mean array resizing (doubling in size), i >= 0 mean update at case i. *) mutable history : list int ; mutable current_time : int ; mutable buffer : array (list 'a) ; (* Invariant of stored data. *) ghost inv : 'a -> bool ; } end module Logic use Types use int.Int use int.ComputerDivision use import map.Map as M use array.Array use list.List use Functions.Func use Choice.Choice function func_of_array (a:array 'a) (def:'a) : int -> 'a axiom func_of_array_def : forall a:array 'a,def:'a,x:int. func_of_array a def x = if (0 <= x < a.length) then M.get a.elts x else def function current_timestamp (x:t 'a) : timestamp 'a = { time = x.current_time ; size = x.buffer.length ; table = func_of_array x.buffer Nil ; } predicate correct_table (sz:int) (b: int -> list 'a) = forall x:int. x >= sz \/ x < 0 -> b x = Nil function pop (l:list 'a) : list 'a = match l with | Nil -> default | Cons _x q -> q end function unroll (tm:int) (t0:int) (h:list int) (b:int -> list 'a) (sz:int) : timestamp 'a = if tm = 0 then { time = t0 ; size = sz ; table = b } else match h with | Nil -> { time = (t0+tm) ; size = sz ; table = b ; } | Cons x q -> if x = (-1) then unroll (tm-1) t0 q b (div sz 2) else unroll (tm-1) t0 q (b[x <- pop (b x)]) sz end predicate unroll_correct (tm:int) (h:list int) (b:int -> list 'a) (sz:int) = match h with | Nil -> tm = 0 | Cons x q -> if x = (-1) then let s0 = div sz 2 in s0 * 2 = sz /\ unroll_correct (tm-1) q b s0 /\ (forall i:int. i >= s0 \/ i < 0 -> b i = Nil) else b x <> Nil /\ 0 <= x < sz /\ unroll_correct (tm-1) q (b[x <- pop (b x)]) sz end predicate past_time (t:timestamp 'a) (tb:t 'a) = tb.current_time >= t.time /\ unroll (tb.current_time - t.time) t.time tb.history (func_of_array tb.buffer Nil) tb.buffer.length = t predicate precede (tb1:t 'a) (tb2:t 'a) = forall t:timestamp 'a. past_time t tb1 -> past_time t tb2 predicate before (t1 t2:timestamp 'a) = t1.time <= t2.time predicate list_forall (p:'a -> bool) (l:list 'a) = match l with | Nil -> true | Cons x q -> p x /\ list_forall p q end predicate correct (tb:t 'a) = (forall t:timestamp 'a. past_time t tb -> t.size > 0) /\ (forall t:timestamp 'a,i:int. past_time t tb /\ i >= 0 -> list_forall tb.inv (eval t.table i)) /\ (forall t:timestamp 'a. past_time t tb -> correct_table t.size t.table) /\ unroll_correct tb.current_time tb.history (func_of_array tb.buffer Nil) tb.buffer.length (* I MUST INTRODUCE THIS PREDICATE FOR ONLY ONE REASON : ABUSIVE RECORD DECONSTRUCTION IN ASSERTIONS. *) predicate backtrack_to (tbold:t 'a) (tbinter:t 'a) (tbnew:t 'a) = (forall tm:timestamp 'a. past_time tm tbold -> past_time tm tbinter && time tm <= time (current_timestamp tbold) && time tm <= time (current_timestamp tbnew) && before tm (current_timestamp tbnew) && past_time tm tbnew) && (forall tm:timestamp 'a. past_time tm tbold -> past_time tm tbnew) && precede tbold tbnew end module Impl use Types use Logic use int.Int use int.ComputerDivision use import map.Map as M use array.Array use list.List use Functions.Func use Predicates.Pred use Choice.Choice (* extraction trick to speedup integer operations with constants. *) let constant mone : int = -1 let constant zero : int = 0 let constant one : int = 1 let constant two : int = 2 let create (ghost p: 'a -> bool) : t 'a ensures { forall t:timestamp 'a. past_time t result -> t.table = const Nil } ensures { past_time (current_timestamp result) result } ensures { result.inv = p } ensures { correct result } = let res = { history = Nil ; current_time = zero ; buffer = make one Nil ; inv = p ; } in assert { extensionalEqual (func_of_array res.buffer Nil) (const Nil) } ; res (* Internal utility (break some of the invariants), but useful in practice. *) let add_event (x:int) (tb:t 'a) : unit writes { tb.history,tb.current_time } ensures { tb.history = Cons x (old tb).history } ensures { tb.current_time = (old tb).current_time + 1 } = tb.history <- Cons x tb.history ; tb.current_time <- tb.current_time + one (* Internal utility. *) let resize_for (x:int) (tb:t 'a) : unit writes { tb } requires { correct tb } requires { x >= tb.buffer.length } ensures { x < tb.buffer.length } ensures { precede (old tb) tb } ensures { correct tb } ensures { (current_timestamp tb).table = (current_timestamp (old tb)).table } = (* pattern : in order to do an optimization (resize only once), introduce a ghost value on which we 'execute' the unoptimized code and 'check' at end that it give the same result. *) let ghost tbc = { history = tb.history ; current_time = tb.current_time ; buffer = copy tb.buffer; inv = tb.inv ; } in let rec aux (size:int) : int requires { 0 < size <= x } requires { correct tbc } requires { tbc.history = tb.history /\ tbc.current_time = tb.current_time /\ func_of_array tbc.buffer Nil = func_of_array tb.buffer Nil } requires { tbc.buffer.length = size } variant { x - size } writes { tb.history,tb.current_time,tbc.history,tbc.current_time,tbc.buffer } ensures { correct tbc } ensures { tbc.history = tb.history /\ tbc.current_time = tb.current_time /\ func_of_array tbc.buffer Nil = func_of_array tb.buffer Nil } ensures { tbc.buffer.length = result } ensures { result > x } ensures { result >= size } ensures { precede (old tbc) tbc } = label AuxInit in assert { past_time (current_timestamp tbc) tbc } ; add_event mone tb ; add_event mone tbc ; let size2 = two * size in let ghost buf2 = make size2 Nil in let buf1 = tbc.buffer in blit buf1 zero buf2 zero size ; tbc.buffer <- buf2 ; assert { extensionalEqual (func_of_array tbc.buffer Nil) (func_of_array (tbc at AuxInit).buffer Nil) } ; assert { forall t:timestamp 'a. (past_time t (tbc at AuxInit) \/ t = current_timestamp tbc) <-> past_time t tbc } ; if size2 > x then size2 else aux size2 in let len = length tb.buffer in assert { extensionalEqual (func_of_array tbc.buffer Nil) (func_of_array tb.buffer Nil) } ; assert { len = (current_timestamp tb).size } ; let size = aux len in let buf2 = make size Nil in let buf1 = tb.buffer in blit buf1 zero buf2 zero len ; assert { extensionalEqual (func_of_array buf1 Nil) (func_of_array buf2 Nil) } ; tb.buffer <- buf2 let iadd (x:int) (b:'a) (tb:t 'a) : unit writes { tb.history,tb.current_time,tb.buffer.elts } requires { 0 <= x < tb.buffer.length } requires { correct tb } requires { inv tb b } ensures { past_time (current_timestamp tb) tb } ensures { correct tb } ensures { precede (old tb) tb } ensures { let tb0 = (current_timestamp (old tb)).table in (current_timestamp tb).table = tb0[x <- Cons b (tb0 x)] } = label Init in let buf = tb.buffer in buf[x]<- Cons b (buf[x]) ; add_event x tb ; assert { let tb0 = (current_timestamp (tb at Init)).table in extensionalEqual ((current_timestamp tb).table) (tb0[x <- Cons b (tb0 x)]) } ; assert { let tb0 = (current_timestamp (tb at Init)).table in let tb1 = (current_timestamp tb).table in extensionalEqual (tb1[x <- pop (tb1 x)]) tb0 } ; assert { past_time (current_timestamp tb) tb } ; assert { forall t:timestamp 'a. past_time t tb <-> past_time t (tb at Init) \/ t = current_timestamp tb } ; assert { precede (tb at Init) tb } let add (x:int) (b:'a) (tb:t 'a) : unit writes { tb } requires { correct tb } requires { x >= 0 } requires { inv tb b } ensures { past_time (current_timestamp tb) tb } ensures { correct tb } ensures { precede (old tb) tb } ensures { let tb0 = (current_timestamp (old tb)).table in (current_timestamp tb).table = tb0[x <- Cons b (tb0 x)] } = if x >= length tb.buffer then resize_for x tb ; iadd x b tb let get (tb:t 'a) (x:int) : list 'a requires { correct tb } requires { x >= 0 } ensures { result = table (current_timestamp tb) x } ensures { list_forall tb.inv result } = if x >= length tb.buffer then Nil else let res = tb.buffer[x] in (assert { res = table (current_timestamp tb) x } ; res ) let backtrack (t:timestamp 'a) (tb:t 'a) : unit writes { tb } requires { past_time t tb } requires { correct tb } ensures { correct tb } ensures { current_timestamp tb = t } ensures { past_time (current_timestamp tb) tb } ensures { forall t2:timestamp 'a. before t2 t /\ past_time t2 (old tb) -> past_time t2 tb } ensures { precede tb (old tb) } = let final_size = t.size in let ghost tbc = { history = tb.history ; current_time = tb.current_time ; buffer = copy tb.buffer ; inv = tb.inv ; } in let rec unroll (delta:int) : unit requires { correct tbc } requires { past_time t tbc } requires { delta >= 0 } requires { tbc.current_time = t.time + delta } requires { tbc.history = tb.history /\ (forall x:int. 0 <= x < final_size /\ x < tbc.buffer.length -> func_of_array tbc.buffer Nil x = func_of_array tb.buffer Nil x) } requires { tb.buffer.length <= final_size } variant { delta } writes { tb.history,tb.buffer.elts,tbc } ensures { correct tbc } ensures { tbc.history = tb.history /\ (forall x:int. 0 <= x < final_size -> func_of_array tbc.buffer Nil x = func_of_array tb.buffer Nil x) } ensures { current_timestamp tbc = t } (* This is a trick avoiding an inductive reasoning outside. *) ensures { tbc.buffer.length <= (old tbc).buffer.length } ensures { precede tbc (old tbc) } ensures { forall t2:timestamp 'a. before t2 t /\ past_time t2 (old tbc) -> past_time t2 tbc } = label UInit in if delta <> zero then begin match tb.history with | Nil -> absurd | Cons x q -> tb.history <- q ; tbc.history <- q ; tbc.current_time <- tbc.current_time - one ; if x = mone then begin let buf1 = tbc.buffer in let len = length buf1 in let len2 = div len two in (* nothing to do on non-ghost side. *) let buf2 = make len2 Nil in blit buf1 zero buf2 zero len2 ; tbc.buffer <- buf2 ; assert { let t0 = { time = tbc.current_time ; size = len2 ; table = func_of_array (tbc at UInit).buffer Nil } in let t1 = { t0 with table = func_of_array tbc.buffer Nil } in past_time t0 (tbc at UInit) && extensionalEqual t0.table t1.table && t0 = t1 } ; assert { extensionalEqual (func_of_array tbc.buffer Nil) (func_of_array (tbc at UInit).buffer Nil) } ; assert { precede tbc (tbc at UInit) } ; unroll (delta - one) end else begin assert { 0 <= x < tbc.buffer.length } ; if x < final_size then begin let h = tb.buffer[x] in match h with | Nil -> absurd | Cons _ q -> tb.buffer[x]<- q ; tbc.buffer[x]<- q ; assert { let tb0 = func_of_array (tbc at UInit).buffer Nil in extensionalEqual (tb0[x <- pop (tb0 x)]) (func_of_array tbc.buffer Nil) } ; assert { precede tbc (tbc at UInit) } ; unroll (delta - one) end end else begin let hc = tbc.buffer[x] in match hc with | Nil -> absurd | Cons _ q -> tbc.buffer[x]<- q end ; assert { let tb0 = func_of_array (tbc at UInit).buffer Nil in extensionalEqual (tb0[x <- pop (tb0 x)]) (func_of_array tbc.buffer Nil) } ; assert { precede tbc (tbc at UInit) } ; (* nothing to do on non-ghost side. *) unroll (delta - one) end end end end in assert { extensionalEqual (func_of_array tb.buffer Nil) (func_of_array tbc.buffer Nil) } ; (* direct resizing if necessary. *) if final_size < length tb.buffer then begin let buf2 = make final_size Nil in let buf1 = tb.buffer in blit buf1 zero buf2 zero final_size ; tb.buffer <- buf2 end ; let tm0 = tb.current_time in tb.current_time <- t.time ; unroll (tm0 - t.time) ; assert { extensionalEqual (func_of_array tb.buffer Nil) (func_of_array tbc.buffer Nil) } val ghost hack_func_of_array (a:array 'a) (def:'a) : int -> 'a ensures { result = func_of_array a def } let stamp (tb:t 'a) : timestamp 'a requires { correct tb } ensures { result = current_timestamp tb } = { time = tb.current_time ; size = length tb.buffer ; table = hack_func_of_array tb.buffer Nil ; } (* look for the correct syntax : meta "remove_program" val hack_func_of_array*) end
Generated by why3doc 1.7.0