Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
106
Issues
106
List
Boards
Labels
Milestones
Merge Requests
14
Merge Requests
14
Packages
Packages
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
7990ef5e
Commit
7990ef5e
authored
Jun 13, 2018
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Translate some examples to new syntax.
parent
fee45607
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
51 additions
and
51 deletions
+51
-51
examples/verifythis_2016_tree_traversal.mlw
examples/verifythis_2016_tree_traversal.mlw
+33
-33
examples/verifythis_fm2012_LRS.mlw
examples/verifythis_fm2012_LRS.mlw
+18
-18
No files found.
examples/verifythis_2016_tree_traversal.mlw
View file @
7990ef5e
...
...
@@ -62,7 +62,7 @@ who entered the competition.
module Memory
use import map.Map
(**
[loc]
is the type of memory locations (e.g pointers) *)
(**
`loc`
is the type of memory locations (e.g pointers) *)
type loc
val predicate eq (x y:loc) ensures { result <-> x = y }
(** Kinds of pointer fields. *)
...
...
@@ -73,9 +73,9 @@ module Memory
mutable accessor : pmem;
mutable mark : map loc bool;
}
(**
[memo]
represent memory. *)
(**
`memo`
represent memory. *)
val memo : memory
(** the memory model has a
[null]
pointer. *)
(** the memory model has a
`null`
pointer. *)
constant null : loc
val null () : loc ensures { result = null }
val is_null (l:loc) : bool ensures { result <-> l = null }
...
...
@@ -116,7 +116,7 @@ module Memory
end
(** In module
[TreeShape]
we describe the correlation between
(** In module
`TreeShape`
we describe the correlation between
the memory and the binary tree model. We also gives
elements of the algorithm specification, and prove
some frame/separation properties. *)
...
...
@@ -132,8 +132,8 @@ module TreeShape
(** The described structure can be modeled as a tree of locations *)
type treel = tree loc
(**
[is_tree memo t c p] describe the fact that [c]
points to
a well-formed tree modeled by
[t], whose root parent node is [p]
. *)
(**
`is_tree memo t c p` describe the fact that `c`
points to
a well-formed tree modeled by
`t`, whose root parent node is `p`
. *)
predicate is_tree (memo:pmem) (t:treel) (c p:loc) = match t with
| Empty -> c = null
| Node l m r -> c <> null /\ c = m /\ memo[Parent][c] = p /\
...
...
@@ -143,23 +143,23 @@ module TreeShape
is_tree memo l cl c /\ is_tree memo r cr c
end
(**
[footprint t] is the memory footprint of [t]
, e.g the set of
(**
`footprint t` is the memory footprint of `t`
, e.g the set of
locations occuring in the tree. *)
function footprint (t:treel) : set loc = match t with
| Empty -> empty
| Node l m r -> add m (union (footprint l) (footprint r))
end
(**
[ext s memo1 memo2]
mean that the pointer fields associated to
locations in set
[s]
are identical in memo1 and memo2. *)
(**
`ext s memo1 memo2`
mean that the pointer fields associated to
locations in set
`s`
are identical in memo1 and memo2. *)
predicate ext (s:set loc) (memo1 memo2:pmem) =
forall k x. mem x s -> memo1[k][x] = memo2[k][x]
(**
[unchanged memo1 memo2]
mean that all pointer fields in
[memo1] and [memo2]
are identical. *)
(**
`unchanged memo1 memo2`
mean that all pointer fields in
`memo1` and `memo2`
are identical. *)
predicate unchanged (memo1 memo2:pmem) =
forall k x. memo1[k][x] = memo2[k][x]
(**
[was_marked t memo1 memo2] mean that [memo2]
is the update
of
[memo1] obtained by marking all elements in [t]
. *)
(**
`was_marked t memo1 memo2` mean that `memo2`
is the update
of
`memo1` obtained by marking all elements in `t`
. *)
predicate was_marked (t:treel) (memo1 memo2:map loc bool) =
(forall l. mem l (footprint t) -> memo2[l]) /\
(forall l. not mem l (footprint t) -> memo2[l] = memo1[l])
...
...
@@ -221,11 +221,11 @@ module TreeShape
aux lf (memo[Left][c]) c; aux rg (memo[Right][c]) c
(** Algorithm phases.
[GoLeft]
mean that the algorithm will try to explore the left
`GoLeft`
mean that the algorithm will try to explore the left
subtree
[GoRight]
mean that the algorithm will explore the right subtree
[GoBack]
mean that the algorithm will go back to the parent node
[Finish]
mean that the alogrithm will exit *)
`GoRight`
mean that the algorithm will explore the right subtree
`GoBack`
mean that the algorithm will go back to the parent node
`Finish`
mean that the alogrithm will exit *)
type phase =
| GoLeft
| GoRight
...
...
@@ -239,9 +239,9 @@ module TreeShape
| GoBack -> GoLeft
| Finish -> Finish
end
(**
[rotated memo1 memo2 ph c] describe how [c]
is rotated in
[memo2] with respect to its initial position in [memo1]
for
current phase
[ph]
. In final phase, it is not rotated but
(**
`rotated memo1 memo2 ph c` describe how `c`
is rotated in
`memo2` with respect to its initial position in `memo1`
for
current phase
`ph`
. In final phase, it is not rotated but
null instead. *)
predicate rotated (memo1 memo2:pmem) (ph:phase) (c:loc) =
(forall k x. x <> c -> memo1[k][x] = memo2[k][x]) /\
...
...
@@ -279,25 +279,25 @@ module Recursive
to link it with its recursive version. However,
the obtained algorithm does not really need the call stack
to run. Here is how we achieve this:
- We create a non-recursive sub-routine
[bloc]
corresponding to
- We create a non-recursive sub-routine
`bloc`
corresponding to
one turn of the while loop in the challenge's code.
It uses an exception to simulate exit.
Also, this sub-routine does not have any non-ghost argument,
so calling
[bloc]
really amounts to advancing in the loop execution.
so calling
`bloc`
really amounts to advancing in the loop execution.
- We forbids use of any side-effect in the recursive procedure
except those obtained by calling
[bloc]
. Hence calling
except those obtained by calling
`bloc`
. Hence calling
the recursive procedure is equivalent to run a certain
amounts of turns in the loop execution.
Note that since we will prove that the recursive procedure
terminates, it might not run a finite amount of turns and diverges
afterward.
- After the topmost call to the recursive procedure,
we add an infinite loop who only calls
[bloc]
at every turns.
we add an infinite loop who only calls
`bloc`
at every turns.
This call and the loop are enclosed in an exception catching
construction to detect loop termination.
Hence it is justifiable that the algorithm with
the recursive procedure is equivalent (in the sense that
they have the same side-effects) as an infinite loop of
[bloc]
calls,
they have the same side-effects) as an infinite loop of
`bloc`
calls,
encapsulated in an exception catching expression. And this
algorithm is evidently equivalent to the original challenge code.
*)
...
...
@@ -320,17 +320,17 @@ module Recursive
(* ^ Used to encode the do { .. } while() loop as a while() {..}.
Iterations will set the flag. *)
let ghost z = ref (null ()) in (* Store previously explored node. *)
(* Loop body.
[mem0]
is memory state at start of recursive call,
[ph]
is phase. *)
(* Loop body.
`mem0`
is memory state at start of recursive call,
`ph`
is phase. *)
let bloc (ghost mem0:pmem) (ghost ph:phase) : unit
(* current node
[!x]
is rotated correctly with
(* current node
`!x`
is rotated correctly with
respect to the phase. *)
requires { rotated mem0 memo.accessor ph !x }
requires { ph = Finish -> !entered }
writes { memo, x, y, z, entered }
(* Caracterise
[x] and [z]
reference updates. *)
(* Caracterise
`x` and `z`
reference updates. *)
ensures { !z = !(old x) /\ !x = memo.accessor[Parent][!z] }
(*
[Finish]
phase never ends normally *)
(*
`Finish`
phase never ends normally *)
ensures { ph <> Finish /\ !entered }
(* Node is marked, and other nodes do not change. *)
ensures { memo.mark[!z] }
...
...
@@ -341,7 +341,7 @@ module Recursive
= (old memo).accessor[Right][!z]
then memo.accessor = (old memo).accessor
else rotated mem0 memo.accessor (next_phase ph) !z }
(* In
[Finish] phase, the code throws [Stop]
without changing
(* In
`Finish` phase, the code throws `Stop`
without changing
anything. *)
raises { Stop -> ph = Finish /\ memo = old memo }
= if !entered && is_null !x then raise Stop; (* ==> do { BODY *)
...
...
@@ -457,7 +457,7 @@ module Iterative
else if pc <= 3 then f.memo3
else f.memo4
(** Postcondition relation for
[bloc]
calls. *)
(** Postcondition relation for
`bloc`
calls. *)
predicate bloc_rel (mem0:pmem) (ph:phase) (s1 s2:snap) =
s2.parent = s1.cursor /\ s2.cursor = s2.pointers[Parent][s2.parent] /\
s2.marks[s2.parent] /\
...
...
@@ -466,7 +466,7 @@ module Iterative
then s2.pointers = s1.pointers
else rotated mem0 s2.pointers (next_phase ph) s2.parent
(** postcondition relation for recursive (
[aux]
) calls. *)
(** postcondition relation for recursive (
`aux`
) calls. *)
predicate rec_rel (t:treel) (s1 s2:snap) =
unchanged s1.pointers s2.pointers /\
s2.cursor = s1.parent /\ s2.parent = s1.cursor /\
...
...
examples/verifythis_fm2012_LRS.mlw
View file @
7990ef5e
...
...
@@ -91,31 +91,31 @@ module LCP
use export int.Int
use import array.Array
(**
[is_common_prefix a x y l] is true when the prefixes of length [l]
at respective positions
[x] and [y] in array [a]
are identical. In
other words, the array parts
a[x..x+l-1] and a[y..y+l-1]
are equal
(**
`is_common_prefix a x y l` is true when the prefixes of length `l`
at respective positions
`x` and `y` in array `a`
are identical. In
other words, the array parts
`a[x..x+l-1]` and `a[y..y+l-1]`
are equal
*)
predicate is_common_prefix (a:array int) (x y l:int) =
0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
(forall i:int. 0 <= i < l -> a[x+i] = a[y+i])
(** This lemma helps for the proof of
[lcp]
(but is not mandatory) and
is needed later (for
[le_trans]
) *)
(** This lemma helps for the proof of
`lcp`
(but is not mandatory) and
is needed later (for
`le_trans`
) *)
lemma not_common_prefix_if_last_char_are_different:
forall a:array int, x y:int, l:int.
0 <= l /\ x+l < a.length /\ y+l < a.length /\ a[x+l] <> a[y+l] ->
not is_common_prefix a x y (l+1)
(**
[is_longest_common_prefix a x y l] is true when [l]
is the maximal
length such that prefixes at positions
[x] and [y] in array [a]
(**
`is_longest_common_prefix a x y l` is true when `l`
is the maximal
length such that prefixes at positions
`x` and `y` in array `a`
are identical. *)
predicate is_longest_common_prefix (a:array int) (x y l:int) =
is_common_prefix a x y l /\
forall m:int. l < m -> not (is_common_prefix a x y m)
(** This lemma helps to proving
[lcp]
(but again is not mandatory),
and is needed for proving
[lcp_sym] and [le_trans]
lemmas, and
the post-condition of
[compare]
function in the "absurd" case *)
(** This lemma helps to proving
`lcp`
(but again is not mandatory),
and is needed for proving
`lcp_sym` and `le_trans`
lemmas, and
the post-condition of
`compare`
function in the "absurd" case *)
lemma longest_common_prefix_succ:
forall a:array int, x y l:int.
...
...
@@ -226,11 +226,11 @@ let compare (a:array int) (x y:int) : int
use map.MapInjection
(**
[range a] is true when for each [i], [a[i]] is between [0] at
[a.length-1]
*)
(**
`range a` is true when for each `i`, `a[i]` is between `0` and
`a.length-1`
*)
predicate range (a:array int) = MapInjection.range a.elts a.length
(** for the
[permut]
predicate (permutation of elements) *)
(** for the
`permut`
predicate (permutation of elements) *)
use array.ArrayPermut
predicate le (a : array int) (x y:int) = x = y \/ lt a x y
...
...
@@ -281,7 +281,7 @@ let sort (a:array int) (data : array int)
assert { ArrayPermut.exchange (data at L) data (!j-1) !j };
decr j
done;
(* needed to prove the invariant
[sorted_sub a data.elts 0 i]
*)
(* needed to prove the invariant
`sorted_sub a data.elts 0 i`
*)
assert { !j > 0 -> le a data[!j-1] data[!j] }
done
...
...
@@ -351,7 +351,7 @@ let select (s:suffixArray) (i:int) : int
use array.ArrayPermut
(** needed to establish invariant in function
[create]
*)
(** needed to establish invariant in function
`create`
*)
lemma permut_permutation : forall a1 a2:array int.
ArrayPermut.permut_all a1 a2 /\ permutation a1.elts a1.length ->
permutation a2.elts a2.length
...
...
@@ -444,9 +444,9 @@ module LRS
use SuffixArray
(** additional properties relating
[le] and [longest_common_prefix]
*)
(** additional properties relating
`le` and `longest_common_prefix`
*)
(* needed for
[lrs]
function, last before last assert *)
(* needed for
`lrs`
function, last before last assert *)
lemma lcp_sym :
forall a:array int, x y l:int.
0 <= x <= a.length /\ 0 <= y <= a.length ->
...
...
@@ -506,7 +506,7 @@ lemma le_le_common_prefix:
solLength := l
end
done;
(** the following assert needs
[lcp_sym]
lemma *)
(** the following assert needs
`lcp_sym`
lemma *)
assert { forall j k l:int.
0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
LCP.is_longest_common_prefix a
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment