From f82c19b38ac9cf26d24f54d63e3a4d22f88f250d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rio=20Pereira?= Date: Wed, 19 Jul 2017 16:55:38 +0200 Subject: [PATCH] cursor_examples.mlw moved to the gallery --- examples/cursor_examples.mlw | 262 +++++++++++++++++++++++ examples/to_port/cursor/why3session.xml | 52 ----- examples/to_port/cursor/why3shapes.gz | Bin 859 -> 0 bytes examples/to_port/cursor_examples.mlw | 272 ------------------------ modules/array.mlw | 6 +- modules/cursor.mlw | 15 +- src/mlw/pmodule.ml | 4 +- theories/int.why | 7 + 8 files changed, 281 insertions(+), 337 deletions(-) create mode 100644 examples/cursor_examples.mlw delete mode 100644 examples/to_port/cursor/why3session.xml delete mode 100644 examples/to_port/cursor/why3shapes.gz delete mode 100644 examples/to_port/cursor_examples.mlw diff --git a/examples/cursor_examples.mlw b/examples/cursor_examples.mlw new file mode 100644 index 000000000..7c2e12886 --- /dev/null +++ b/examples/cursor_examples.mlw @@ -0,0 +1,262 @@ + +(** Cursors + + TO BE DISCUSSED + - a [coherent] predicate is also convenient for an immutable collection + - having [next] raising an exception imposes a try-with around the loop + it is simpler to have [next] with a precondition together with + an operation [has_next] + + QUESTION: in IntListCursor, field to_do is no more ghost; will it be + allowed by refinement? otherwise, simply add a non-ghost field + identical to to_do +*) + +module TestCursor + + use import int.Int + use import int.Sum + use import seq.Seq + use import ref.Refint + + use import cursor.Cursor + + (** sums all the remaining elements in the cursor *) + let sum (c: cursor int) : int + requires { permitted c } + requires { c.visited = empty } + ensures { result = sum (get c.visited) 0 (length c.visited) } + diverges + = let s = ref 0 in + while has_next c do + invariant { permitted c } + invariant { !s = sum (get c.visited) 0 (length c.visited) } + let x = next c in + s += x + done; + !s + +end + +(** {2 Iteration over an immuable collection} + + here we choose a list *) + +module ListCursorImpl (* : ListCursor *) + + use import int.Int + use import list.List + use import seq.Seq + use import seq.OfList + + type cursor 'a = { + mutable ghost visited : seq 'a; + ghost collection : list 'a; + mutable to_visit : list 'a; + } invariant { visited ++ to_visit = collection } + by { visited = empty; collection = Nil; to_visit = Nil } + + predicate permitted (c: cursor 'a) = + length c.visited <= length c.collection /\ + forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i] + + predicate complete (c: cursor 'a) = + length c.visited = length c.collection + + let lemma snoc_Cons (s: seq 'a) (l: list 'a) (x: 'a) + ensures { snoc s x ++ l == s ++ Cons x l } + = () + + let next (c: cursor 'a) : 'a + requires { not (complete c) } + writes { c } + ensures { c.visited = snoc (old c).visited result } + ensures { match (old c).to_visit with + | Nil -> false + | Cons x r -> c.to_visit = r /\ x = result + end } + = match c.to_visit with + | Nil -> absurd + | Cons x r -> + let ghost v0 = c.visited in + c.visited <- snoc c.visited x; c.to_visit <- r; + snoc_Cons v0 r x; + assert { c.to_visit == c.collection [length c.visited ..] }; + x + end + + let has_next (c: cursor 'a) : bool + ensures { result <-> not (complete c) } + = match c.to_visit with (* could define a [val eq (l1 l2: list 'a) : bool] *) + | Nil -> false + | _ -> true + end + + let create (t: list 'a) : cursor 'a + ensures { result.visited = empty } + ensures { result.collection = t } + ensures { result.to_visit = t } + = { visited = empty; collection = t; to_visit = t } + + clone cursor.ListCursor with + type cursor = cursor, + val create = create, + val C.has_next = has_next, + val C.next = next + +end + +module TestListCursor + + use import int.Int + use import int.Sum as S + use import list.List + use import list.Length + use import list.Sum + use import ref.Refint + use import seq.Seq + use import seq.OfList + + clone import cursor.ListCursor + + lemma sum_of_list: forall l: list int. + sum l = S.sum (get (of_list l)) 0 (length l) + + let list_sum (l: list int) : int + ensures { result = sum l } + = let s = ref 0 in + let c = create l in + while C.has_next c do + invariant { !s = S.sum (get c.visited) 0 (length c.visited) } + invariant { permitted c } + variant { length l - length c.visited } + let x = C.next c in + s += x + done; + !s + +end + +module TestListCursorLink + + use import ListCursorImpl + + clone import TestListCursor with + type ListCursor.cursor = cursor, + val ListCursor.C.next = next, + val ListCursor.C.has_next = has_next, + val ListCursor.create = create + +end + +(** {2 Iteration over a mutable collection} + + here we choose an array of integers *) + +module ArrayCursorImpl (* : ArrayCursor *) + + use import int.Int + use import array.Array + use import array.ToSeq + use import list.List + use import list.Reverse + use import array.ToList + use import seq.Seq + + type cursor 'a = { + mutable ghost visited : seq 'a; + collection : seq 'a; (* FIXME : extraction of seq *) + mutable index : int; (** index of next element *) + } invariant { 0 <= index <= length collection /\ + index = length visited /\ + forall i. 0 <= i < index -> collection[i] = visited[i] } + by { visited = empty; collection = empty; index = 0 } + + predicate permitted (c: cursor 'a) = + length c.visited <= length c.collection /\ + forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i] + + predicate complete (c: cursor 'a) = + length c.visited = length c.collection + + let create (a: array 'a) : cursor 'a + ensures { result.visited = empty } + ensures { result.index = 0 } + ensures { result.collection = to_seq a } + = { visited = empty; collection = to_seq a; index = 0; } + + let has_next (c: cursor 'a) : bool + ensures { result <-> not (complete c) } + = c.index < length c.collection + + let next (c: cursor 'a) : 'a + requires { not (complete c) } + writes { c } + ensures { c.visited = snoc (old c).visited result } + ensures { c.index = (old c).index + 1 } + = if c.index >= length c.collection then absurd + else begin let x = c.collection[c.index] in + c.visited <- snoc c.visited x; + c.index <- c.index + 1; + x end + + clone cursor.ArrayCursor with + type cursor = cursor, + val C.next = next, + val C.has_next = has_next, + val create = create + +end + +module TestArrayCursor + + use import int.Int + use import array.Array + use import array.ToSeq + use import seq.Seq + use import int.Sum + use import ref.Refint + + clone import cursor.ArrayCursor + + let array_sum (a: array int) : int + ensures { result = sum (Array.([]) a) 0 (length a) } + = let s = ref 0 in + let c = create a in + while C.has_next c do + invariant { !s = sum (get c.visited) 0 (length c.visited) } + invariant { permitted c } + variant { length c.collection - length c.visited } + let x = C.next c in + s += x + done; + !s + + let harness1 () : unit + = let a = Array.make 42 0 in + let c = create a in + let x = C.next c in + assert { x = 0 } + +(* + let harness2 () : unit + = let a = Array.make 42 0 in + let c = create a in + a[1] <- 17; + let x = C.next c in + assert { x = 0 } +*) + +end + +module TestArrayCursorLink + + use import ArrayCursorImpl + + clone import TestArrayCursor with + type ArrayCursor.cursor = cursor, + val ArrayCursor.C.next = next, + val ArrayCursor.C.has_next = has_next, + val ArrayCursor.create = create + +end \ No newline at end of file diff --git a/examples/to_port/cursor/why3session.xml b/examples/to_port/cursor/why3session.xml deleted file mode 100644 index 64e225a78..000000000 --- a/examples/to_port/cursor/why3session.xml +++ /dev/null @@ -1,52 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/examples/to_port/cursor/why3shapes.gz b/examples/to_port/cursor/why3shapes.gz deleted file mode 100644 index 733b83b6d0859af7da84d69b18e1f549c4849c62..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 859 zcmV-h1El;PiwFP!00000|D{$-Ya=-jzW1-lJusBs5+txDU@#1GT69^4P%23?4SrUw#1b+MWN!S!P2TNq4$qq& z`)%%DZtgwDvVGnCktXpZnEt)=%4__RhVg%ifA@!eNYM)dT&L}q;cFGms@>12X5bm~ zj32chS5?2c)NdB}l=ho`D4Qzuuxjj{R=1veyIj@l9T>+|mLg}TLf4if{ zhu!ut8E7nwXC6vcUKM*bpLv+AjUSib*s^mn2*wR%tF^K!Mk|s{%9Lfu!p6zwHoXiF zd35viJA=ivmy0>lQ{W{9o|%&sKgpopnout}8~vU4;APDMQ_a0a6-%VudYx$KciZz5 zQOz$dupjl!n25Tp&fmA^oBm}K{`L6b!{;t%Oj0@{xKqeO$P{(Z860FMbfyWUuXuPI zf%;Tj+&rz*kZNeH*YIt2TH>Gk=d^lg1WQ~W(iz65OaIJBE-Ol+T39qS*&1sQsv5fD z5QLbKCBs!I6Dt%MnJBU>9U3`Pd7p4dZxhVhbT-ELwKVe+?^nZOSpA+N&uTE09t{W1 z$kE7WYVhSXYRs93y6RXkh6f!KfHg$Su?$9`)s{J>!M=x3!_KRu{|*}L9W=hDs11HT zI*Yu~bHC7OUe{9k=DY3NFujg;7a#ALtS2aD&Lm5Jx2eglQ?fL z8i_33{l|UeQh!q+re3Sj>+2pDQcZ?eSMPQ~@hm}V8;k-|>L)TAa{^hi;Sk~1Tfq-+ zoS1TnI=oZm|Gy;!FvwAJCNrbRZAvf+Fpm}$ c.visited[i] = c.collection[i] - - predicate complete (c: cursor 'a) = - length c.visited = length c.collection - - let lemma snoc_Cons (s: seq 'a) (l: list 'a) (x: 'a) - ensures { snoc s x ++ l == s ++ Cons x l } - = () - - let next (c: cursor 'a) : 'a - requires { not (complete c) } - writes { c } - ensures { c.visited = snoc (old c).visited result } - ensures { match (old c).to_visit with - | Nil -> false - | Cons x r -> c.to_visit = r /\ x = result - end } - = match c.to_visit with - | Nil -> absurd - | Cons x r -> - let ghost v0 = c.visited in - c.visited <- snoc c.visited x; c.to_visit <- r; - snoc_Cons v0 r x; - assert { c.to_visit == c.collection [length c.visited ..] }; - x - end - - let has_next (c: cursor 'a) : bool - ensures { result <-> not (complete c) } - = match c.to_visit with (* could define a [val eq (l1 l2: list 'a) : bool] *) - | Nil -> false - | _ -> true - end - - let create (t: list 'a) : cursor 'a - ensures { result.visited = empty } - ensures { result.collection = t } - ensures { result.to_visit = t } - = { visited = empty; collection = t; to_visit = t } - - clone cursor.ListCursor with - type cursor = cursor, - val create = create, - val C.has_next = has_next, - val C.next = next - -end - -module TestListCursor - - use import int.Int - use import int.Sum as S - use import list.List - use import list.Length - use import list.Sum - use import ref.Refint - use import seq.Seq - use import seq.OfList - use import cursor.ListCursor - - let lemma aux2 (f g: int -> int) (a b c d: int) - requires { b - a = d - c } - requires { forall i. a <= i < b -> f i = g i } - ensures { S.sum f a b = S.sum g a b } - = () - - let lemma aux (s: seq int) (x: int) - ensures { let ss = cons x s in - S.sum (get ss) 0 (length ss) = x + S.sum (get s) 0 (length s) } - = let ss = cons x s in - assert { forall i. 0 <= i < length s -> get s i = get ss (i+1) } - - lemma sum_of_list: forall l: list int. - sum l = S.sum (get (of_list l)) 0 (length l) - - let list_sum (l: list int) : int - ensures { result = sum l } - = let s = ref 0 in - let c = create l in - while C.has_next c do - invariant { !s = S.sum (get c.visited) 0 (length c.visited) } - invariant { permitted c } - variant { length l - length c.visited } - let x = C.next c in - s += x - done; - !s - -end - -(** {2 Iteration over a mutable collection} - - here we choose an array of integers *) - -(* module IntArrayCursor (\* : IterableList *\) *) - -(* use import int.Int *) -(* use import array.Array *) -(* use import list.List *) -(* use import list.Reverse *) -(* use import array.ToList *) -(* use import seq.Seq *) - -(* type t 'a = array 'a *) - -(* val ghost constant a : {array 'a} *) -(* ensures { Array.length result = 0 } *) - -(* type cursor 'a = { *) -(* mutable ghost visited: seq 'a; *) -(* ghost collection: {t 'a}; *) -(* mutable index: int; (\** index of next element *\) *) -(* } invariant { 0 <= index <= Array.length collection /\ *) -(* index = length visited /\ *) -(* forall i. 0 <= i < index -> *) -(* Array.([]) collection i = visited[i] } *) -(* by { visited = empty; collection = a; index = 0 } *) - -(* clone import cursor.Cursor with *) -(* type cursor = cursor, *) -(* type t = t *) - -(* (\* predicate permitted (v: seq int) (t: t) = *\) *) -(* (\* length v <= length t /\ *\) *) -(* (\* forall i. 0 <= i *\) *) - -(* (\* let create (t: t) : cursor *\) *) -(* (\* ensures { result.done_ = Nil } *\) *) -(* (\* ensures { coherent t result } *\) *) -(* (\* = *\) *) -(* (\* { done_ = Nil; to_do = to_list t 0 (length t); index = 0; } *\) *) - -(* (\* let has_next (t: t) (c: cursor) : bool *\) *) -(* (\* requires { coherent t c } *\) *) -(* (\* ensures { result <-> c.to_do <> Nil } *\) *) -(* (\* = *\) *) -(* (\* c.index < length t *\) *) - -(* (\* let rec lemma reverse_cons (a: array int) (l u: int) *\) *) -(* (\* requires { l <= u } *\) *) -(* (\* ensures { reverse (to_list a l (u+1)) = *\) *) -(* (\* Cons a[u] (reverse (to_list a l u)) } *\) *) -(* (\* variant { u - l } *\) *) -(* (\* = if l < u then reverse_cons a (l+1) u *\) *) - -(* (\* let next (t: t) (c: cursor) : elt *\) *) -(* (\* requires { c.to_do <> Nil } *\) *) -(* (\* requires { coherent t c } *\) *) -(* (\* writes { c } *\) *) -(* (\* ensures { match old c.to_do with *\) *) -(* (\* | Nil -> false *\) *) -(* (\* | Cons x l -> result = x /\ c.done_ = Cons x (old c.done_) /\ *\) *) -(* (\* c.to_do = l end } *\) *) -(* (\* ensures { coherent t c } *\) *) -(* (\* = *\) *) -(* (\* match c.to_do with *\) *) -(* (\* | Nil -> absurd *\) *) -(* (\* | Cons x r -> c.to_do <- r; c.done_ <- Cons x c.done_ *\) *) -(* (\* end; *\) *) -(* (\* let x = t[c.index] in *\) *) -(* (\* c.index <- c.index + 1; *\) *) -(* (\* x *\) *) - -(* end *) - -(* module TestArrayCursor *) - -(* use import int.Int *) -(* use list.Sum as L *) -(* use list.Length as LL *) -(* use import array.Array *) -(* use import array.ArraySum *) -(* use import array.ToList *) -(* use import ref.Refint *) -(* use import IntArrayCursor *) - -(* let rec lemma array_sum_array_to_list (a: array int) (l u: int) : unit *) -(* ensures { sum a l u = L.sum (to_list a l u) } variant { u-l } *) -(* = if l < u then array_sum_array_to_list a (l+1) u *) - -(* let array_sum (a: array int) : int *) -(* ensures { result = sum a 0 (length a) } *) -(* = *) -(* let s = ref 0 in *) -(* let c = create a in *) -(* while has_next a c do *) -(* invariant { sum a 0 (length a) = !s + L.sum c.to_do } *) -(* invariant { coherent a c } *) -(* variant { LL.length c.to_do } *) -(* let x = next a c in *) -(* s += x *) -(* done; *) -(* !s *) - -(* let harness1 () : unit *) -(* = *) -(* let a = Array.make 42 0 in *) -(* let c = create a in *) -(* let x = next a c in *) -(* assert { x = 0 } *) - -(* (\* *) -(* let harness2 () : unit *) -(* = *) -(* let a = Array.make 42 0 in *) -(* let c = create a in *) -(* a[1] <- 17; *) -(* let x = next a c in *) -(* assert { x = 0 } *) -(* *\) *) - -(* end *) diff --git a/modules/array.mlw b/modules/array.mlw index eda3e7a17..b2927ba74 100644 --- a/modules/array.mlw +++ b/modules/array.mlw @@ -339,15 +339,13 @@ module ToSeq variant { u - l } = if u <= l then S.empty else S.cons a[l] (to_seq_sub a (l+1) u) - let rec lemma to_seq_length - (a: array 'a) (l u: int) + let rec lemma to_seq_length (a: array 'a) (l u: int) requires { 0 <= l <= u <= length a } variant { u - l } ensures { S.length (to_seq_sub a l u) = u - l } = if l < u then to_seq_length a (l+1) u - let rec lemma to_seq_nth - (a: array 'a) (l i u: int) + let rec lemma to_seq_nth (a: array 'a) (l i u: int) requires { 0 <= l <= i < u <= length a } variant { i - l } ensures { S.get (to_seq_sub a l u) (i - l) = a[i] } diff --git a/modules/cursor.mlw b/modules/cursor.mlw index 9b4762127..41dd879e4 100644 --- a/modules/cursor.mlw +++ b/modules/cursor.mlw @@ -56,29 +56,30 @@ module ListCursor end -module CursorArray +module ArrayCursor use import array.Array + use import array.ToSeq use import seq.Seq use import seq.OfList use import int.Int type cursor 'a = private { - ghost mutable visited : seq 'a; - ghost array : array 'a; + ghost mutable visited : seq 'a; + ghost collection : seq 'a; } predicate permitted (c: cursor 'a) = - length c.visited <= Array.length c.array /\ - forall i. 0 <= i < length c.visited -> c.visited[i] = Array.([]) c.array i + length c.visited <= length c.collection /\ + forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i] predicate complete (c: cursor 'a) = - length c.visited = Array.length c.array + length c.visited = length c.collection val create (a: array 'a) : cursor 'a ensures { permitted result } ensures { result.visited = empty } - ensures { result.array = a } + ensures { result.collection = to_seq a } clone import Cursor as C with type cursor = cursor, diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml index a8aadd6a6..408d18309 100644 --- a/src/mlw/pmodule.ml +++ b/src/mlw/pmodule.ml @@ -864,8 +864,8 @@ let clone_type_record cl s d s' d' = let pj_str = pj.pv_vs.vs_name.id_string in let pj_ity = clone_ity cl pj.pv_ity in let pj_ght = pj.pv_ghost in - let rs' = try Hstr.find fields' pj_str - with Not_found -> raise (BadInstance id) in + let rs' = try Hstr.find fields' pj_str with Not_found -> + raise (BadInstance id) in let pj' = fd_of_rs rs' in let pj'_ity = pj'.pv_ity in let pj'_ght = pj'.pv_ghost in diff --git a/theories/int.why b/theories/int.why index 671b0f8ea..b286034b5 100644 --- a/theories/int.why +++ b/theories/int.why @@ -416,6 +416,13 @@ theory Sum forall f: int -> int, a b c: int. a <= b <= c -> sum f a c = sum f a b + sum f b c + let rec lemma shift_left (f g: int -> int) (a b c d: int) + requires { b - a = d - c } + requires { forall i. a <= i < b -> f i = g (c + i - a) } + variant { b - a } + ensures { sum f a b = sum g c d } + = if a < b then shift_left f g (a+1) b (c+1) d + end (** {2 Factorial function} *) -- GitLab