Skip to content

GitLab

why3
why3
Commit f82c19b3 authored by Mário Pereira's avatar Mário Pereira
Browse files
Options

cursor_examples.mlw moved to the gallery

parent c9b80a74
Show whitespace changes
Inline Side-by-side
Showing with 281 additions and 65 deletions
examples/to_port/cursor_examples.mlw → examples/cursor_examples.mlw
View file @ f82c19b3
......@@ -42,7 +42,7 @@ end
here we choose a list *)
module ListCursorImpl (* : IterableList *)
module ListCursorImpl (* : ListCursor *)
use import int.Int
use import list.List
......@@ -116,19 +116,8 @@ module TestListCursor
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) }
clone import cursor.ListCursor
lemma sum_of_list: forall l: list int.
sum l = S.sum (get (of_list l)) 0 (length l)
......@@ -148,125 +137,126 @@ module TestListCursor
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 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 *)
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
examples/to_port/cursor/why3session.xml deleted 100644 → 0
View file @ c9b80a74
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../cursor.mlw">
<theory name="TestCursor" sum="401d4ce6900374ae25d5039a681f2923">
<goal name="VC sum" expl="VC for sum">
<proof prover="0"><result status="valid" time="1.00" steps="461"/></proof>
</goal>
</theory>
<theory name="ListCursor" sum="98ec1f1e0527eca4c14a2ff349314fb9">
<goal name="VC cursor" expl="VC for cursor">
<proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
</goal>
<goal name="VC snoc_Cons" expl="VC for snoc_Cons">
<proof prover="0"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="VC next" expl="VC for next">
<proof prover="0"><result status="valid" time="0.23" steps="465"/></proof>
</goal>
<goal name="VC has_next" expl="VC for has_next">
<proof prover="0"><result status="valid" time="0.03" steps="66"/></proof>
</goal>
<goal name="VC create" expl="VC for create">
<proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
</goal>
<goal name="Cursor.VC create" expl="VC for create">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="Cursor.VC next" expl="VC for next">
<proof prover="0"><result status="valid" time="0.02" steps="55"/></proof>
</goal>
<goal name="Cursor.VC has_next" expl="VC for has_next">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
</theory>
<theory name="TestListCursor" sum="912c61d8c8a3a20497d6a0b557c300d1">
<goal name="VC list_sum" expl="VC for list_sum">
<proof prover="0"><result status="valid" time="2.58" steps="1648"/></proof>
</goal>
</theory>
<theory name="IntArrayCursor" sum="4c9dca290af968fc2d686a13d791aecc">
<goal name="VC a" expl="VC for a">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="VC cursor" expl="VC for cursor">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
</file>
</why3session>
modules/array.mlw
View file @ f82c19b3
......@@ -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] }
......
modules/cursor.mlw
View file @ f82c19b3
......@@ -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 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,
......
src/mlw/pmodule.ml
View file @ f82c19b3
......@@ -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
......
theories/int.why
View file @ f82c19b3
......@@ -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} *)
......
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