syntax.tex 11.8 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
\chapter{The \why Language}
2
\label{chap:syntax}
3
%HEVEA\cutname{syntax.html}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
4 5 6 7

This chapter describes the input syntax, and informally gives its semantics,
illustrated by examples.

MARCHE Claude's avatar
MARCHE Claude committed
8
A \why text contains a list of \emph{theories}.
9
A theory is a list of \emph{declarations}. Declarations introduce new
10
types, functions and predicates, state axioms, lemmas and goals.
11
These declarations can be directly written in the theory or taken from
MARCHE Claude's avatar
MARCHE Claude committed
12
existing theories. The base logic of \why is first-order
13
logic with polymorphic types.
MARCHE Claude's avatar
doc  
MARCHE Claude committed
14

15
\section{Example 1: Lists}
16

17 18 19 20 21
%BEGIN LATEX
Figure~\ref{fig:tutorial1} contains an example of \why input
text, containing three theories.
%END LATEX
%HEVEA The code below is an example of \why input text, containing three theories.
22

23
%BEGIN LATEX
24
\begin{figure}
25
\centering
26
%END LATEX
27
\begin{whycode}
28 29 30 31 32 33 34 35
theory List
  type list 'a = Nil | Cons 'a (list 'a)
end

theory Length
  use import List
  use import int.Int

36
  function length (l : list 'a) : int =
37 38 39 40 41
    match l with
    | Nil      -> 0
    | Cons _ r -> 1 + length r
    end

42
  lemma Length_nonnegative : forall l:list 'a. length l >= 0
43 44 45 46 47
end

theory Sorted
  use import List
  use import int.Int
48

49
  inductive sorted (list int) =
50
    | Sorted_Nil :
51
        sorted Nil
52
    | Sorted_One :
53
        forall x:int. sorted (Cons x Nil)
54 55
    | Sorted_Two :
        forall x y : int, l : list int.
56 57
        x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
end
58
\end{whycode}
59
%BEGIN LATEX
60 61
\vspace*{-1em}%\hrulefill
\caption{Example of \why text}
62 63
\label{fig:tutorial1}
\end{figure}
64 65 66 67 68 69 70 71 72 73 74
%END LATEX

The first theory, \texttt{List},
declares a new algebraic type for polymorphic lists, \texttt{list 'a}.
As in ML, \texttt{'a} stands for a type variable.
The type \texttt{list 'a} has two constructors, \texttt{Nil} and
\texttt{Cons}. Both constructors can be used as usual function
symbols, respectively of type \texttt{list 'a} and \texttt{'a
  $\times$ list 'a $\rightarrow$ list 'a}.
We deliberately make this theory that short, for reasons which will be
discussed later.
75 76 77 78 79 80

The next theory, \texttt{Length}, introduces the notion of list
length. The \texttt{use import 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
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
81
us to use them without qualification.
82 83 84 85 86 87

Similarly, the next command \texttt{use import 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
either appear earlier in the current file, \eg\ \texttt{List}, or are
88
predefined.
89

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
90
The next declaration defines a recursive function, \texttt{length},
91 92 93
which computes the length of a list. The \texttt{function} and
\texttt{predicate} keywords are used to introduce function and
predicate symbols, respectively.
MARCHE Claude's avatar
MARCHE Claude committed
94
\why checks every recursive, or mutually recursive, definition for
95
termination. Basically, we require a lexicographic and structural
96 97
descent for every recursive call for some reordering of arguments.
Notice that matching must be exhaustive and that every \texttt{match}
98 99
expression must be terminated by the \texttt{end} keyword.

MARCHE Claude's avatar
MARCHE Claude committed
100
Despite using higher-order ``curried'' syntax, \why does not permit
101 102
partial application: function and predicate arities must be respected.

103
The last declaration in theory \texttt{Length} is a lemma stating that
104
the length of a list is non-negative.
105

106 107 108 109 110
The third theory, \texttt{Sorted}, demonstrates the definition of
an inductive predicate. Every such definition is a list of clauses:
universally closed implications where the consequent is an instance
of the defined predicate. Moreover, the defined predicate may only
occur in positive positions in the antecedent. For example, a clause:
111
\begin{whycode}
112 113 114
  | Sorted_Bad :
      forall x y : int, l : list int.
      (sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l))
115
\end{whycode}
116 117
would not be allowed. This positivity condition assures the logical
soundness of an inductive definition.
118

119
Note that the type signature of \lstinline{sorted} predicate does not
120 121
include the name of a parameter (see \texttt{l} in the definition
of \texttt{length}): it is unused and therefore optional.
MARCHE Claude's avatar
doc  
MARCHE Claude committed
122

123
\section{Example 1 (continued): Lists and Abstract Orderings}
124 125 126 127

In the previous section we have seen how a theory can reuse the
declarations of another theory, coming either from the same input
text or from the library. Another way to referring to a theory is
MARCHE Claude's avatar
MARCHE Claude committed
128
by ``cloning''. A \texttt{clone} declaration constructs a local
129
copy of the cloned theory, possibly instantiating some of its
MARCHE Claude's avatar
MARCHE Claude committed
130
abstract (\ie declared but not defined) symbols.
131

132 133 134 135 136 137 138 139 140 141 142
%BEGIN LATEX
Consider the continued example in Figure~\ref{fig:tutorial2}.
%END LATEX
%HEVEA Consider the continued example below.
We write an abstract theory of partial orders, declaring an
abstract type \texttt{t} and an abstract binary predicate
\texttt{<=}. Notice that an infix operation must be enclosed
in parentheses when used outside a term. We also specify
three axioms of a partial order.

%BEGIN LATEX
143 144
\begin{figure}
\centering
145
%END LATEX
146
\begin{whycode}
147 148
theory Order
  type t
149
  predicate (<=) t t
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171

  axiom Le_refl : forall x : t. x <= x
  axiom Le_asym : forall x y : t. x <= y -> y <= x -> x = y
  axiom Le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
end

theory SortedGen
  use import List
  clone import Order as O

  inductive sorted (l : list t) =
    | Sorted_Nil :
        sorted Nil
    | Sorted_One :
        forall x:t. sorted (Cons x Nil)
    | Sorted_Two :
        forall x y : t, l : list t.
        x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
end

theory SortedIntList
  use import int.Int
172
  clone SortedGen with type O.t = int, predicate O.(<=) = (<=)
173
end
174
\end{whycode}
175
%BEGIN LATEX
176 177
\vspace*{-1em}%\hrulefill
\caption{Example of \why text (continued)}
178 179
\label{fig:tutorial2}
\end{figure}
180
%END LATEX
181 182 183 184 185 186 187 188 189 190 191 192 193

There is little value in \texttt{use}'ing such a theory: this
would constrain us to stay with the type \texttt{t}. However,
we can construct an instance of theory \texttt{Order} for
any suitable type and predicate. Moreover, we can build some
further abstract theories using order, and then instantiate
those theories.

Consider theory \texttt{SortedGen}. In the beginning, we
\texttt{use} the earlier theory \texttt{List}. Then we
make a simple \texttt{clone} theory \texttt{Order}.
This is pretty much equivalent to copy-pasting every
declaration from \texttt{Order} to \texttt{SortedGen};
MARCHE Claude's avatar
MARCHE Claude committed
194
the only difference is that \why traces the history
195 196 197 198 199
of cloning and transformations and drivers often make
use of it (see Section~\ref{sec:drivers}).

Notice an important difference between \texttt{use}
and \texttt{clone}. If we \texttt{use} a theory, say
MARCHE Claude's avatar
MARCHE Claude committed
200
\texttt{List}, twice (directly or indirectly: \eg by
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
making \texttt{use} of both \texttt{Length} and
\texttt{Sorted}), there is no duplication: there is
still only one type of lists and a unique pair
of constructors. On the contrary, when we \texttt{clone}
a theory, we create a local copy of every cloned
declaration, and the newly created symbols, despite
having the same names, are different from their originals.

Returning to the example, we finish theory \texttt{SortedGen}
with a familiar definition of predicate \texttt{sorted};
this time we use the abstract order on the values of type
\texttt{t}.

Now, we can instantiate theory \texttt{SortedGen} to any
ordered type, without having to retype the definition of
\texttt{sorted}. For example, theory \texttt{SortedIntList}
MARCHE Claude's avatar
MARCHE Claude committed
217
makes \texttt{clone} of \texttt{SortedGen} (\ie copies its
218 219
declarations) substituting type \texttt{int} for type
\texttt{O.t} of \texttt{SortedGen} and the default order
MARCHE Claude's avatar
MARCHE Claude committed
220
on integers for predicate \texttt{O.(<=)}. \why will
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
control that the result of cloning is well-typed.

Several remarks ought to be made here. First of all, why should
we clone theory \texttt{Order} in \texttt{SortedGen} if we make
no instantiation? Couldn't we write \texttt{use import Order as O}
instead? The answer is no, we could not. When cloning a theory,
we only can instantiate the symbols declared locally in this theory,
not the symbols imported with \texttt{use}. Therefore, we create
a local copy of \texttt{Order} in \texttt{SortedGen} to be able
to instantiate \texttt{t} and \texttt{(<=)} later.

Secondly, when we instantiate an abstract symbol, its declaration
is not copied from the theory being cloned. Thus, we will not create
a second declaration of type \texttt{int} in \texttt{SortedIntList}.

The mechanism of cloning bears some resemblance to modules and functors
MARCHE Claude's avatar
MARCHE Claude committed
237 238
of ML-like languages. Unlike those languages, \why makes no distinction
between modules and module signatures, modules and functors. Any \why
239 240 241 242 243 244 245 246 247 248 249
theory can be \texttt{use}'d directly or instantiated in any of its
abstract symbols.

The command-line tool \texttt{why3} (described in
Section~\ref{sec:batch}), allows us to see the effect of cloning.
If the input file containing our example is called \texttt{lists.why},
we can launch the following command:
\begin{verbatim}
> why3 lists.why -T SortedIntList
\end{verbatim}
to see the resulting theory \texttt{SortedIntList}:
250
\begin{whycode}
251 252 253 254 255 256 257 258 259 260
theory SortedIntList
  (* use BuiltIn *)
  (* use Int *)
  (* use List *)

  axiom Le_refl : forall x:int. x <= x
  axiom Le_asym : forall x:int, y:int. x <= y -> y <= x -> x = y
  axiom Le_trans : forall x:int, y:int, z:int. x <= y -> y <= z
    -> x <= z

261
  (* clone Order with type t = int, predicate (<=) = (<=),
262 263 264 265 266 267 268 269 270
    prop Le_trans1 = Le_trans, prop Le_asym1 = Le_asym,
    prop Le_refl1 = Le_refl *)

  inductive sorted (list int) =
    | Sorted_Nil : sorted (Nil:list int)
    | Sorted_One : forall x:int. sorted (Cons x (Nil:list int))
    | Sorted_Two : forall x:int, y:int, l:list int. x <= y ->
        sorted (Cons y l) -> sorted (Cons x (Cons y l))

271 272
  (* clone SortedGen with type t1 = int, predicate sorted1 = sorted,
    predicate (<=) = (<=), prop Sorted_Two1 = Sorted_Two,
273 274 275 276
    prop Sorted_One1 = Sorted_One, prop Sorted_Nil1 = Sorted_Nil,
    prop Le_trans2 = Le_trans, prop Le_asym2 = Le_asym,
    prop Le_refl2 = Le_refl *)
end
277
\end{whycode}
278 279 280 281 282 283 284 285 286 287 288 289 290

In conclusion, let us briefly explain the concept of namespaces
in \why. Both \texttt{use} and \texttt{clone} instructions can
be used in three forms (the examples below are given for \texttt{use},
the semantics for \texttt{clone} is the same):
\begin{itemize}
\item \texttt{use List as L} --- every symbol $s$ of theory \texttt{List}
is accessible under the name \texttt{L.$s$}. The \texttt{as L} part is
optional, if it is omitted, the name of the symbol is \texttt{List.$s$}.

\item \texttt{use import List as L} --- every symbol $s$ from
\texttt{List} is accessible under the name \texttt{L.$s$}. It is also
accessible simply as \texttt{$s$}, but only up to the end of the current
MARCHE Claude's avatar
MARCHE Claude committed
291
namespace, \eg the current theory. If the current theory, that is the
292 293 294 295 296 297 298 299 300 301 302 303 304
one making \texttt{use}, is later used under the name \texttt{T},
the name of the symbol would be \texttt{T.L.$s$}. (This is why we
could refer directly to the symbols of \texttt{Order} in theory
\texttt{SortedGen}, but had to qualify them with \texttt{O.}
in \texttt{SortedIntList}.)
As in the previous case, \texttt{as L} part is optional.

\item \texttt{use export List} --- every symbol $s$ from \texttt{List}
is accessible simply as \texttt{$s$}. If the current theory
is later used under the name \texttt{T}, the name of the symbol
would be \texttt{T.$s$}.
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
305
\why allows to open new namespaces explicitly in the text. In particular,
306 307
the instruction ``\texttt{clone import Order as O}'' can be equivalently
written as:
308 309 310 311 312
\begin{whycode}
namespace import O
  clone export Order
end
\end{whycode}
313
However, since \why favors short theories over long and complex ones,
314 315
this feature is rarely used.

MARCHE Claude's avatar
doc  
MARCHE Claude committed
316 317 318 319 320 321

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: