language tutorial (work in progress)

doc/.gitignore

+apidoc.tex
+manual.out

doc/Makefile

-HEVEA=hevea -fix
-
-all: manual.pdf manual.html
-
-manual.pdf: manual.tex version.tex
-	pdflatex manual
-	pdflatex manual
-
-manual.html: manual.tex version.tex
-	$(HEVEA) manual.tex
-
-manual.bib: manual.aux
-	aux2bib manual.aux > manual.bib
-
-clean:
-	rm -f $(addprefix manual, .wdvi .raux .log .aux . bbl .blg\
-				  .ind .ilg .idx .html .toc)
-	rm -f *.haux *.pdf *.hind *.htoc *whizzy*
-
-
-
-.PHONY: all clean

doc/manual.tex

@@ -4,14 +4,16 @@
 %\usepackage{url}
 \usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
 
-\usepackage[toc,nonumberlist]{glossaries}
-\makeglossaries
+%\usepackage[toc,nonumberlist]{glossaries}
+%\makeglossaries
 
 % for ocamldoc generated pages
 \usepackage{ocamldoc}
 \let\tt\ttfamily
 \let\bf\bfseries
 
+\newcommand{\why}{\textsf{Why3}}
+\newcommand{\eg}{\emph{e.g.}}
 
 \begin{document}
 \sloppy
@@ -88,7 +90,7 @@ We gratefully thank all the people who contributed to this document:
 
 \part{Reference Manual}
 
-\input{glossary.tex}
+% \input{glossary.tex}
 
 \input{syntaxref.tex}
 

doc/syntax.tex

-\chapter{Syntax}
+\chapter{Why3 Language}
 \label{chap:syntax}
 
 This chapter describes the input syntax, and informally gives its semantics,
 illustrated by examples.
 
-\section{Terms and Formulas}
+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 a first-order
+polymorphic logic.
 
-\section{Declarations, Theories}
+The Figure~\ref{fig:tutorial1} contains an example of \why\ input
+text, containing three theories. 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.
+
+\begin{figure}
+  \centering
+\begin{verbatim}
+theory List
+
+  type list 'a = Nil | Cons 'a (list 'a)
+
+end
+
+theory Length
+
+  use import List
+  use import int.Int
+
+  logic 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 (l : 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{verbatim}
+\caption{Example of Why3 text.}
+\label{fig:tutorial1}
+\end{figure}
+
+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
+use 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. 
+
+% \section{Terms and Formulas} *)
+
+% \section{Declarations, Theories} *)
+
+% \section{Using and Cloning Theories} *)
 
-\section{Using and Cloning Theories}
 
 %%% Local Variables:
 %%% mode: latex

src/bench/.gitignore

+bench.annot
+whybench.annot

tests/test-jcf.why

 
-(* test file *)
 
-theory Test
+theory List
 
-  use import list.List
+  type list 'a = Nil | Cons 'a (list 'a)
 
-  logic p (list 'a)
+end
+
+theory Length
+  use import int.Int
+  use import List
+
+  logic 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 (l : 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
 
-  goal G : p (Nil : list 'a) -> not (p (Nil : list 'bcd)) -> false
+theory Order
+
+  type t
+  logic (<=) 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, logic O.(<=) = (<=)
+
+end
 
 (*
 Local Variables: