Verified Commit feea6afc authored by Camil Staps's avatar Camil Staps 🚀

Update documentation; CI for documentation

parent 84dc5f6e
Pipeline #13824 failed with stage
in 3 minutes and 2 seconds
......@@ -6,3 +6,16 @@ build:
- apt-get install -y -qq build-essential subversion
script:
- make
doc:
image: "camilstaps/texlive"
before_script:
- apt-get update -qq
- apt-get install -y -qq git
script:
- cd doc
- pdflatex -shell-escape doc.tex
- pdflatex -shell-escape doc.tex
artifacts:
paths:
- doc/doc.pdf
......@@ -4,78 +4,7 @@ This tool can generate test programs using [Gast][]'s `exposeProperties` (see
above) from dcl modules. The tool was conceived in
[clean-platform#17](https://gitlab.science.ru.nl/clean-and-itasks/clean-platform/issues/19).
The properties to test are described in [CleanDoc][] blocks: comments above
function types. This works as follows:
- On the module documentation block, add a `@property-bootstrap` field. This
field should contain the 'header' of the generated test program: required
imports and helper definitions. The programmer must not add a module header
(`definition module ...`) and does not need to import Gast modules or the
module under test itself.
- On each function to test, add one or more `@property` fields to the docblock.
This property for now always starts with `A.`, followed by a number of
parameters and their types. The first line ends with a colon `:`. The
implementation of the property follows on the next line(s). For example:
```clean
/**
* @property member_correct: A.x :: a; xs :: [a]:
* member x (fromList xs) <==> isMember x xs
*/
member :: !a !(Set a) -> Bool | < a
```
Note that one can use Gast's `<==>` here without import, nor does one need to
import the module itself for `member` (and `fromList`). However, `isMember`
requires `import StdList` in the `@property-bootstrap` of the module.
It is possible to use multiple lines for the implementation of the property.
`testproperties` will guess the right indentation level.
- When parameters in `@property` fields contain type variables, the programmer
is required to suggest types to instantiate these variables with when
testing &mdash; otherwise, how would Gast be able to generate test cases?
This can be done with `@property-test-with`, either locally on the function
docblock or globally on the module docblock. For example:
```clean
/**
* @property-test-with a = Int
* @property-test-with a = Real
*/
```
For all relevant tests using the type variable `a`, two versions will be
generated: one with `Int` and one with `Real`. When multiple type variables
are used, all combinations are tested.
- Sometimes, Gast's generic test generation method is not very useful. This is
for instance the case with types for which automatically generated values are
not 'valid'.
Take `Set a` as an example. It is possible to write tests on `[a]` instead,
then in every test use `fromList :: [a] -> Set a` to get the set. However,
this is not very modular, and also clutters up the properties.
What you can do instead is writing tests as you would normally do,
quantifying over `Set a` in the property signature, and then add a
`@property-test-generator` to the module. This field tells the test generator
how to generate values of a certain type. An example is:
```clean
/**
* @property-test-generator [a] -> Set a | < a
* gen xs = fromList xs
*/
```
Currently, only generators with arity 1 are supported (but this can be worked
around using a tuple or an auxiliary data type in the `@property-bootstrap`).
When the generator has class constraints, you are expected to resolve them
yourself by providing the required instances, depending on the type variable
instantiations.
The latest documentation can be [downloaded][doc] in PDF format.
[doc]: https://gitlab.science.ru.nl/clean-and-itasks/clean-test-properties/-/jobs/artifacts/master/download?job=doc
[Gast]: https://gitlab.science.ru.nl/clean-and-itasks/gast
[CleanDoc]: https://github.com/clean-cloogle/Cloogle#clean-documentation
......@@ -4,16 +4,26 @@
\usepackage[hidelinks]{hyperref}
\usepackage[british]{babel}
\usepackage{latexgit}
\usepackage{fancyvrb}
\usepackage{cleveref}
\usepackage{csquotes}
\usepackage{relsize}
\usepackage{nameref}
\usepackage{enumitem}
\setlist{itemsep=0pt}
\title{clean-test-properties: documentation}
\usepackage{fancyvrb}
\fvset{gobble=1,fontsize=\small,xleftmargin=1cm}
\title{Clean-Test-Properties Documentation}
\author{Camil Staps}
\date{\gitcommitdate[formatDate]}
\newcommand{\bash}[1]{\texttt{\smaller[0.2]#1}}
\newcommand{\clean}[1]{\texttt{\smaller[0.2]#1}}
\newcommand{\filename}[1]{\textsf{#1}}
\newcommand{\module}[1]{\textsf{#1}}
\begin{document}
\maketitle
......@@ -27,5 +37,7 @@ It collects Gast properties from definition modules and automatically generates
\input{installation}
\input{usage}
\input{specifying-properties}
\input{examples}
\end{document}
\section{Examples}
Examples using clean-test-properties can currently be found in experimental branches in Platform:
\begin{itemize}
\item \url{https://gitlab.science.ru.nl/clean-and-itasks/clean-platform/merge_requests/131};
\item \sloppy\url{https://gitlab.science.ru.nl/clean-and-itasks/clean-platform/compare/master...geometryProperties}.
\end{itemize}
......@@ -2,10 +2,10 @@
Clean-test-properties is not yet included in any distribution, so you have to build the tool yourself.
On Linux and Mac, you can clone the repository and run \verb$make$ to fetch dependencies and build the binary.
On Linux and Mac, you can clone the repository and run \bash{make} to fetch dependencies and build the binary:
\begin{Verbatim}[fontsize=\small]
git clone https://gitlab.science.ru.nl/clean-and-itasks/clean-test-properties
cd clean-test-properties
make
\begin{Verbatim}
git clone https://gitlab.science.ru.nl/clean-and-itasks/clean-test-properties
cd clean-test-properties
make
\end{Verbatim}
\section{Specifying properties}
\label{sec:specifying-properties}
The tests of a module are specified in its documentation blocks,
both globally (in the documentation of the module itself) and locally (in the documentation of functions, types, etc.).
The format is dictated by the parsing tools in Platform, specifically \module{Clean.Parse.Comments} and \module{Clean.Doc}.
\makeatletter
\newcommand{\availableon}[1]{%
\vspace{-6mm}%
\hfill\small{\textit{Available on:} #1.}%
\vspace{2mm}\par\noindent%
\@ifnextchar\par\@gobble\relax}
\makeatother
\subsection{Basic properties}
Minimal test suites use only \nameref{sec:property}, though \nameref{sec:property-bootstrap} is virtually always needed.
\subsubsection{\clean{@property}}
\label{sec:property}
\availableon{functions}
In properties, the full Clean syntax can be used to specify Gast properties.
Since Gast is automatically imported (see \cref{sec:property-bootstrap}), you can use its combinators.
The first line of a property indicates its name and arguments.
An example test for the correctness of \clean{member} in \module{Data.Set} is:
\begin{Verbatim}
* @property correctness: A.x :: Int; s :: Set Int:
* member x s <==> isMember x (toList s)
\end{Verbatim}
This can be read as:
\enquote{there is a property \enquote{correctness}, which says that
for all \clean{x} of type \clean{Int} and \clean{s} of type \clean{Set Int},
\clean{member x s} holds if and only if \clean{isMember x (toList s)} holds.}
Obviously, this property should hold for more types than \clean{Int}.
However, Gast needs to have a concrete type in order to be able to generate test values.
It is possible to specify properties more abstractly; see \nameref{sec:property-test-with}.
\subsubsection{\clean{@property-bootstrap}}
\label{sec:property-bootstrap}
\availableon{modules}
In this field, give all the \enquote{bootstrap} that the generated test module should contain.
This includes imports, file-global helper types and functions, necessary instances and derivations, etc.
Some imports are included automatically and do not need to be added here:
\begin{itemize}
\item \module{Gast};
\item \module{Gast.CommandLine};
\item \clean{instance toString \{\#Char\}} from \module{StdString};
\item \module{Control.GenBimap};
\item The tested module itself.
\end{itemize}
\subsection{Advanced properties}
\subsubsection{\clean{@invariant}}
\label{sec:invariant}
\availableon{types}
Invariants are properties of types that should always hold.
This is useful for types of which the values are often assumed to be more restrictive than the type system allows to specify.
For instance, it is assumed that a \clean{Map} or a \clean{Set} is ordered, and that a type for angles has values from $[0,2\pi)$ or $[0,360)$ degrees.
Invariants on types are specified with the exact same syntax as properties on functions.
In the generated test module, they become plain functions and can thus be used in \nameref{sec:property} and \nameref{sec:precondition} fields.
For instance, for the \clean{Set} type we may specify:
\begin{Verbatim}
* @invariant no_duplicates: A.s :: Set a | Eq, genShow{|*|}, gPrint{|*|} a:
* xs =.= removeDup xs where xs = toList s
\end{Verbatim}
Then we can use this invariant in the definition of the correctness property of \clean{insert}:
\begin{Verbatim}
* @property correctness: A.x :: a; xs :: Set a:
* let xs` = insert x xs in
* check member x xs` /\ // Membership
* check contains xs` (toList xs) /\ // Rest untouched
* no_duplicates xs` // Data structure integrity
\end{Verbatim}
\subsubsection{\clean{@precondition}}
\label{sec:precondition}
\availableon{functions}
This is a convenience field for functions that already have a(t least one) \nameref{sec:property} field.
Its content should be an arbitrary Clean expression with type \clean{Bool} or \clean{Property}.
The expression is then taken as a condition for \emph{all} properties of the function, using Gast's \clean{==>} operator.
For instance, this property for \module{Data.Set}'s \clean{findMin} function:
\begin{Verbatim}
* @property correctness: A.xs :: Set a:
* not (null xs) ==> minList (toList xs) == findMin xs
\end{Verbatim}
can also be specified as:
\begin{Verbatim}
* @property correctness: A.xs :: Set a:
* minList (toList xs) == findMin xs
* @precondition not (null xs)
\end{Verbatim}
\subsection{Abstracting test types}
This section describes ways to specify properties in more abstract ways.
This serves two main functions:
it makes properties more readable as documentation,
and it reduces code duplication in properties.
\subsubsection{\clean{@property-test-generator}}
\label{sec:property-test-generator}
\availableon{modules}
In some cases, Gast's value generation is not suitable for generating useful test cases.
In particular this is the case for types as \clean{Map} and \clean{Set} which assume that some properties hold for their values
(while these properties cannot be ensured by the type system).
When testing such types, it is custom to use a \enquote{shadow type} to generate values and transform the shadow type to the tested type.%
\footnote{Common shadow types are \clean{[(k,v)]} for \clean{Map k v} and \clean{[a]} for \clean{Set a}.}
Inconveniently, classic testing with Gast then requires one to specify properties on the shadow type instead of the actual type and call the value transformer from every test.
Clean-test-properties can automate this process by defining a file-global test generator containing the value transformer.
A typical test generator for \clean{Set} would look like:
\begin{Verbatim}
* @property-test-generator [a] -> Set a | < a
* gen xs = fromList xs
\end{Verbatim}
On the first line, the type of the test generator is specified, including both the shadow type (\clean{[a]}) and the actual type (\clean{Set a}).
The following lines specify the implementation, assuming the generator is called \clean{gen}.
When clean-test-properties encounters a property requiring arguments that can be generated by this generator,
it will automatically insert it into the property (and change the property's type accordingly).
When multiple test generators are applicable, one is picked arbitrarily.
For a generator to be recognised by clean-test-properties it must have the \emph{exact same} result type as the argument used in the property.
This means that a property with arguments of type \clean{Set b} will \emph{not} use the test generator specified above, because the type variables do not match.
\subsubsection{\clean{@property-test-with}}
\label{sec:property-test-with}
\availableon{modules; functions}
With this field it is possible to abstract from concrete types in property signatures and still allow Gast to generate test values.
We can specify the correctness property of \module{Data.Set}'s \clean{member} function (\cref{sec:property}) more abstractly using \clean{a} instead of \clean{Int}:
\begin{Verbatim}
* @property correctness: A.x :: a; s :: Set a:
* member x s <==> isMember x (toList s)
\end{Verbatim}
To tell Gast how to test this property, use:
\begin{Verbatim}
* @property-test-with a = Int
\end{Verbatim}
When \clean{@property-test-with} is given globally (on a module), it is used for all tests described by that module;
otherwise, it is used only locally.
It is possible to give multiple type instantiations for a type variable.
Furthermore, properties can use multiple type variables.
In such cases, all possible configurations will be tested.
(When used unwisely, this can lead to long running times.)
\section{Usage}
For a list of all command line arguments, run \verb$testproperties --help$.
For a list of all command line arguments, run \bash{testproperties --help}.
This documentation discusses the most common use cases.
General options are \verb$--verbose$ (\verb$-v$) for more verbose output,
\verb$--quiet$ (\verb$-q$) for less verbose output,
and \verb$--no-color$ for output without ANSI escape sequences for colors.
The verbosity options (\verb$-v$ and \verb$-q$) may be given multiple times.
General options are \bash{--verbose} (\bash{-v}) for more verbose output,
\bash{--quiet} (\bash{-q}) for less verbose output,
and \bash{--no-color} for output without ANSI escape sequences for colors.
The verbosity options (\bash{-v} and \bash{-q}) may be given multiple times.
The typical workflow followed by \verb$testproperties$ is:
The typical workflow followed by \bash{testproperties} is:
\begin{enumerate}
\item Find modules to test.
......@@ -19,9 +19,9 @@ The typical workflow followed by \verb$testproperties$ is:
\end{enumerate}
\subsection{Find modules to test}
By default, \verb$testproperties$ recursively searches all definition modules in the current directory for properties.
Use \verb$--directory$ (\verb$-d$) to specify a different directory.
Use \verb$--module$ (\verb$-m$) to only search a specific module.
By default, \bash{testproperties} recursively searches all definition modules in the current directory for properties.
Use \bash{--directory} (\bash{-d}) to specify a different directory.
Use \bash{--module} (\bash{-m}) to only search a specific module.
This option can be given multiple times.
\subsection{Find properties}
......@@ -30,30 +30,30 @@ There are no options relating to this step.
\subsection{Generate test modules}
For each module, a new module is generated with the same name and a prefix.
The prefix can be set with \verb$--prefix$ (\verb$-p$; default \verb$_Tests$).
For instance, by default the tests for \verb$Data.Set$ appear in \verb$_Tests.Data.Set$.
The prefix can be set with \bash{--prefix} (\bash{-p}; default \module{\textunderscore{}Tests}).
For instance, by default the tests for \module{Data.Set} appear in \module{\textunderscore{}Tests.Data.Set}.
By default, tests are generated in the current directory (e.g., \verb$./_Tests/Data/Set.icl$).
Use \verb$--output-directory$ (\verb$-D$) to set a different directory.
By default, tests are generated in the current directory (e.g., \filename{./\textunderscore{}Tests/Data/Set.icl}).
Use \bash{--output-directory} (\bash{-D}) to set a different directory.
The generated module uses \verb$exposeProperties$ from \verb$Gast.CommandLine$.
The generated module uses \clean{exposeProperties} from \module{Gast.CommandLine}.
This means the test module has a standard command line interface to set test and output options.
The default options can be set with \verb$--print-option$ (\verb$-P$) and \verb$--test-option$ (\verb$-T$).
For instance, use \verb$--test-option 'Tests 10000'$ to test 10,000 values by default.
For an overview of the options available, see Gast's \verb$PrintOption$ and \verb$Testoption$ types.
The default options can be set with \bash{--print-option} (\bash{-P}) and \bash{--test-option} (\bash{-T}).
For instance, use \bash{--test-option 'Tests 10000'} to test 10,000 values by default.
For an overview of the options available, see Gast's \clean{PrintOption} and \clean{Testoption} types.
\subsection{Compile test modules}
This step is optional and only included when \verb$--compile$ (\verb$-c$) is given.
This option is implied by \verb$--run$ (see below).
This step is optional and only included when \bash{--compile} (\bash{-c}) is given.
This option is implied by \bash{--run} (see below).
For compiling the test modules, \verb$clm$ is used, by default with the arguments \verb$-nt -nr$.
Add more arguments with \verb$--clm-arg$ (\verb$-C$).
Note that to give several arguments to \verb$clm$, this option must be repeated,
i.e. \verb$-C -h -C 100m$ and not \verb$ -C '-h 100m'$.
For convenience, \verb$testproperties$ accepts \verb$-I$ and \verb$-IL$ like \verb$clm$.
For compiling the test modules, \bash{clm} is used, by default with the arguments \bash{-nt -nr}.
Add more arguments with \bash{--clm-arg} (\bash{-C}).
Note that to give several arguments to \bash{clm}, this option must be repeated,
i.e. \bash{-C -h -C 100m} and not \bash{ -C '-h 100m'}.
For convenience, \bash{testproperties} accepts \bash{-I} and \bash{-IL} like \bash{clm}.
\subsection{Run test modules}
This step is optional and only included when \verb$--run$ (\verb$-r$) is given.
It implies \verb$--compile$ (see above).
This step is optional and only included when \bash{--run} (\bash{-r}) is given.
It implies \bash{--compile} (see above).
When the step is included, every generated module is executed.
If a test fails, the return code of \verb$testproperties$ is non-zero, but the program will continue to test other modules (if any).
If a test fails, the return code of \bash{testproperties} is non-zero, but the program will continue to test other modules (if any).
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