Commit 58d20088 authored by Jean-Christophe's avatar Jean-Christophe

programs documentation (in progress)

parent cbf0cede
......@@ -171,28 +171,44 @@ is inspired by~\cite{ayad10ijcar}.
\section{Library \texttt{array}}
\begin{description}
\item[Array]
\item[ArraySorted]
\item[ArrayEq]
\item[ArrayPermut]
\item[Array]polymorphic arrays (type \texttt{array 'a}, infix
syntax $a[i]$ for access and $a[i] \leftarrow e$ for update,
functions \texttt{length}, \texttt{make}, \texttt{append},
\texttt{sub}, \texttt{copy}, \texttt{fill}, and \texttt{blit})
\item[ArraySorted] an array of integers is sorted
(\verb|array_sorted_sub| and \verb|array_sorted|)
\item[ArrayEq] two arrays are identical
(\verb|array_eq_sub| and \verb|array_eq|)
\item[ArrayPermut] two arrays are permutation of each other
(\verb|permut_sub| and \verb|permut|)
\end{description}
\section{Library \texttt{queue}}
\begin{description}
\item[Queue]
\item[Queue] polymorphic mutable queues (type \texttt{t 'a} and
functions \texttt{create}, \texttt{push}, \texttt{pop},
\texttt{top}, \texttt{clear}, \texttt{copy}, \texttt{is\_empty},
\texttt{length})
\end{description}
\section{Library \texttt{stack}}
\begin{description}
\item[Stack]
\item[Stack] polymorphic mutable stacks (type \texttt{t 'a} and
functions \texttt{create}, \texttt{push}, \texttt{pop},
\texttt{top}, \texttt{clear}, \texttt{copy}, \texttt{is\_empty},
\texttt{length})
\end{description}
\section{Library \texttt{hashtbl}}
\begin{description}
\item[Hashtbl]
\item[Hashtbl] hash tables with monomorphic keys (type \texttt{key})
and polymorphic values (type \texttt{t 'a} of hash tables, syntax
$h[k]$ for access, functions \texttt{create}, \texttt{clear},
\texttt{add}, \texttt{mem}, \texttt{find}, \texttt{find\_all},
\texttt{copy}, \texttt{remove}, and \texttt{replace})
\end{description}
\section{Library \texttt{string}}
......
......@@ -100,7 +100,7 @@ a new architecture for calling external provers, and a
well-designed API, allowing to use \why\ as a software library.
An important emphasis is put on modularity and genericity,
giving the end user a possibility to easily reuse \why\
formalisations or to add support for a new external
formalizations or to add support for a new external
prover if wanted.
\subsection*{Availability}
......
......@@ -2,12 +2,32 @@
\label{chap:whyml}
This chapter describes the \whyml\ programming language.
% simple message = all Why3 language + mutable record fields + model
A \whyml\ input text contains a list of theories (see
chapter~\ref{chap:syntax}) and/or modules.
Modules extend theories with \emph{programs}.
Programs can use all types, symbols, and constructs from the logic.
They also provide extra features:
\begin{itemize}
\item In a record type declaration, some fields can be declared
\texttt{mutable}.
\item There are programming constructs with no counterpart in the logic:
\begin{itemize}
\item mutable field assignment;
\item sequence;
\item loops;
\item exceptions;
\item local and anonymous functions;
\item annotations: pre- and postconditions, assertions, loop invariants.
\end{itemize}
\item A program function can be non-terminating or can be proved
to be terminating using a variant (a term together with a well-founded
order relation).
\end{itemize}
% TODO: model types
% files .mlw
% command line
% tutorial with an example (same fringe)
% tutorial with examples: same fringe, max/sum
%%% Local Variables:
%%% mode: latex
......
......@@ -4,20 +4,21 @@
module M
use import int.Int
use import module ref.Ref
use import module ref.Refint
use import module array.Array
let max_sum (a: array int) (n: int) =
{ n >= 0 and length a = n and forall i:int. 0 <= i < n -> a[i] >= 0 }
let sum = ref 0 in
let max = ref 0 in
for i = 0 to n-1 do
invariant { !sum <= i * !max and forall j:int. 0 <= j < i -> a[j] <= !max }
if !max < a[i] then max := a[i];
sum := !sum + a[i]
done;
(!sum, !max)
{ let (sum, max) = result in sum <= n * max }
{ n >= 0 and length a = n and forall i:int. 0 <= i < n -> a[i] >= 0 }
let sum = ref 0 in
let max = ref 0 in
for i = 0 to n-1 do
invariant
{ !sum <= i * !max and forall j:int. 0 <= j < i -> a[j] <= !max }
if !max < a[i] then max := a[i];
sum += a[i]
done;
(!sum, !max)
{ let (sum, max) = result in sum <= n * max }
end
......
......@@ -23,10 +23,12 @@ module Refint
use export module Ref
(* parameter incr : r:ref int -> {} unit writes r { !r = old !r + 1 } *)
let incr (r:ref int) = {} r := !r + 1 { !r = old !r + 1 }
let incr (r: ref int) = {} r := !r + 1 { !r = old !r + 1 }
(* parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 } *)
let decr (r:ref int) = {} r := !r - 1 { !r = old !r - 1 }
let decr (r: ref int) = {} r := !r - 1 { !r = old !r - 1 }
let (+=) (r: ref int) (v: int) = {} r := !r + v { !r = old !r + v }
end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment