Commit 263c6b90 authored by Michael Hanus 's avatar Michael Hanus
Browse files

Manual of curry2verify extended

parent 9c11b925
module Double(double,coin,even) where
import Nat
import Test.Prop
double x = add x x
coin x = x ? S x
even Z = True
even (S Z) = False
even (S (S n)) = even n
evendoublecoin x = always (even (double (coin x)))
-- Agda program using the Iowa Agda library
open import bool
module PROOF-evendoublecoin
(Choice : Set)
(choose : Choice → 𝔹)
(lchoice : Choice → Choice)
(rchoice : Choice → Choice)
where
open import eq
open import nat
open import list
open import maybe
---------------------------------------------------------------------------
-- Translated Curry operations:
add : ℕ → ℕ → ℕ
add zero x = x
add (suc y) z = suc (add y z)
coin : Choice → ℕ → ℕ
coin c1 x = if choose c1 then x else suc x
double : ℕ → ℕ
double x = add x x
even : ℕ → 𝔹
even zero = tt
even (suc zero) = ff
even (suc (suc x)) = even x
---------------------------------------------------------------------------
add-suc : ∀ (x y : ℕ) → add x (suc y) ≡ suc (add x y)
add-suc zero y = refl
add-suc (suc x) y rewrite add-suc x y = refl
-- auxiliary property for x+x instead of double:
even-add-x-x : ∀ (x : ℕ) → even (add x x) ≡ tt
even-add-x-x zero = refl
even-add-x-x (suc x) rewrite add-suc x x | even-add-x-x x = refl
evendoublecoin : (c1 : Choice) → (x : ℕ) → (even (double (coin c1 x))) ≡ tt
evendoublecoin c1 x rewrite even-add-x-x (coin c1 x) = refl
---------------------------------------------------------------------------
-- Agda program using the Iowa Agda library
open import bool
module TO-PROVE-evendoublecoin
(Choice : Set)
(choose : Choice → 𝔹)
(lchoice : Choice → Choice)
(rchoice : Choice → Choice)
where
open import eq
open import nat
open import list
open import maybe
---------------------------------------------------------------------------
-- Translated Curry operations:
add : ℕ → ℕ → ℕ
add zero x = x
add (suc y) z = suc (add y z)
coin : Choice → ℕ → ℕ
coin c1 x = if choose c1 then x else suc x
double : ℕ → ℕ
double x = add x x
even : ℕ → 𝔹
even zero = tt
even (suc zero) = ff
even (suc (suc x)) = even x
---------------------------------------------------------------------------
evendoublecoin : (c1 : Choice) → (x : ℕ) → (even (double (coin c1 x))) ≡ tt
evendoublecoin c1 x = ?
---------------------------------------------------------------------------
......@@ -29,7 +29,7 @@ However, these limitations might be relaxed in future releases.
Hence, the current tool should be considered as a first prototypical
approach to support the verification of Curry programs.
\subsection{Options}
\subsection{Basic Usage}
To translate the properties of a Curry program stored
in the file \code{prog.curry} into Agda,
......@@ -47,9 +47,140 @@ the completed file should be renamed into
This has the effect that CurryCheck does not test this property again
but trusts the proof and use this knowledge to simplify other tests.
As a concrete example, consider the following Curry module \code{Double},
shown in Figure~\ref{fig:double-curry},
which uses the Peano representation of natural numbers
(module \code{Nat}) to define an operation to double the value
of a number, a non-deterministic operation \code{coin}
which returns its argument or its incremented argument,
and a predicate to test whether a number is even.
Furthermore, it contains a property specifying that
doubling the coin of a number is always even.
\begin{figure}[t]
\begin{curry}
module Double(double,coin,even) where
import Nat
import Test.Prop
double x = add x x
coin x = x ? S x
even Z = True
even (S Z) = False
even (S (S n)) = even n
evendoublecoin x = always (even (double (coin x)))
\end{curry}
\caption{Curry program \code{Double.curry}\label{fig:double-curry}}
\end{figure}
In order to prove the correctness of this property,
we translate it into an Agda program by executing
%
\begin{curry}
> curry2verify Double
$\ldots$
Agda module 'TO-PROVE-evendoublecoin.agda' written.
If you completed the proof, rename it to 'PROOF-evendoublecoin.agda'.
\end{curry}
%
The Curry program is translated with
the default scheme (see further options below) based on
the ``planned choice'' scheme, described in \cite{AntoyHanusLibby16}.
The result of this translation is shown in
Figure~\ref{fig:to-prove-evendoublecoin}.
\begin{figure}[t]
\begin{curry}
-- Agda program using the Iowa Agda library
open import bool
module TO-PROVE-evendoublecoin
(Choice : Set)
(choose : Choice $\to$ ${\mathbb B}$)
(lchoice : Choice $\to$ Choice)
(rchoice : Choice $\to$ Choice)
where
open import eq
open import nat
open import list
open import maybe
---------------------------------------------------------------------------
-- Translated Curry operations:
add : ${\mathbb N}$ $\to$ ${\mathbb N}$ $\to$ ${\mathbb N}$
add zero x = x
add (suc y) z = suc (add y z)
coin : Choice $\to$ ${\mathbb N}$ $\to$ ${\mathbb N}$
coin c1 x = if choose c1 then x else suc x
double : ${\mathbb N}$ $\to$ ${\mathbb N}$
double x = add x x
even : ${\mathbb N}$ $\to$ ${\mathbb B}$
even zero = tt
even (suc zero) = ff
even (suc (suc x)) = even x
---------------------------------------------------------------------------
evendoublecoin : (c1 : Choice) $\to$ (x : ${\mathbb N}$) $\to$ (even (double (coin c1 x))) $\equiv$ tt
evendoublecoin c1 x = ?
\end{curry}
\caption{Agda program \code{TO-PROVE-evendoublecoin.agda}\label{fig:to-prove-evendoublecoin}}
\end{figure}
The Agda program contains all operations involved in the property
and the property itself.
Non-deterministic operations, like \code{coin}, have an additional
additional argument of the abstract type \code{Choice}
that represents the plan to execute some non-deterministic branch
of the program. By proving the property for all possible branches
as correct, it universally holds.
In our example, the proof is quite easy. First, we prove
that the addition of a number to itself is always even
(lemma \code{even-add-x-x}, which uses an auxiliary lemma
\code{add-suc}). Then, the property is an immediate consequence
of this lemma:
%
\begin{curry}
add-suc : $\forall$ (x y : ${\mathbb N}$) $\to$ add x (suc y) $\equiv$ suc (add x y)
add-suc zero y = refl
add-suc (suc x) y rewrite add-suc x y = refl
even-add-x-x : $\forall$ (x : ${\mathbb N}$) $\to$ even (add x x) $\equiv$ tt
even-add-x-x zero = refl
even-add-x-x (suc x) rewrite add-suc x x | even-add-x-x x = refl
evendoublecoin : (c1 : Choice) $\to$ (x : ${\mathbb N}$) $\to$ (even (double (coin c1 x))) $\equiv$ tt
evendoublecoin c1 x rewrite even-add-x-x (coin c1 x) = refl
\end{curry}
%
As the proof is complete, we rename this Agda program
into \code{PROOF-evendoublecoin.agda} so that the proof
can be used by further invocations of CurryCheck.
\subsection{Options}
The command \code{curry2verify} can be parameterized
with various options which can also be shown using the option
\ccode{--help} and are described in the following.
with various options.
The available options can also be shown by executing
\begin{curry}
curry2verify --help
\end{curry}
The options are briefly described in the following.
\begin{description}
\item{\code{-h}, \code{-?}, \code{--help}}
......
module Double(double,coin,even) where
import Nat
import Test.Prop
......@@ -5,8 +7,8 @@ double x = add x x
coin x = x ? S x
even Z = True
even (S Z) = False
even Z = True
even (S Z) = False
even (S (S n)) = even n
evendoublecoin x = always (even (double (coin x)))
......
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