diff --git a/doc/manual.tex b/doc/manual.tex
index f6fd625f6e754cb763adee3b054d7fe6f701129f..bed077b9b5652d71349662394b3e2476bf0af9bd 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -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} \\
diff --git a/src/trywhy3/examples/ex1_eucl_div.mlw b/src/trywhy3/examples/ex1_eucl_div.mlw
index 3083f9ee6717c3a33b7859fcbdb17f488678a878..ad2299493de85086219d975f7c22893339fb862b 100644
--- a/src/trywhy3/examples/ex1_eucl_div.mlw
+++ b/src/trywhy3/examples/ex1_eucl_div.mlw
@@ -1,4 +1,3 @@
-
(* 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 }
diff --git a/src/trywhy3/examples/ex2_fact.mlw b/src/trywhy3/examples/ex2_fact.mlw
index c8a72cb7615a84951fa88429b7f421006de85002..c6308237d294b303fa7e8dd9da2a63246bc52ec2 100644
--- a/src/trywhy3/examples/ex2_fact.mlw
+++ b/src/trywhy3/examples/ex2_fact.mlw
@@ -1,5 +1,4 @@
-
-(* 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 }
diff --git a/src/trywhy3/examples/ex3_multiplication.mlw b/src/trywhy3/examples/ex3_multiplication.mlw
index 799601aa0d9d4d9bb6cab871eae91516b6dc7b94..fdeb6079f6c2b47420129442f25048c2c5cf9ec0 100644
--- a/src/trywhy3/examples/ex3_multiplication.mlw
+++ b/src/trywhy3/examples/ex3_multiplication.mlw
@@ -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
diff --git a/src/trywhy3/examples/ex4_two_way.mlw b/src/trywhy3/examples/ex4_two_way.mlw
index ab1fda5bdd4ae966b385591fd953914ac6e0d941..7793507eaaa913ff4faea87ea3999ec6d052656f 100644
--- a/src/trywhy3/examples/ex4_two_way.mlw
+++ b/src/trywhy3/examples/ex4_two_way.mlw
@@ -1,4 +1,3 @@
-
(* 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
diff --git a/src/trywhy3/examples/ex5_flag.mlw b/src/trywhy3/examples/ex5_flag.mlw
index 00f1cf2b42fc2c5b0d4de5d99472ebba9fb3ab8d..36456d7eb69882ac8aa0ed03fd49bb84da8de3d8 100644
--- a/src/trywhy3/examples/ex5_flag.mlw
+++ b/src/trywhy3/examples/ex5_flag.mlw
@@ -1,4 +1,3 @@
-
(* 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
diff --git a/src/trywhy3/examples/ex6_buffer.mlw b/src/trywhy3/examples/ex6_buffer.mlw
index 3ca275939f05a7253b5cb0276f133e498510c7e7..d1aafa6dca63a9070b63612299029967a11ba939 100644
--- a/src/trywhy3/examples/ex6_buffer.mlw
+++ b/src/trywhy3/examples/ex6_buffer.mlw
@@ -1,4 +1,3 @@
-
(* 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
diff --git a/src/trywhy3/examples/ex7_fill.mlw b/src/trywhy3/examples/ex7_fill.mlw
index 6587b462d177f9d3a1d66bbc8adaea8561223d2b..e25c27bdf398ab0dacd59c567e01023a040fe803 100644
--- a/src/trywhy3/examples/ex7_fill.mlw
+++ b/src/trywhy3/examples/ex7_fill.mlw
@@ -1,4 +1,3 @@
-
(* (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