trywhy3: fixed Makefile deps, changed examples

parent 1c782a4f
......@@ -304,3 +304,4 @@ pvsbin/
/src/jessie/tests/demo/result/*.log
/trash
trywhy3.tar.gz
......@@ -1489,7 +1489,7 @@ trywhy3_package: trywhy3
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js src/trywhy3/examples/*.mlw
js_of_ocaml -I src/trywhy3 \
--file=why3_worker.js:/ \
--file=alt_ergo_worker.js:/ \
......
module BinaryMultiplication
use import mach.int.Int
use import ref.Ref
let mult (a b: int)
requires { b >= 0 }
ensures { result = a * b }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { 0 <= !y }
invariant { !z + !x * !y = a * b }
variant { !y }
if !y % 2 <> 0 then z := !z + !x;
x := 2 * !x;
y := !y / 2
done;
!z
end
module Test1
use BinaryMultiplication as B
let main () = B.mult 6 7
end
module Test2
use BinaryMultiplication as B
let main () = B.mult 4546729 21993833369
end
\ No newline at end of file
theory T
(** Type of all persons *)
type person
(** Predicate saying that some person drinks *)
predicate drinks person
(** Paradox: there exists a person x such that if x drinks,
then everybody drinks *)
goal drinkers_paradox:
exists x:person. drinks x ->
forall y:person. drinks y
end
(* Euclidean division
1. Prove soundness, i.e. (division a b) returns an integer q such that
a = bq+r and 0 <= r < b for some r.
(You have to strengthen the precondition.)
Do you have to require b <> 0? Why?
2. Prove termination.
(You may have to strengthen the precondition even further.)
*)
module Division
use import int.Int
use import ref.Ref
let division (a b: int) : int
requires { true }
ensures { exists r: int. a = b * result + r /\ 0 <= r < b }
=
let q = ref 0 in
let r = ref a in
while !r >= b do
invariant { true }
q := !q + 1;
r := !r - b
done;
!q
let main () =
division 1000 42
end
(* Two programs to compute the factorial.
Note: function "fact" from module int.Fact (already imported)
can be used in specifications.
Questions :
1. In module FactRecursive:
a. Prove soundness of function fact_rec.
b. Prove its termination.
2. In module FactLoop
a. Prove soundness of function fact_loop
b. Prove its termination
c. Change the code to use a for loop instead of a while loop.
*)
module FactRecursive
use import int.Int
use import int.Fact
let rec fact_rec (n: int) : int
requires { true }
ensures { result = fact n }
=
if n = 0 then 1 else n * fact_rec (n - 1)
end
module FactLoop
use import int.Int
use import int.Fact
use import ref.Ref
let fact_loop (n: int) : int
requires { true }
ensures { result = fact n }
= let m = ref 0 in
let r = ref 1 in
while !m < n do
invariant { true }
m := !m + 1;
r := !r * !m
done;
!r
end
(* Ancient Egyptian multiplication
Multiply two integers a and b using only addition, multiplication by 2,
and division by 2. You may assume b to be nonnegative.
Note: library int.ComputerDivision (already imported) provide functions
"div" and "mod".
Questions:
1. Prove soundness of function multiplication.
2. Prove its termination.
*)
module Multiplication
use import int.Int
use import int.ComputerDivision
use import ref.Ref
let multiplication (a b: int) : int
requires { true }
ensures { true }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { true }
if mod !y 2 = 1 then z := !z + !x;
x := 2 * !x;
y := div !y 2
done;
!z
end
(* Note: this is exactly the same algorithm as exponentiation by squarring
with power/*/1 being replaced by */+/0.
*)
\ No newline at end of file
(* Two Way Sort
The following program sorts an array of Boolean values, with False<True.
Questions:
1. Prove safety i.e. the absence of array access out of bounds.
2. Prove termination.
3. Prove that array a is sorted after execution of function two_way_sort
(using the predicate sorted that is provided).
4. Show that after execution the array contents is a permutation of its
initial contents. Use the library predicate "permut_all" to do so
(the corresponding module ArrayPermut is already imported).
You can refer to the contents of array a at the beginning of the
function with notation (at a 'Init).
*)
module TwoWaySort
use import int.Int
use import bool.Bool
use import ref.Refint
use import array.Array
use import array.ArraySwap
use import array.ArrayPermut
predicate (<<) (x y: bool) = x = False \/ y = True
predicate sorted (a: array bool) =
forall i1 i2: int. 0 <= i1 <= i2 < a.length -> a[i1] << a[i2]
let two_way_sort (a: array bool) : unit
ensures { true }
=
'Init:
let i = ref 0 in
let j = ref (length a - 1) in
while !i < !j do
invariant { true }
if not a[!i] then
incr i
else if a[!j] then
decr j
else begin
swap a !i !j;
incr i;
decr j
end
done
end
(* Dijkstra's "Dutch national flag"
The following program sorts an array whose elements may have three
different values, standing for the three colors of the Dutch
national flag (blue, white, and red).
Questions:
1. Prove safety i.e. the absence of array access out of bounds.
2. Prove termination.
3. Prove that, after execution, the array is sorted as follows:
+--------+---------+---------+
| blue | white | red |
+--------+---------+---------+
(using the predicate "monochrome" that is provided).
4. Show that after execution the array contents is a permutation of its
initial contents. Use the library predicate "permut_all" to do so
(the corresponding module ArrayPermut is already imported).
*)
module Flag
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArraySwap
use import array.ArrayPermut
type color = Blue | White | Red
predicate monochrome (a: array color) (i: int) (j: int) (c: color) =
forall k: int. i <= k < j -> a[k]=c
let dutch_flag (a: array color)
requires { 0 <= length a }
ensures { true }
=
let b = ref 0 in
let i = ref 0 in
let r = ref (length a) in
while !i < !r do
invariant { true }
match a[!i] with
| Blue ->
swap a !b !i;
b := !b + 1;
i := !i + 1
| White ->
i := !i + 1
| Red ->
r := !r - 1;
swap a !r !i
end
done
end
(* Ring buffer (from the 2nd Verified Software Competition 2012)
Implement operations create, clear, push, head, and pop below (that
is, replace "val" with "let", add a body to the function, and prove
it correct).
*)
module RingBuffer
use import int.Int
use import seq.Seq
use import array.Array
type queue 'a = {
mutable first: int;
mutable len : int;
data : array 'a;
ghost capacity: int;
ghost mutable sequence: Seq.seq 'a;
}
invariant {
self.capacity = Array.length self.data /\
0 <= self.first < self.capacity /\
0 <= self.len <= self.capacity /\
self.len = Seq.length self.sequence /\
forall i: int. 0 <= i < self.len ->
Seq.([]) self.sequence i =
self.data[if self.first + i < self.capacity
then self.first + i
else self.first + i - self.capacity]
}
val create (n: int) (dummy: 'a) : queue 'a
requires { n > 0 }
ensures { capacity result = n }
ensures { result.sequence = Seq.empty }
(* = ... *)
let length (q: queue 'a) : int
ensures { result = Seq.length q.sequence }
= q.len
val clear (q: queue 'a) : unit
writes { q.len, q.sequence }
ensures { q.sequence = Seq.empty }
(* = ... *)
val push (q: queue 'a) (x: 'a) : unit
requires { Seq.length q.sequence < q.capacity }
writes { q.data.elts, q.len, q.sequence }
ensures { q.sequence = Seq.snoc (old q.sequence) x }
(* = ... *)
val head (q: queue 'a) : 'a
requires { Seq.length q.sequence > 0 }
ensures { result = Seq.([]) q.sequence 0 }
(* = ... *)
val pop (q: queue 'a) : 'a
requires { Seq.length q.sequence > 0 }
writes { q.first, q.len, q.sequence }
ensures { result = Seq.([]) (old q.sequence) 0 }
ensures { q.sequence = (old q.sequence)[1 ..] }
(* = ... *)
end
(* (Exercise borrowed from Rustan Leino's Dafny tutorial at VSTTE 2012)
Function "fill" below stores the elements of tree "t" in array "a",
according to some inorder traversal, starting at array index "start",
as long as there is room in the array. It returns the array position
immediately right of the last element of "t" stored in "a".
Questions:
1. Prove safety i.e. the absence of array access out of bounds.
(You have to strengthen the precondition.)
2. Show that, after the execution of "fill", the elements in
a[0..start[ have not been modified.
3. Show that, after the execution of "fill", the elements in
a[start..result[ belong to tree "t" (using predicate
"contains" below).
4. Prove termination of function "fill".
*)
module Fill
use import int.Int
use import array.Array
type elt
type tree = Null | Node tree elt tree
predicate contains (t: tree) (x: elt) = match t with
| Null -> false
| Node l y r -> contains l x || x = y || contains r x
end
let rec fill (t: tree) (a: array elt) (start: int) : int
requires { 0 <= length a }
ensures { true }
=
match t with
| Null ->
start
| Node l x r ->
let res = fill l a start in
if res <> length a then begin
a[res] <- x;
fill r a (res + 1)
end else
res
end
end
module FactWhile
use import mach.int.Int
use import int.Fact
use import ref.Ref
(** Factorial with a while loop *)
let fact_imp (x:int) : int
requires { x >= 0 }
ensures { result = fact x }
= let y = ref 0 in
let r = ref 1 in
while !y < x do
invariant { 0 <= !y <= x }
invariant { !r = fact !y }
variant { x - !y }
y := !y + 1;
r := !r * !y
done;
!r
let main () = (fact_imp 7, fact_imp 42)
end
module FactFor
use import mach.int.Int
use import int.Fact
use import ref.Ref
(** Factorial with a for loop *)
let fact_imp (x:int) : int
requires { x >= 0 }
ensures { result = fact x }
= let r = ref 1 in
for y = 1 to x do
invariant { !r = fact (y-1) }
r := !r * y
done;
!r
let main () = (fact_imp 7, fact_imp 42)
end
Ex1 Eucl Div
ex1_eucl_div.mlw
Ex2 Fact
ex2_fact.mlw
Ex3 Multiplication
ex3_multiplication.mlw
Ex4 Two Way
ex4_two_way.mlw
Ex5 Flag
ex5_flag.mlw
Ex6 Buffer
ex6_buffer.mlw
Ex7 Fill
ex7_fill.mlw
module M
use import int.Int
use import ref.Ref
function sqr (x:int) : int = x * x
lemma sqr_sum :
forall x y : int. sqr(x+y) = sqr x + 2*x*y + sqr y
let isqrt (x:int) : int
requires { x >= 0 }
ensures { result >= 0 }
ensures { sqr result <= x < sqr (result + 1) }
= let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
invariant { !count >= 0 }
invariant { x >= sqr !count }
invariant { !sum = sqr (!count+1) }
variant { x - !count }
count := !count + 1;
sum := !sum + 2 * !count + 1
done;
!count
let main () ensures { result = 4 } = isqrt 17
end
theory T
use import int.Int
goal g: exists x:int. x*(x+1) = 42
end
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