Commit a706e1cd authored by MARCHE Claude's avatar MARCHE Claude
Browse files

manual for why3

parent 7e74b5cb
\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}
%% file := decl*
%% decl := | "theory" uident decl* "end"
%% | "theory" uident "." uqualid ("with" instance+ )?
%% | "use" ("open" | "include")? uqualid ("as" ident)
%% | ("axiom"|"lemma"|"goal") ident ":" fmla
%% | "type" typarams lident ("=" (ty-alg | ty))?
%% ("and" typarams lident ("=" (ty-alg | ty))?)*
%% Il faut verifier qu'il y a toujours un constructeur entre deux
%% définitions récursives.
%% | "logic" def ("and" def)*
%% | "inductive" ...
%% def := lident_ou_infix ("(" formal+, ")")? (":" ty)? ("=" lexpr)?
%% formal := ((lident|_)":")? ty
%% instance := | lqualid "=" lqualid
%% ty-alg := | uident ("(" ty,+ ")")? ("|" uident ...)*
\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)
\end{displaymath}
\begin{displaymath}
\frac{\Sigma\vdash\wf{P_1} \quad \Sigma\vdash\wf{P_2}}
{\Sigma\vdash\wf{P_1\lor P_2}}(\mathsf{P}_5)
\qquad
\frac{\Sigma\vdash\wf{P}}
{\Sigma\vdash\wf{\lnot P}}(\mathsf{P}_6)
\end{displaymath}
\begin{displaymath}
\frac{\Sigma\vdash\wf{P_1} \quad \Sigma\vdash\wf{P_2}}
{\Sigma\vdash\wf{P_1\Rightarrow P_2}}(\mathsf{P}_7)
\end{displaymath}
\begin{displaymath}
\frac{\Sigma,x:\tau\vdash\wf{P}}
{\Sigma\vdash\wf{\forall x:\tau.\,P}}(\mathsf{P}_8)
\qquad
\frac{\Sigma,x:\tau\vdash\wf{P}}
{\Sigma\vdash\wf{\exists x:\tau.\,P}}(\mathsf{P}_8)
\end{displaymath}
Well-formed theories ($\vdash\wf{\Sigma}$):
\begin{displaymath}
\frac{}{\vdash\wf{\emptyset}}(\textsf{Th}_1)
\qquad
\frac{\texttt{type}~s\not\in\Sigma}
{\vdash\wf{\Sigma,\texttt{type}~(\alpha_1,\dots,\alpha_n)~s}}(\textsf{Th}_2)
\qquad
\frac{x\not\in\Sigma \quad \Sigma\vdash\wf{\tau}}
{\vdash\wf{\Sigma,x:\tau}}(\textsf{Th}_3)
\end{displaymath}
\begin{displaymath}
\frac{\texttt{logic}~f\not\in\Sigma \quad
\forall i,\, \Sigma\vdash\wf{\tau_i}}
{\vdash\wf{\Sigma,\mathtt{logic}~f:\forall\vec{\alpha}.\,\tau_1,\dots,\tau_n\rightarrow\tau_{n+1}}}(\textsf{Th}_4)
\end{displaymath}
\begin{displaymath}
\frac{\texttt{logic}~p\not\in\Sigma \quad
\forall i,\, \Sigma\vdash\wf{\tau_i}}
{\vdash\wf{\Sigma,\mathtt{logic}~p:\forall\vec{\alpha}.\,\tau_1,\dots,\tau_n\rightarrow\mathtt{prop}}}(\textsf{Th}_5)
\end{displaymath}
\begin{displaymath}
\frac{\Sigma\vdash\wf{P}}
{\vdash\wf{\Sigma,\texttt{axiom}~\forall\vec{\alpha}.\,P}}(\textsf{Th}_6) \qquad
\frac{\Sigma\vdash\wf{P}}
{\vdash\wf{\Sigma,\texttt{goal}~\forall\vec{\alpha}.\,P}}(\textsf{Th}_6)
\end{displaymath}
Well-formed definitions of functions and predicates:
\begin{displaymath}
\frac{\Sigma\vdash\wf{\tau_i} \quad
\Sigma,x_1:\tau_1,\dots,x_n:\tau_n\vdash t:\tau}
{\Sigma\vdash\wf{\mathtt{function}~f(x_1:\tau_1,\dots,x_n:\tau_n) : \tau = t}}(\textsf{Th}_7)
\end{displaymath}
\begin{displaymath}
\frac{\Sigma\vdash\wf{\tau_i} \quad
\Sigma,x_1:\tau_1,\dots,x_n:\tau_n\vdash\wf{P}}
{\Sigma\vdash\wf{\mathtt{predicate}~p(x_1:\tau_1,\dots,x_n:\tau_n) = P}}(\textsf{Th}_8)
\end{displaymath}
Then, as far as typing and validity in concerned, the function $f$
(resp. the predicate $p$) is added to $\Sigma$ as
$\mathtt{logic}~f:\tau_1,\dots,\tau_n\rightarrow\tau$
(resp. $\mathtt{logic}~p:\tau_1,\dots,\tau_n\rightarrow\mathtt{prop}$).
\subsubsection{Validity}
Validity is defined as a set of natural deduction rules
($\Sigma\models P$). For the sake of clarity,
we write $\Sigma,P$ for $\Sigma,\texttt{axiom}~P$ in the following.
A substitution $\sigma$ over from type variables to types in extended
to terms and predicates in the obvious way. We write $P[t/x]$ for the
substitution of all the occurrences of a free variable $x$ in $P$ by a
term $t$.
\begin{displaymath}
\frac{\texttt{axiom}~\forall\vec{\alpha}.\,P\in\Sigma \quad
\Subst{\sigma}{\Sigma}}