Commit bd7d809c authored by Léo Andrès's avatar Léo Andrès

remove useless `import` (avoid warnings)

parent 16ea7c91
......@@ -6,7 +6,7 @@ generated counterexample in comments:
\begin{whycode}
theory T
use import int.Int
use int.Int
goal g_no_lab_ex : forall x:int. x >= 42 -> x + 3 <= 50
......@@ -79,7 +79,7 @@ counterexample of an abstract value:
\begin{whycode}
theory A
use import int.Int
use int.Int
type byte
function to_rep byte : int
......
......@@ -30,8 +30,8 @@ theory List
end
theory Length
use import List
use import int.Int
use List
use int.Int
function length (l : list 'a) : int =
match l with
......@@ -43,8 +43,8 @@ theory Length
end
theory Sorted
use import List
use import int.Int
use List
use int.Int
inductive sorted (list int) =
| Sorted_Nil :
......@@ -74,13 +74,12 @@ We deliberately make this theory that short, for reasons which will be
discussed later.
The next theory, \texttt{Length}, introduces the notion of list
length. The \texttt{use import List} command indicates that this new
length. The \texttt{use List} command indicates that this new
theory may refer to symbols from theory \texttt{List}. These symbols
are accessible in a qualified form, such as \texttt{List.list} or
\texttt{List.Cons}. The \texttt{import} qualifier additionally allows
us to use them without qualification.
\texttt{List.Cons} or without qualification.
Similarly, the next command \texttt{use import int.Int} adds to our
Similarly, the next command \texttt{use int.Int} adds to our
context the theory \texttt{int.Int} from the standard library. The
prefix \texttt{int} indicates the file in the standard library
containing theory \texttt{Int}. Theories referred to without prefix
......@@ -154,7 +153,7 @@ theory Order
end
theory SortedGen
use import List
use List
clone import Order as O
inductive sorted (l : list t) =
......@@ -168,7 +167,7 @@ theory SortedGen
end
theory SortedIntList
use import int.Int
use int.Int
clone SortedGen with type O.t = int, predicate O.(<=) = (<=)
end
\end{whycode}
......
......@@ -847,16 +847,16 @@ To \texttt{use} or \texttt{clone} a module \texttt{M} from file
available in \why's default load path. For instance, the module of
integers and the module of references are imported as follows:
\begin{whycode}
use import int.Int
use import ref.Ref
use int.Int
use ref.Ref
\end{whycode}
A sub-directory \texttt{mach/} provides various modules to model
machine arithmetic.
For instance, the module of 63-bit integers and the module of arrays
indexed by 63-bit integers are imported as follows:
\begin{whycode}
use import mach.int.Int63
use import mach.array.Array63
use mach.int.Int63
use mach.array.Array63
\end{whycode}
In particular, the types and operations from these modules are mapped
to native OCaml's types and operations when \why code is extracted to
......
......@@ -195,7 +195,7 @@ The next theory contains the 15 hypotheses. It starts by importing
theory \texttt{Einstein}.
\begin{whycode}
theory EinsteinHints
use import Einstein
use Einstein
\end{whycode}
Then each hypothesis is stated in terms of \texttt{to\_} and \texttt{of}
functions. For instance, the hypothesis ``The Englishman lives in a
......@@ -215,8 +215,8 @@ end
Finally, we declare the goal in a fourth theory:
\begin{whycode}
theory Problem
use import Einstein
use import EinsteinHints
use Einstein
use EinsteinHints
goal G: Pet.to_ Fish = German
end
......@@ -253,13 +253,13 @@ module MaxAndSum
We are obviously needing arithmetic, so we import the corresponding
theory, exactly as we would do within a theory definition:
\begin{whycode}
use import int.Int
use int.Int
\end{whycode}
We are also going to use references and arrays from \why\ standard
library, so we import the corresponding modules:
\begin{whycode}
use import ref.Ref
use import array.Array
use ref.Ref
use array.Array
\end{whycode}
Modules \texttt{Ref} and \texttt{Array} respectively provide a type
\texttt{ref 'a} for references and a type \texttt{array 'a} for
......@@ -340,9 +340,9 @@ Figure~\ref{fig:MaxAndSum} shows the whole code.
\begin{whycode}
module MaxAndSum
use import int.Int
use import ref.Ref
use import array.Array
use int.Int
use ref.Ref
use array.Array
let max_sum (a: array int) (n: int) : (int, int)
requires { n = length a }
......@@ -392,8 +392,8 @@ with as much automation as possible. In a new file, we start a new
module and we import arithmetic and arrays:
\begin{whycode}
module InvertingAnInjection
use import int.Int
use import array.Array
use int.Int
use array.Array
\end{whycode}
It is convenient to introduce predicate definitions for the properties
of being injective and surjective. These are purely logical
......@@ -448,8 +448,8 @@ discharged automatically, thanks to the lemma.
\begin{whycode}
module InvertingAnInjection
use import int.Int
use import array.Array
use int.Int
use array.Array
predicate injective (a: array int) (n: int) =
forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
......@@ -505,8 +505,8 @@ for the $n$-th element of a list. The latter returns an option type,
depending on whether the index is meaningful or not.
\begin{whycode}
module SearchingALinkedList
use import int.Int
use import option.Option
use int.Int
use option.Option
use export list.List
use export list.Length
use export list.Nth
......@@ -576,7 +576,7 @@ The verification conditions are all discharged automatically.
\begin{whycode}
module SearchingALinkedList
use import int.Int
use int.Int
use export list.List
use export list.Length
use export list.Nth
......@@ -614,8 +614,8 @@ To do this, we need to import references from the standard library,
together with theory \texttt{list.HdTl} which defines functions
\texttt{hd} and \texttt{tl} over lists.
\begin{whycode}
use import ref.Ref
use import list.HdTl
use ref.Ref
use list.HdTl
\end{whycode}
Being partial functions, \texttt{hd} and \texttt{tl} return options.
For the purpose of our code, though, it is simpler to have functions
......@@ -673,8 +673,8 @@ $N$-element array which assigns the queen on row $i$ to its column.
Thus we start our module by importing arithmetic and arrays:
\begin{whycode}
module NQueens
use import int.Int
use import array.Array
use int.Int
use array.Array
\end{whycode}
The code is a simple backtracking algorithm, which tries to put a queen
on each row of the chess board, one by one (there is basically no
......@@ -741,8 +741,8 @@ This first part of the solution is given in Figure~\ref{fig:NQueens1}.
%END LATEX
\begin{whycode}
module NQueens
use import int.Int
use import array.Array
use int.Int
use array.Array
predicate consistent_row (board: array int) (pos: int) (q: int) =
board[q] <> board[pos] /\
......@@ -954,8 +954,8 @@ In a new module, we import arithmetic and theory
operations we will require: length, reversal, and concatenation.
\begin{whycode}
module AmortizedQueue
use import int.Int
use import option.Option
use int.Int
use option.Option
use export list.ListRich
\end{whycode}
The queue data type is naturally introduced as a polymorphic record type.
......@@ -1062,9 +1062,9 @@ The verification conditions are all discharged automatically.
\begin{whycode}
module AmortizedQueue
use import int.Int
use import option.Option
use import list.ListRich
use int.Int
use option.Option
use list.ListRich
type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; }
......
......@@ -14,8 +14,8 @@ end
module A
use import int.Int
use import mach.int.Int63
use int.Int
use mach.int.Int63
val add (x y:int63) : int63
requires { int63'minInt <= int63'int x + int63'int y <= int63'maxInt }
......@@ -27,4 +27,4 @@ let test (x:int63) : int63
end
*)
\ No newline at end of file
*)
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