Commit a1a3cb00 authored by Michael Hanus 's avatar Michael Hanus

Manual updated

parent 2b441573
Pipeline #302 failed with stages
......@@ -639,6 +639,71 @@ psort_equiv_isort'TERMINATE = psort <=> isort
Now a counter example is found by the 11th test.
\subsection{Combining Testing and Verification}
Usually, CurryCheck tests all user-defined properties as well as
postconditions or specifications,
as described in Section~\ref{sec:currycheck:contracts}.
If a programmer uses some other tool to verify such properties,
it is not necessary to check such properties with test data.
In order to advice CurryCheck to do so,
it is sufficient to store the proofs in specific files.
Since the proof might be constructed by some tool
unknown to CurryCheck or even manually,
CurryCheck does not check the proof file but trusts the programmer
and uses a naming convention for files containing proofs.
If there is a property \code{p} in a module \code{M}
for which a proof in file \code{proof-M-p.*}
(the name is case independent), then
CurryCheck assumes that this file contains
a valid proof for this property.
For instance, the following property states that
sorting a list does not change its length:
%
\begin{curry}
sortlength xs = length (sort xs) <~> length xs
\end{curry}
%
If this property is contained in module \code{Sort} and
there is a file \code{proof-Sort-sortlength.txt}
containing a proof for this property,
CurryCheck considers this property as valid and does not check it.
Moreover, it uses this information to simplify other properties to be tested.
For instance, consider the property \code{sortSatisfiesPostCondition}
of Section~\ref{sec:currycheck:contracts}.
This can be simplified to
\code{always$\;$True} so that it does not need to be tested.
One can also provide proofs for generated properties,
e.g., determinism, postconditions, specifications,
so that they are not tested:
\begin{itemize}
\item
If there is a proof file \code{proof-$M$-$f$IsDeterministic.*},
a determinism annotation for operation $M.f$ is not tested.
\item
If there is a proof file \code{proof-$M$-$f$SatisfiesPostCondition.*},
a postcondition for operation $M.f$ is not tested.
\item
If there is a proof file \code{proof-$M$-$f$SatisfiesSpecification.*},
a specification for operation $M.f$ is not tested.
\end{itemize}
Note that the file suffix and all non-alpha-numberic characters
in the name of the proof file are ignored.
Furthermore, the name is case independent
This should provide enough flexibility when other verification tools
require specific naming conventions.
For instance, a proof for the property \code{Sort.sortlengh}
could be stored in the following files in order to be considered
by CurryCheck:
\begin{curry}
proof-Sort-sortlength.tex
PROOF_Sort_sortlength.agda
Proof-Sort_sortlength.smt
ProofSortSortlength.smt
\end{curry}
\subsection{Checking Usage of Specific Operations}
In addition to testing dynamic properties of programs,
......
......@@ -4,9 +4,10 @@ Combining Testing and Verification
This directory contains some examples demonstrating the
combination of testing and verification.
If there are is a property `p` in a program `m` for which
a proof exists, i.e., a file named `proof-m-p` (the name
is case independent), then:
If there is a property `p` in a module `M` for which
a proof exists, i.e., a file named `proof-M-p.abc` (the name
is case independent and the suffix and all non-alpha-numberic characters
in the file name are ignored), then:
1. Property `p` is not checked by CurryCheck
......
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