un debut de manuel

parent 83c69bf9
\newtheorem{example}{Example}[chapter]
% common Why title page
\newcommand{\whytitlepage}[4]{%
\begin{titlepage}
\begin{center}
~\vfill
\rule\textwidth{0.1cm}\\[0.5cm]
\begin{Huge}\sffamily
#1 % title
\end{Huge}
\\[1cm]
\begin{Large}\sffamily
#2
\end{Large}
\\[0.1cm]
\rule\textwidth{0.1cm}\\[1cm]
Version #3\\[3cm]
#4
\vfill
\today\\
INRIA Team-Project \emph{Proval} \url{http://proval.lri.fr} \\
INRIA Saclay - \^Ile-de-France \& LRI, CNRS UMR 8623\\
4, rue Jacques Monod, 91893 Orsay cedex, France
\end{center}
\end{titlepage}}
\newcommand{\why}{\textsf{Why}}
\newcommand{\Why}{\why}
\newcommand{\java}{\textsc{Java}\index{Java@\textsf{Java}}}
\newcommand{\Java}{\java}
\newcommand{\krakatoa}{\textsf{Krakatoa}\index{Krakatoa@\textsf{Krakatoa}}}
\newcommand{\Krakatoa}{\krakatoa}
\newcommand{\caduceus}{\textsf{Caduceus}\index{Caduceus@\textsf{Caduceus}}}
\newcommand{\Caduceus}{\caduceus}
\newcommand{\coq}{\textsf{Coq}\index{Coq@\textsf{Coq}}}
\newcommand{\Coq}{\coq}
\newcommand{\pvs}{\textsf{PVS}\index{PVS@\textsf{PVS}}}
%
\newcommand{\kw}[1]{\ensuremath{\mathsf{#1}}}
% types
\newcommand{\bool}{\kw{bool}}
\newcommand{\unit}{\kw{unit}}
%\newcommand{\tref}[1]{\ensuremath{#1~\kw{ref}}}
\newcommand{\tref}[1]{\ensuremath{#1~\mathsf{ref}}}
\newcommand{\tarray}[2]{\ensuremath{\kw{array}~#1~\kw{of}~#2}}
% constructs
\newcommand{\prepost}[3]{\ensuremath{\{#1\}\,#2\,\{#3\}}}
\newcommand{\result}{\ensuremath{\mathit{result}}}
\newcommand{\void}{\kw{void}}
\newcommand{\access}[1]{\ensuremath{!#1}}
\newcommand{\assign}[2]{\ensuremath{#1~:=~#2}}
\newcommand{\pref}[1]{\ensuremath{\kw{ref}~#1}}
\newcommand{\taccess}[2]{\ensuremath{#1\texttt{[}#2\texttt{]}}}
\newcommand{\tassign}[3]{\ensuremath{#1\texttt{[}#2\texttt{]}~\texttt{:=}~#3}}
\newcommand{\faccess}[2]{\ensuremath{(\mathit{access}~#1~#2)}}
\newcommand{\fupdate}[3]{\ensuremath{(\mathit{update}~#1~#2~#3)}}
%\newcommand{\taccess}[2]{\ensuremath{#1[#2]}}
%\newcommand{\tassign}[3]{\ensuremath{#1[#2]~:=~#3}}
%\newcommand{\faccess}[2]{\ensuremath{(\mathit{access}~#1~#2)}}
%\newcommand{\fupdate}[3]{\ensuremath{(\mathit{update}~#1~#2~#3)}}
% \newcommand{\block}[1]{\ensuremath{\kw{begin}~#1~\kw{end}}}
\newcommand{\seq}[2]{\ensuremath{#1;~#2}}
%\newcommand{\plabel}[2]{\ensuremath{#1:#2}}
\newcommand{\plabel}[2]{\ensuremath{#1\texttt{:}#2}}
\newcommand{\assert}[2]{\ensuremath{\kw{assert}~\{#1\};~#2}}
\newcommand{\while}[4]{\ensuremath{\kw{while}~#1~\kw{do}~\{\kw{invariant}~#2~\kw{variant}~#3\}~#4~\kw{done}}}
\newcommand{\ite}[3]{\ensuremath{\kw{if}~#1~\kw{then}~#2~\kw{else}~#3}}
\newcommand{\fun}[3]{\ensuremath{\kw{fun}~#1:#2\rightarrow#3}}
\newcommand{\app}[2]{\ensuremath{(#1~#2)}}
\newcommand{\rec}[4]{\ensuremath{\kw{rec}~#1:#2~\{\kw{variant}~#3\}=#4}}
\newcommand{\letin}[3]{\ensuremath{\kw{let}~#1=#2~\kw{in}~#3}}
\newcommand{\raisex}[2]{\ensuremath{\kw{raise}~(#1~#2)}}
\newcommand{\exn}[1]{\ensuremath{\kw{Exn}~#1}}
\newcommand{\try}[2]{\ensuremath{\kw{try}~#1~\kw{with}~#2~\kw{end}}}
\newcommand{\coerce}[2]{\ensuremath{(#1:#2)}}
\newcommand{\statement}{\textit{statement}}
\newcommand{\program}{\textit{program}}
\newcommand{\expression}{\textit{expression}}
\newcommand{\predicate}{\textit{predicate}}
% inference rules
\newcommand{\espacev}{\rule{0in}{1em}}
\newcommand{\espacevn}{\rule[-0.4em]{0in}{1em}}
\newcommand{\irule}[2]
{\frac{\espacevn\displaystyle#1}{\espacev\displaystyle#2}}
\newcommand{\typage}[3]{#1 \, \vdash \, #2 : #3}
\newcommand{\iname}[1]{\textsf{#1}}
\newcommand{\emptyef}{\bot}
\newcommand{\wf}[1]{#1~\kw{wf}}
\newcommand{\pur}[1]{#1~\kw{pure}}
\newcommand{\variant}[1]{#1~\kw{variant}}
\newcommand{\wpre}[2]{\ensuremath{\mathit{wp}(#1,#2)}}
\newcommand{\wprx}[3]{\ensuremath{\mathit{wp}(#1,#2,#3)}}
\newcommand{\barre}[1]{\ensuremath{\overline{#1}}}
% backslash keywords
\newcommand{\ttkw}[1]{\texttt{#1}}
\newcommand{\bskw}[1]{\ttkw{\char'134 #1}}
\newcommand{\bkw}[1]{\ttkw{\textbf{#1}}}
\newcommand{\caml}{\textsf{Caml}}
\newcommand{\ergo}{\textsf{Ergo}\index{Ergo@\textsf{Ergo}}}
\newcommand{\yices}{\textsf{Yices}\index{Yices@\textsf{Yices}}}
\newcommand{\harvey}{\textsf{haRVey}\index{haRVey@\textsf{haRVey}}}
\newcommand{\simplify}{\textsf{Simplify}\index{Simplify@\textsf{Simplify}}}
\newcommand{\mizar}{\textsf{Mizar}\index{Mizar@\textsf{Mizar}}}
\newcommand{\hollight}{\textsf{HOL Light}\index{HOL Light@\textsf{HOL Light}}}
\newcommand{\isabelle}{\textsf{Isabelle/HOL}\index{Isabelle/HOL@\textsf{Isabelle/HOL}}}
\newcommand{\holfour}{\textsf{HOL 4}\index{HOL 4@\textsf{HOL 4}}}
\newcommand{\cvclite}{\textsf{CVC Lite}\index{CVC Lite@\textsf{CVC Lite}}}
\newcommand{\cvcthree}{\textsf{CVC 3}\index{CVC 3@\textsf{CVC 3}}}
\newcommand{\zenon}{\textsf{Zenon}\index{Zenon@\textsf{Zenon}}}
\newcommand{\jml}{\textsc{JML}\index{JML@\textsf{JML}}}
\newcommand{\caveat}{\paragraph{Caveat.}}
\newcommand{\caveats}{\paragraph{Caveats.}}
% BNF syntax
\newenvironment{syntax}{\begin{tabular}{lrll}}{\end{tabular}}
\newcommand{\te}[1]{\texttt{#1}}
\newcommand{\nt}[1]{$\langle$\textsl{#1}$\rangle$}
\newcommand{\indexnt}[1]{\index{#1@\textsl{#1}, grammar entry}}
\newcommand{\indextt}[1]{\index{#1@\texttt{#1}}}
\newcommand{\repstar}{$^{\star}$}
\newcommand{\repstarsep}[1]{$^{\star}_#1$}
\newcommand{\repplus}{$^+$}
\newcommand{\repplussep}[1]{$^+_#1$}
\newcommand{\orelse}{$\mid$}
\newcommand{\is}{ & $::=$ &}
\newcommand{\newl}{ \\ & $|$ &}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "doc"
%%% End:
\documentclass[a4paper,12pt]{report}
\usepackage{fullpage}
\usepackage{url}
\usepackage{makeidx}
\usepackage{verbatim}
\usepackage{graphicx}
\input{./version.tex}
\input{./macros.tex}
\makeindex
\begin{document}
%%% coverpage
\whytitlepage{The WHY verification tool}{Tutorial and Reference
Manual}{\whyversion}{Team-Project ProVal}
\tableofcontents
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter*{Foreword}
\addcontentsline{toc}{chapter}{Foreword}
\subsection*{License}
The \why\ tool is \copyright\ 2002--2010 team-project ProVal
(\url{proval.lri.fr}).
It is open source and freely available under the terms of the Gnu
Library General Public License Version 2.1 (see the file
\texttt{LICENSE} included in the distribution).
\subsection*{Availability}
The \why\ tool is available from \url{http://why.lri.fr/}, in source
and binary formats, together with this documentation and many
examples.
\subsection*{Contact}
There is a mailing list for \why;
see \url{http://lists.lri.fr/mailman/listinfo/why}.
% TODO BTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Syntax of input files}
\label{syntax}
\section{Lexical conventions}
Comments are opened with \texttt{(*}, closed
with \texttt{*)} and can be nested.
Identifiers are made of letters, digits,
the underscore character \texttt{\_} and the single quote \texttt{'},
starting with a letter. In many cases, identifiers starting with
lowercase or uppercase characters are distinguished.
\begin{center}\framebox{\begin{syntax}
\nt{lident}\indexnt{lident}
\is \te{a}..\te{z} \nt{ident\_char}\repstar \\
\nt{uident}\indexnt{uident}
\is \te{A}..\te{Z} \nt{ident\_char}\repstar \\
\nt{ident\_char}
\is \te{A}..\te{Z} \orelse \te{a}..\te{z} \orelse
\te{0}..\te{9} \orelse \te{\_} \orelse \te{'} \\[0.1em]
\nt{ident}
\is \nt{lident} \orelse\ \nt{uident}
\end{syntax}}\end{center}
Keywords are the following:
\begin{center}
{\tt\begin{tabular}{l@{\qquad}l@{\qquad}l@{\qquad}l@{\qquad}l}
absurd &
and &
array &
as &
assert \\
axiom &
begin &
bool &
do &
done \\
else &
end &
exception &
exists &
external \\
false &
for &
forall &
fun &
function \\
goal &
if &
in &
int &
invariant \\
% label &
let &
logic &
not &
of \\
or &
parameter &
predicate &
prop &
raise \\
raises &
reads &
real &
rec &
ref \\
returns &
then &
true &
try &
type \\
unit &
variant &
void &
while &
with \\
writes &
\end{tabular}}
\end{center}
\section{Grammar}
\subsection{Qualified names}
\begin{center}\framebox{\begin{syntax}
\nt{lqualid} \is
\end{syntax}}\end{center}
\subsection{Terms}
\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
\nt{term}\indexnt{term}
\is \nt{constant}
\newl \nt{term} \nt{arith\_op} \nt{term} \\
& $|$ & \te{-} \nt{term} \\
& $|$ & \nt{lab\_identifier} \\
& $|$ & \nt{identifier} \te{(} \nt{term}\repplussep{\te{,}} \te{)} \\
& $|$ & \nt{lab\_identifier} \te{[} \nt{term} \te{]} \\
& $|$ & \te{if} \nt{term} \te{then} \nt{term} \te{else} \nt{term} \\
& $|$ & \te{let} \nt{identifier} \te{=} \nt{term} \te{in} \nt{term} \\
& $|$ & \te{(} \nt{term} \te{)} \\
\\[0.1em]
\nt{constant}\indexnt{constant}
& $::=$ & \nt{integer-constant} \\
& $|$ & \nt{real-constant} \\
\end{tabular}\\
\hrulefill
\caption{Syntax of terms}
\label{fig:terms}
\end{center}
\end{figure}
\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
\nt{predicate}\indexnt{predicate}
& $::=$ & \te{true} \\
& $|$ & \te{false} \\
& $|$ & \nt{identifier} \\
& $|$ & \nt{identifier} \te{(} \nt{term}\repplussep{\te{,}} \te{)} \\
& $|$ & \nt{term} \nt{relation} \nt{term}
$[$ \nt{relation} \nt{term} $]$ \\
& $|$ & \nt{predicate} \te{->} \nt{predicate} \\
& $|$ & \nt{predicate} \te{<->} \nt{predicate} \\
& $|$ & \nt{predicate} \te{or} \nt{predicate} \\
& $|$ & \nt{predicate} \te{and} \nt{predicate} \\
& $|$ & \te{not} \nt{predicate} \\
& $|$ & \te{if} \nt{term} \te{then} \nt{predicate}
\te{else} \nt{predicate} \\
& $|$ & \te{let} \nt{identifier} \te{=} \nt{term}
\te{in} \nt{predicate} \\
& $|$ & \te{forall} \nt{identifier}\repplussep{\te{,}}
\te{:} \nt{primitive\_type} $[$ \nt{triggers} $]$
\te{.} \nt{predicate} \\
& $|$ & \te{exists} \nt{identifier}\repplussep{\te{,}}
\te{:} \nt{primitive\_type}
\te{.} \nt{predicate} \\
& $|$ & \te{(} \nt{predicate} \te{)} \\
& $|$ & (\nt{identifier} $|$ \nt{string}) \te{:} \nt{predicate} \\
\\[0.1em]
\nt{triggers}
& $::=$ & \te{[} \nt{trigger}\repplussep{\te{|}} \te{]} \\
\nt{trigger}
& $::=$ & \nt{term}\repplussep{\te{,}} \\
\\[0.1em]
\nt{primitive\_type}\indexnt{primitive\_type}
& $::=$ & \te{int} $|$ \te{bool} $|$ \te{real} $|$
\te{unit} $|$ \nt{identifier} $|$ \te{'} \nt{identifier} \\
& $|$ & \nt{primitive\_type} \nt{identifier} $|$ \te{(}
\nt{primitive\_type}\repstarsep{\te{,}} \te{)} \nt{identifier} \\
\\[0.1em]
\nt{relation}\indexnt{relation}
& $::=$ & \te{=} $|$ \te{<>} $|$
\te{<} $|$ \te{<=} $|$ \te{>} $|$ \te{>=}
\end{tabular}\\
\hrulefill
\caption{Syntax of predicates}
\label{fig:predicates}
\end{center}
\end{figure}
\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
\nt{l\_declaration}
& $::=$ & $[$ \te{external} $]$ \te{type} $[$ \nt{type\_parameters} $]$
\nt{identifier} \\\indextt{type} \indextt{external}
& $|$ & $[$ \te{external} $]$ \te{logic} \nt{identifier}\repplussep{\te{,}}
\te{:} \nt{logic\_type} \\\indextt{logic} \indextt{external}
& $|$ & \te{function} \nt{identifier}
\te{(} \nt{logic\_binder}\repstarsep{\te{,}}
\te{)} \te{:} \nt{primitive\_type} \\
& & \te{=} \nt{term} \\ \indextt{function}
& $|$ & \te{predicate} \nt{identifier}
\te{(} \nt{logic\_binder}\repstarsep{\te{,}}
\te{)} \te{=} \nt{predicate} \\ \indextt{predicate}
& $|$ & \te{inductive} \nt{identifier}
\te{:} \nt{logic\_type} \te{=}\\
& &(\te{|} \nt{identifier} \te{:} \nt{predicate})\repstar{}
\te{\}} \\ \indextt{predicate}
& $|$ & \te{axiom} \nt{identifier} \te{:}
\nt{predicate} \\\indextt{axiom}
& $|$ & \te{goal} \nt{identifier} \te{:}
\nt{predicate} \\\indextt{goal}
\\[0.1em]
\nt{logic\_type}
& $::=$ & \nt{logic\_arg\_type}\repstarsep{\te{,}} \te{->} \te{prop}
\\ \indextt{prop}
& $|$ & \nt{logic\_arg\_type}\repstarsep{\te{,}} \te{->}
\nt{primitive\_type} \\ \indextt{logic}
\\[0.1em]
\nt{logic\_arg\_type}
& $::=$ & \nt{primitive\_type} $|$ \nt{primitive\_type} \te{array} \\
\\[0.1em]
\nt{logic\_binder}
& $::=$ & \nt{identifier} \te{:} \nt{primitive\_type} \\
\\[0.1em]
\nt{type\_parameters}
& $::=$ & \te{'}\nt{identifier} $|$
\te{(} (\te{'}\nt{identifier})\repplussep{\te{,}} \te{)}
\end{tabular}\\
\hrulefill
\caption{Syntax of logic declarations}
\label{fig:ldecl}
\end{center}
\end{figure}
\subsubsection{Programs}
Syntax of types is given Figure~\ref{fig:types}.
Syntax of annotated programs is given Figure~\ref{fig:caml}.
Syntax of input files is given Figure~\ref{fig:input}.
\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
\nt{simple\_value\_type}\indexnt{simple\_value\_type}
& $::=$ & \nt{primitive\_type} \\
& $|$ & \nt{primitive\_type} \te{ref} \\
& $|$ & \nt{primitive\_type} \te{array} \\
& $|$ & \te{(} \nt{value\_type} \te{)} \\
\\[0.1em]
\nt{value\_type}\indexnt{value\_type}
& $::=$ & \nt{simple\_value\_type} \\
& $|$ & \nt{simple\_value\_type} \te{->} \nt{computation\_type} \\
& $|$ & \nt{identifier} \te{:} \nt{simple\_value\_type}
\te{->} \nt{computation\_type} \\
\\[0.1em]
\nt{computation\_type}\indexnt{computation\_type}
& $::=$ & \te{\{} $[$ \nt{precondition} $]$ \te{\}} \\
& & $[$ \te{returns} \nt{identifier} \te{:} $]$ \nt{value\_type}
\nt{effects} \\
& & \te{\{} $[$ \nt{postcondition} $]$ \te{\}} \\
& $|$ & \nt{value\_type} \\
\\[0.1em]
\nt{effects}
& $::=$ & $[$ \te{reads} \nt{identifier}\repstarsep{\te{,}} $]$
$[$ \te{writes} \nt{identifier}\repstarsep{\te{,}} $]$
$[$ \te{raises} \nt{identifier}\repstarsep{\te{,}} $]$ \\
\\[0.1em]
\nt{precondition}\indexnt{precondition}
& $::=$ & \nt{assertion} \\
\\[0.1em]
\nt{postcondition}\indexnt{postcondition}
& $::=$ & \nt{assertion} \nt{exn\_condition}\repstar \\
\\[0.1em]
\nt{exn\_condition}
& $::=$ & \te{|} \nt{identifier} \te{=>} \nt{assertion} \\
\\[0.1em]
\nt{assertion}
& $::=$ & \nt{predicate} $[$ \te{as} \nt{identifier} $]$ \\
\end{tabular}\\
\hrulefill
\caption{Syntax of types}
\label{fig:types}
\end{center}
\end{figure}
\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
\nt{prog}\indexnt{prog}
& $::=$ & \nt{constant} \\
& $|$ & \nt{identifier} \\
& $|$ & \te{!} \nt{identifier} \\
& $|$ & \nt{identifier} \te{:=} \nt{prog} \\
& $|$ & \nt{identifier} \te{[} \nt{prog} \te{]} \\
& $|$ & \nt{identifier} \te{[} \nt{prog} \te{]} \te{:=} \nt{prog} \\
& $|$ & \nt{prog} \nt{infix} \nt{prog} \\
& $|$ & \nt{prefix} \nt{prog} \\
& $|$ & \te{let} \nt{identifier} \te{=} \nt{prog}
\te{in} \nt{prog} \\
& $|$ & \te{let} \nt{identifier} \te{=} \te{ref}
\nt{prog} \te{in} \nt{prog} \\
& $|$ & \te{if} \nt{prog} \te{then} \nt{prog}
$[$ \te{else} \nt{prog} $]$ \\
& $|$ & \te{while} \nt{prog} \te{do}
[ \nt{loop\_annot} ] \nt{prog} \te{done} \\
& $|$ & \nt{prog} \te{;} \nt{prog} \\
& $|$ & \nt{identifier} \te{:} \nt{prog} \\
& $|$ & \te{assert} (\te{\{} \nt{assertion} \te{\}})\repplus\
\te{;} \nt{prog} \\
& $|$ & \nt{prog} \te{\{}\ \nt{postcondition} \te{\}} \\
& $|$ & \nt{prog} \te{\{\{}\ \nt{postcondition} \te{\}\}} \\
& $|$ & \te{fun} \nt{binders} \te{->} \nt{prog} \\
& $|$ & \te{let} \nt{identifier} \nt{binders} \te{=} \nt{prog}
\te{in} \nt{prog} \\
& $|$ & \te{let} \te{rec} \nt{recfun} $[$ \te{in} \nt{prog} $]$ \\
& $|$ & \nt{prog} \nt{prog} \\
& $|$ & \te{raise} \nt{identifier} $[$ \te{:} \nt{value\_type} $]$ \\
& $|$ & \te{raise} \te{(} \nt{identifier} \nt{prog} \te{)}
$[$ \te{:} \nt{value\_type} $]$ \\
& $|$ & \te{try} \nt{prog} \te{with}
\nt{handler}\repplussep{\te{|}} \te{end} \\
& $|$ & \te{absurd} $[$ \te{:} \nt{value\_type} $]$ \\ \indextt{absurd}
& $|$ & \te{(} \nt{prog} \te{)} \\
& $|$ & \te{begin} \nt{prog} \te{end} \\
\\[0.1em]
\nt{infix}
& $::=$ & \te{+} $|$ \te{-} $|$ \te{*} $|$ \te{/} $|$ \te{\%} $|$
\te{=} $|$ \te{<>} $|$
\te{<} $|$ \te{<=} $|$ \te{>} $|$ \te{>=} $|$
\te{||} $|$ \te{\&\&} \\
\nt{prefix}
& $::=$ & \te{-} $|$ \te{not} \\
\\[0.1em]
\nt{binders}\indexnt{binders}
& $::=$ & \te{(} \nt{identifier}\repplussep{\te{,}} \te{:}
\nt{value\_type} \te{)}\repplus \\
\\[0.1em]
\nt{recfun}
& $::=$ & \nt{identifier} \nt{binders} \te{:}
value\_type \\
& & \te{\{} \te{variant} \nt{wf\_arg} \te{\}}
\te{=} \nt{prog} \\
\\[0.1em]
\nt{loop\_annot}
& $::=$ & \te{\{} [ \te{invariant} \nt{assertion} ]
[ \te{variant} \nt{wf\_arg} ] \te{\}} \\
\\[0.1em]
\nt{wf\_arg}
& $::=$ & \nt{term} $[$ \te{for} \nt{identifier} $]$ \\
\\[0.1em]
\nt{handler}\indexnt{handler}
& $::=$ & \nt{identifier} \te{->} \nt{prog} \\
& $|$ & \nt{identifier} \nt{identifier} \te{->} \nt{prog} \\
\end{tabular}\\
\hrulefill\caption{Syntax of annotated programs}
\label{fig:caml}
\end{center}
\end{figure}
\begin{figure}[htbp]
\begin{center}
\hrulefill\\
\begin{tabular}{lrl}
\nt{file}
& $::=$ & \nt{declaration}\repstar\ \\
\\[0.1em]
\nt{declaration}
& $::=$ & \te{let} \nt{identifier} $[$ \nt{binders} $]$ \te{=} \nt{prog} \\
& $|$ & \te{let} \te{rec} \nt{recfun} \\
& $|$ & $[$ \te{external} $]$
\te{parameter} \nt{identifier}\repplussep{\te{,}}
\te{:} \nt{value\_type} \\ \indextt{parameter}\indextt{external}
& $|$ & \te{exception} \nt{identifier}
$[$ \te{of} \nt{primitive\_type} $]$ \\ \indextt{exception}
& $|$ & \nt{l\_declaration}
\end{tabular}\\
\hrulefill
\caption{Syntax of input files}
\label{fig:input}
\end{center}
\end{figure}
\section{Semantics}\label{semantics}\index{Semantics}
\subsection{Logic}\label{semantics:logic}
The abstract syntax for types ($\tau$), terms ($t$) and predicates
($P$) is given by the following grammars:
\begin{displaymath}
\begin{array}{rrl}
\tau & ~::=~ & \alpha ~|~ (\tau,\dots,\tau)~s \\
t & ~::=~ & x ~|~ f(t,\dots,t) \\
P & ~::=~ & p(t,\dots,t) \\
& |~~ & \top ~|~ \bot ~|~ P \land P ~|~ P \lor P
~|~ \lnot P ~|~ P\Rightarrow P \\
& |~~ & \forall x:\tau.\,P ~|~ \exists x:\tau.\,P
\end{array}
\end{displaymath}
A theory $\Sigma$ is a finite list of declarations $\delta$ where
\begin{displaymath}
\begin{array}{rrl}
\delta & ~::=~ &
\texttt{type}~\vec{\alpha}~s ~|~ x:\tau ~|~
\mathtt{logic}~f:\forall\vec{\alpha}.\,\tau,\dots,\tau\rightarrow\tau \\
& |~~ &
\mathtt{logic}~p:\forall\vec{\alpha}.\,\tau,\dots,\tau\rightarrow\mathtt{prop} ~|~
\texttt{axiom}~\forall\vec{\alpha}.\,P ~|~
\texttt{goal}~\forall\vec{\alpha}.\,P \\
\end{array}
\end{displaymath}
\subsubsection{Typing}
\newcommand{\Subst}[2]{\ensuremath{\mathsf{Subst}(#1,#2)}}
Well-formed types ($\Sigma\vdash\wf{\tau}$):
% types wf
\begin{displaymath}
\frac{}{\Sigma\vdash\wf{\alpha}}(\mathsf{Ty}_1)
\qquad
\frac{\mathtt{type}~(\alpha_1,\dots,\alpha_n)~s\in\Sigma
\quad
\forall i,\,\Sigma\vdash\wf{\tau_i}}
{\Sigma\vdash\wf{(\tau_1,\dots,\tau_n)~s}}(\mathsf{Ty}_2)
\end{displaymath}
Well-typed terms ($\Sigma\vdash t:\tau$):
\begin{displaymath}
\frac{x:\tau\in\Sigma}{\Sigma\vdash x:\tau}(\mathsf{T}_1)
\qquad
\frac{
\begin{array}{c}
\texttt{logic}~f:\forall\vec{\alpha}.\,\tau_1,\dots,\tau_n\rightarrow\tau\in\Sigma \\[0.2em]
\Subst{\sigma}{\Sigma} \quad
\forall i,\, \Sigma\vdash t_i:\sigma(\tau_i) \\
\end{array}}
{\Sigma\vdash f(t_1,\dots,t_n):\sigma(\tau)}(\mathsf{T}_2)
\end{displaymath}
\begin{description}
\item[~~~]
where $\sigma$ is a mapping from type variables to types, naturally
extended to types with $\sigma((\tau_1,\dots,\tau_n)~s) =
(\sigma(\tau_1),\dots,\sigma(\tau_n))~s$.
We write $\Subst{\sigma}{\Sigma}$ whenever
$\Sigma\vdash\wf{\sigma(\alpha)}$ holds for any type variable $\alpha$.
\end{description}
Well-typed predicates ($\Sigma\vdash\wf{P}$):
\begin{displaymath}
\frac{
\begin{array}{c}
\texttt{logic}~p:\forall\vec{\alpha}.\,\tau_1,\dots,\tau_n\rightarrow\mathtt{prop}\in\Sigma \quad
\Subst{\sigma}{\Sigma} \quad
\forall i,\,\Sigma\vdash t_i:\sigma(\tau_i) \\
\end{array}}
{\Sigma\vdash\wf{p(t_1,\dots,t_n)}}(\mathsf{P}_1)
\end{displaymath}
\begin{displaymath}
\frac{}
{\Sigma\vdash\wf{\top}}(\mathsf{P}_2)
\qquad
\frac{}
{\Sigma\vdash\wf{\bot}}(\mathsf{P}_3)
\qquad
\frac{\Sigma\vdash\wf{P_1} \quad \Sigma\vdash\wf{P_2}}
{\Sigma\vdash\wf{P_1\land P_2}}(\mathsf{P}_4)