Commit f3867263 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove "use import" from trywhy3's examples and fix a few other typos.

parent eab446ca
......@@ -348,6 +348,8 @@ file contains other potential incompatibility.
\hline
\texttt{namespace N} & \texttt{scope N} \\
\hline
\texttt{use import M} & \texttt{use M} \\
\hline
\texttt{"attribute"} & \texttt{[@attribute]} \\
\hline
\texttt{meta M prop P} & \texttt{meta M lemma P} or \texttt{meta M axiom P} or \texttt{meta M goal P} \\
......
(* Euclidean division
1. Prove soundness, i.e. (division a b) returns an integer q such that
......@@ -9,13 +8,12 @@
2. Prove termination.
(You may have to strengthen the precondition even further.)
*)
module Division
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
let division (a b: int) : int
requires { true }
......
(* Two programs to compute the factorial.
(* Two programs to compute the factorial
Note: function "fact" from module int.Fact (already imported)
can be used in specifications.
......@@ -12,20 +11,19 @@
b. Prove its termination.
2. In module FactLoop
2. In module FactLoop:
a. Prove soundness of function fact_loop
a. Prove soundness of function fact_loop.
b. Prove its termination
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
use int.Int
use int.Fact
let rec fact_rec (n: int) : int
requires { true }
......@@ -37,9 +35,9 @@ end
module FactLoop
use import int.Int
use import int.Fact
use import ref.Ref
use int.Int
use int.Fact
use ref.Ref
let fact_loop (n: int) : int
requires { true }
......
......@@ -3,7 +3,7 @@
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
Note: library int.ComputerDivision (already imported) provides functions
"div" and "mod".
Questions:
......@@ -11,14 +11,13 @@
1. Prove soundness of function multiplication.
2. Prove its termination.
*)
module Multiplication
use import int.Int
use import int.ComputerDivision
use import ref.Ref
use int.Int
use int.ComputerDivision
use ref.Ref
let multiplication (a b: int) : int
requires { true }
......@@ -34,8 +33,11 @@ module Multiplication
done;
!z
let main () =
multiplication 10 13
end
(* Note: this is exactly the same algorithm as exponentiation by squarring
(* Note: this is exactly the same algorithm as exponentiation by squaring
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.
......@@ -18,17 +17,16 @@
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
use int.Int
use bool.Bool
use ref.Refint
use array.Array
use array.ArraySwap
use array.ArrayPermut
predicate (<<) (x y: bool) = x = False \/ y = True
......@@ -38,7 +36,7 @@ module TwoWaySort
let two_way_sort (a: array bool) : unit
ensures { true }
=
'Init:
label Init in
let i = ref 0 in
let j = ref (length a - 1) in
while !i < !j do
......
(* Dijkstra's "Dutch national flag"
The following program sorts an array whose elements may have three
......@@ -22,16 +21,15 @@
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
use int.Int
use ref.Ref
use array.Array
use array.ArraySwap
use array.ArrayPermut
type color = Blue | White | Red
......
(* Ring buffer (from the 2nd Verified Software Competition 2012)
Implement operations create, clear, push, head, and pop below (that
......@@ -8,9 +7,9 @@
module RingBuffer
use import int.Int
use import seq.Seq
use import array.Array
use int.Int
use seq.Seq
use array.Array
type queue 'a = {
mutable first: int;
......@@ -20,15 +19,15 @@ module RingBuffer
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]
capacity = Array.length data /\
0 <= first < capacity /\
0 <= len <= capacity /\
len = Seq.length sequence /\
forall i: int. 0 <= i < len ->
Seq.([]) sequence i =
data[if first + i < capacity
then first + i
else first + i - capacity]
}
val create (n: int) (dummy: 'a) : queue 'a
......
(* (Exercise borrowed from Rustan Leino's Dafny tutorial at VSTTE 2012)
Function "fill" below stores the elements of tree "t" in array "a",
......@@ -8,7 +7,7 @@
Questions:
1. Prove safety i.e. the absence of array access out of bounds.
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
......@@ -19,13 +18,12 @@
"contains" below).
4. Prove termination of function "fill".
*)
module Fill
use import int.Int
use import array.Array
use int.Int
use array.Array
type elt
type tree = Null | Node tree elt tree
......
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