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

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

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

14
\section{Example 1: Lists}
15

16 17 18 19 20
%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.
21

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

theory Length
  use import List
  use import int.Int

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

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

theory Sorted
  use import List
  use import int.Int
47

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

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 Filliâtre's avatar
Jean-Christophe Filliâtre committed
80
us to use them without qualification.
81 82 83 84 85 86

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
87
predefined.
88

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89
The next declaration defines a recursive function, \texttt{length},
90 91 92
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
93
\why checks every recursive, or mutually recursive, definition for
94
termination. Basically, we require a lexicographic and structural
95 96
descent for every recursive call for some reordering of arguments.
Notice that matching must be exhaustive and that every \texttt{match}
97 98
expression must be terminated by the \texttt{end} keyword.

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

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

105 106 107 108 109
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:
110
\begin{whycode}
111 112 113
  | Sorted_Bad :
      forall x y : int, l : list int.
      (sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l))
114
\end{whycode}
115 116
would not be allowed. This positivity condition assures the logical
soundness of an inductive definition.
117

118
Note that the type signature of \lstinline{sorted} predicate does not
119 120
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
121

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

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
127
by ``cloning''. A \texttt{clone} declaration constructs a local
128
copy of the cloned theory, possibly instantiating some of its
MARCHE Claude's avatar
MARCHE Claude committed
129
abstract (\ie declared but not defined) symbols.
130

131 132 133 134 135 136 137 138 139 140 141
%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
142 143
\begin{figure}
\centering
144
%END LATEX
145
\begin{whycode}
146 147
theory Order
  type t
148
  predicate (<=) t t
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170

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

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
193
the only difference is that \why traces the history
194 195 196 197 198
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
199
\texttt{List}, twice (directly or indirectly: \eg by
200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215
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
216
makes \texttt{clone} of \texttt{SortedGen} (\ie copies its
217 218
declarations) substituting type \texttt{int} for type
\texttt{O.t} of \texttt{SortedGen} and the default order
MARCHE Claude's avatar
MARCHE Claude committed
219
on integers for predicate \texttt{O.(<=)}. \why will
220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
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
236 237
of ML-like languages. Unlike those languages, \why makes no distinction
between modules and module signatures, modules and functors. Any \why
238 239 240 241 242 243 244 245 246 247 248
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}:
249
\begin{whycode}
250 251 252 253 254 255 256 257 258 259
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

260
  (* clone Order with type t = int, predicate (<=) = (<=),
261 262 263 264 265 266 267 268 269
    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))

270 271
  (* clone SortedGen with type t1 = int, predicate sorted1 = sorted,
    predicate (<=) = (<=), prop Sorted_Two1 = Sorted_Two,
272 273 274 275
    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
276
\end{whycode}
277 278 279 280 281 282 283 284 285 286 287 288 289

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
290
namespace, \eg the current theory. If the current theory, that is the
291 292 293 294 295 296 297 298 299 300 301 302 303
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
304
\why allows to open new namespaces explicitly in the text. In particular,
305 306
the instruction ``\texttt{clone import Order as O}'' can be equivalently
written as:
307 308 309 310 311
\begin{whycode}
namespace import O
  clone export Order
end
\end{whycode}
312
However, since \why favors short theories over long and complex ones,
313 314
this feature is rarely used.

315
\section{Example 2: Einstein's Problem}
316 317
\index{Einstein's logic problem}

MARCHE Claude's avatar
MARCHE Claude committed
318
We now consider another, slightly more complex example: how to use \why
319
to solve a little puzzle known as ``Einstein's logic
320 321 322 323 324
problem''.%
%BEGIN LATEX
\footnote{This \why example was contributed by St\'ephane Lescuyer.}
%END LATEX
%HEVEA {} (This \why example was contributed by St\'ephane Lescuyer.)
325 326 327
The code given below is available in the source distribution in
directory \verb|examples/logic/einstein.why|.

328 329 330
The problem is stated as follows. Five persons, of five
different nationalities, live in five houses in a row, all
painted with different colors.
331
These five persons own different pets, drink different beverages and
332 333
smoke different brands of cigars.
We are given the following information:
334
\begin{itemize}
335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363
\item The Englishman lives in a red house;

\item The Swede has dogs;

\item The Dane drinks tea;

\item The green house is on the left of the white one;

\item The green house's owner drinks coffee;

\item The person who smokes Pall Mall has birds;

\item The yellow house's owner smokes Dunhill;

\item In the house in the center lives someone who drinks milk;

\item The Norwegian lives in the first house;

\item The man who smokes Blends lives next to the one who has cats;

\item The man who owns a horse lives next to the one who smokes Dunhills;

\item The man who smokes Blue Masters drinks beer;

\item The German smokes Prince;

\item The Norwegian lives next to the blue house;

\item The man who smokes Blends has a neighbour who drinks water.
364 365 366 367 368 369 370
\end{itemize}
The question is: what is the nationality of the fish's owner?

We start by introducing a general-purpose theory defining the notion
of \emph{bijection}, as two abstract types together with two functions from
one to the other and two axioms stating that these functions are
inverse of each other.
371
\begin{whycode}
372 373 374 375
theory Bijection
  type t
  type u

376
  function of t : u
377
  function to_ u : t
378

379 380
  axiom To_of : forall x : t. to_ (of x) = x
  axiom Of_to : forall y : u. of (to_ y) = y
381
end
382
\end{whycode}
383 384 385

We now start a new theory, \texttt{Einstein}, which will contain all
the individuals of the problem.
386
\begin{whycode}
387
theory Einstein "Einstein's problem"
388
\end{whycode}
389 390
First we introduce enumeration types for houses, colors, persons,
drinks, cigars and pets.
391
\begin{whycode}
392 393 394 395 396 397
  type house  = H1 | H2 | H3 | H4 | H5
  type color  = Blue | Green | Red | White | Yellow
  type person = Dane | Englishman | German | Norwegian | Swede
  type drink  = Beer | Coffee | Milk | Tea | Water
  type cigar  = Blend | BlueMaster | Dunhill | PallMall | Prince
  type pet    = Birds | Cats | Dogs | Fish | Horse
398
\end{whycode}
399 400
We now express that each house is associated bijectively to a color,
by cloning the \texttt{Bijection} theory appropriately.
401
\begin{whycode}
402
  clone Bijection as Color with type t = house, type u = color
403
\end{whycode}
404
It introduces two functions, namely \texttt{Color.of} and
405
\texttt{Color.to\_}, from houses to colors and colors to houses,
406 407 408
respectively, and the two axioms relating them.
Similarly, we express that each house is associated bijectively to a
person
409
\begin{whycode}
410
  clone Bijection as Owner with type t = house, type u = person
411
\end{whycode}
412
and that drinks, cigars and pets are all associated bijectively to persons:
413
\begin{whycode}
414 415 416
  clone Bijection as Drink with type t = person, type u = drink
  clone Bijection as Cigar with type t = person, type u = cigar
  clone Bijection as Pet   with type t = person, type u = pet
417
\end{whycode}
418 419
Next we need a way to state that a person lives next to another. We
first define a predicate \texttt{leftof} over two houses.
420
\begin{whycode}
421
  predicate leftof (h1 h2 : house) =
422
    match h1, h2 with
423 424 425
    | H1, H2
    | H2, H3
    | H3, H4
426 427 428
    | H4, H5 -> true
    | _      -> false
    end
429
\end{whycode}
430
Note how we advantageously used pattern matching, with an or-pattern
431 432 433
for the four positive cases and a universal pattern for the remaining
21 cases. It is then immediate to define a \texttt{neighbour}
predicate over two houses, which completes theory \texttt{Einstein}.
434
\begin{whycode}
435
  predicate rightof (h1 h2 : house) =
436
    leftof h2 h1
437 438
  predicate neighbour (h1 h2 : house) =
    leftof h1 h2 \/ rightof h1 h2
439
end
440
\end{whycode}
441 442 443

The next theory contains the 15 hypotheses. It starts by importing
theory \texttt{Einstein}.
444
\begin{whycode}
445 446
theory EinsteinHints "Hints"
  use import Einstein
447
\end{whycode}
448
Then each hypothesis is stated in terms of \texttt{to\_} and \texttt{of}
449 450
functions. For instance, the hypothesis ``The Englishman lives in a
red house'' is declared as the following axiom.
451
\begin{whycode}
452
  axiom Hint1: Color.of (Owner.to_ Englishman) = Red
453
\end{whycode}
454 455 456
And so on for all other hypotheses, up to
``The man who smokes Blends has a neighbour who drinks water'', which completes
this theory.
457
\begin{whycode}
458 459
  ...
  axiom Hint15:
460
    neighbour (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Drink.to_ Water))
461
end
462
\end{whycode}
463
Finally, we declare the goal in the fourth theory:
464
\begin{whycode}
465 466 467
theory Problem "Goal of Einstein's problem"
  use import Einstein
  use import EinsteinHints
468

469
  goal G: Pet.to_ Fish = German
470
end
471
\end{whycode}
MARCHE Claude's avatar
MARCHE Claude committed
472
and we are ready to use \why to discharge this goal with any prover
473
of our choice.
MARCHE Claude's avatar
doc  
MARCHE Claude committed
474 475 476 477 478 479

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