programs library documentation

parent 23332bb6
......@@ -158,7 +158,49 @@ is inspired by~\cite{ayad10ijcar}.
\chapter{Standard Library: Why3ML Modules}
\label{chap:mllibrary}
\section{Library \texttt{ref}}
\begin{description}
\item[Ref] references \emph{i.e.} mutable variables:
type \verb|ref 'a| and functions \verb|ref| for creation,
\verb|(!)| for access, and \verb|(:=)| for mutation
\item[Refint] references with additional functions \texttt{incr} and
\texttt{decr} over integer references
\end{description}
\section{Library \texttt{array}}
\begin{description}
\item[Array]
\item[ArraySorted]
\item[ArrayEq]
\item[ArrayPermut]
\end{description}
\section{Library \texttt{queue}}
\begin{description}
\item[Queue]
\end{description}
\section{Library \texttt{stack}}
\begin{description}
\item[Stack]
\end{description}
\section{Library \texttt{hashtbl}}
\begin{description}
\item[Hashtbl]
\end{description}
\section{Library \texttt{string}}
\begin{description}
\item[Char]
\item[String]
\end{description}
%%% Local Variables:
%%% mode: latex
......
......@@ -44,10 +44,10 @@ module String
logic ([]) (s: string) (i :int) : char = M.([]) s.chars i
logic get (s: string) (i :int) : char = M.([]) s.chars i
parameter make : len:int -> c:char ->
{ len >= 0 }
string
{ length result = len and
parameter make : len:int -> c:char ->
{ len >= 0 }
string
{ length result = len and
forall i:int. 0 <= i < len -> result[i] = c }
parameter get : s:string -> i:int ->
......@@ -62,24 +62,24 @@ module String
parameter length : s:string -> {} int reads s { result = length s }
parameter copy : s:string ->
{}
parameter copy : s:string ->
{}
string
{ length result = length s and
{ length result = length s and
forall i:int. 0 <= i < length result -> result[i] = s[i] }
parameter uppercase : s:string ->
{}
{}
string
{ length result = length s and
forall i:int. 0 <= i < length result ->
{ length result = length s and
forall i:int. 0 <= i < length result ->
result[i] = Char.uppercase s[i] }
parameter lowercase : s:string ->
{}
{}
string
{ length result = length s and
forall i:int. 0 <= i < length result ->
{ length result = length s and
forall i:int. 0 <= i < length result ->
result[i] = Char.lowercase s[i] }
(* TODO
......@@ -109,21 +109,21 @@ module Buffer
parameter contents : b:t -> { } string { S.length result = length b }
parameter add_char :
b:t -> c:char ->
{ }
unit writes b.length b.contents
parameter add_char :
b:t -> c:char ->
{ }
unit writes b.length b.contents
{ length b = old (length b) + 1 and
(forall i: int.
(forall i: int.
0 <= i < length b -> b.contents[i] = (old b.contents)[i]) and
b.contents[length b - 1] = c }
parameter add_string :
b:t -> s:string ->
{ }
unit reads s writes b.length b.contents
parameter add_string :
b:t -> s:string ->
{ }
unit reads s writes b.length b.contents
{ length b = old (length b) + S.length s and
(forall i: int.
(forall i: int.
0 <= i < old (length b) -> b.contents[i] = (old b.contents)[i]) and
(forall i: int.
0 <= i < S.length s -> b.contents[old (length b) + i] = S.get s i) }
......@@ -141,7 +141,7 @@ module Test
use module Char
use module String
use module Buffer
let test1 () =
let b = Buffer.create 1024 in
let c = Char.chr 65 in
......@@ -162,7 +162,7 @@ end
***)
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C .. modules/string"
End:
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