specifying-properties.tex 7.97 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
\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}
21
\availableon{functions; instances}
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
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}
89
\availableon{functions; instances}
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118

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}
Camil Staps's avatar
Camil Staps committed
119 120 121 122 123
For some types, Gast's generic value generation does not generate very useful test cases.
For these types one can specify different test generators in several ways.

\paragraph{Value transformers}
Some types, such as \clean{Map} and \clean{Set}, assume that some properties hold for their values
124 125 126 127 128
	(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.

Camil Staps's avatar
Camil Staps committed
129
One can automate this process by defining a file-global test generator containing the value transformer.
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
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.

Camil Staps's avatar
Camil Staps committed
146 147 148 149 150 151 152 153 154 155 156 157
\paragraph{Predefined lists}
A different type of test generator takes values from a list.
Internally, it uses Gast's \clean{ForEach} property combinator.
The test generator header should start with \texttt{list:} and then list the type for which values are generated.
The rest of the test generator contains the implementation of the list.
For example:

\begin{Verbatim}
	 * @property-test-generator list: Int
	 *   [0..10]
\end{Verbatim}

158 159
\subsubsection{\clean{@property-test-with}}
\label{sec:property-test-with}
160
\availableon{modules; functions; instances}
161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
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.)