\chapter{The \why Language} \label{chap:syntax} %HEVEA\cutname{syntax.html} This chapter describes the input syntax, and informally gives its semantics, illustrated by examples. A \why text contains a list of \emph{theories}. A theory is a list of \emph{declarations}. Declarations introduce new types, functions and predicates, state axioms, lemmas and goals. These declarations can be directly written in the theory or taken from existing theories. The base logic of \why is first-order logic with polymorphic types. \section{Example 1: Lists} %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. %BEGIN LATEX \begin{figure} \centering %END LATEX \begin{whycode} theory List type list 'a = Nil | Cons 'a (list 'a) end theory Length use import List use import int.Int function length (l : list 'a) : int = match l with | Nil -> 0 | Cons _ r -> 1 + length r end lemma Length_nonnegative : forall l:list 'a. length l >= 0 end theory Sorted use import List use import int.Int inductive sorted (list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Example of \why text} \label{fig:tutorial1} \end{figure} %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. 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 us to use them without qualification. 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 predefined. The next declaration defines a recursive function, \texttt{length}, which computes the length of a list. The \texttt{function} and \texttt{predicate} keywords are used to introduce function and predicate symbols, respectively. \why checks every recursive, or mutually recursive, definition for termination. Basically, we require a lexicographic and structural descent for every recursive call for some reordering of arguments. Notice that matching must be exhaustive and that every \texttt{match} expression must be terminated by the \texttt{end} keyword. Despite using higher-order curried'' syntax, \why does not permit partial application: function and predicate arities must be respected. The last declaration in theory \texttt{Length} is a lemma stating that the length of a list is non-negative. 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: \begin{whycode} | Sorted_Bad : forall x y : int, l : list int. (sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l)) \end{whycode} would not be allowed. This positivity condition assures the logical soundness of an inductive definition. Note that the type signature of \lstinline{sorted} predicate does not include the name of a parameter (see \texttt{l} in the definition of \texttt{length}): it is unused and therefore optional. \section{Example 1 (continued): Lists and Abstract Orderings} 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 by cloning''. A \texttt{clone} declaration constructs a local copy of the cloned theory, possibly instantiating some of its abstract (\ie declared but not defined) symbols. %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 \begin{figure} \centering %END LATEX \begin{whycode} theory Order type t predicate (<=) t t 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 clone SortedGen with type O.t = int, predicate O.(<=) = (<=) end \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Example of \why text (continued)} \label{fig:tutorial2} \end{figure} %END LATEX 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}; the only difference is that \why traces the history 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 \texttt{List}, twice (directly or indirectly: \eg by 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} makes \texttt{clone} of \texttt{SortedGen} (\ie copies its declarations) substituting type \texttt{int} for type \texttt{O.t} of \texttt{SortedGen} and the default order on integers for predicate \texttt{O.(<=)}. \why will 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 of ML-like languages. Unlike those languages, \why makes no distinction between modules and module signatures, modules and functors. Any \why 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}: \begin{whycode} 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 (* clone Order with type t = int, predicate (<=) = (<=), 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)) (* clone SortedGen with type t1 = int, predicate sorted1 = sorted, predicate (<=) = (<=), prop Sorted_Two1 = Sorted_Two, 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 \end{whycode} 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 namespace, \eg the current theory. If the current theory, that is the 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} \why allows to open new namespaces explicitly in the text. In particular, the instruction \texttt{clone import Order as O}'' can be equivalently written as: \begin{whycode} namespace import O clone export Order end \end{whycode} However, since \why favors short theories over long and complex ones, this feature is rarely used. %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: