From a1a3cb005eaf51f358cf4c50332e12e36b864044 Mon Sep 17 00:00:00 2001 From: Michael Hanus Date: Thu, 1 Nov 2018 13:34:37 +0100 Subject: [PATCH] Manual updated --- docs/manual.tex | 65 ++++++++++++++++++++++++++++++++ examples/withVerification/README | 7 ++-- 2 files changed, 69 insertions(+), 3 deletions(-) diff --git a/docs/manual.tex b/docs/manual.tex index a5a6f3f..8921cac 100644 --- a/docs/manual.tex +++ b/docs/manual.tex @@ -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, diff --git a/examples/withVerification/README b/examples/withVerification/README index 2090e2b..2a190fc 100644 --- a/examples/withVerification/README +++ b/examples/withVerification/README @@ -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 -- GitLab