Commit c165b523 authored by Michael Hanus 's avatar Michael Hanus
Browse files

currypp updated

parent b729a342
......@@ -15,7 +15,6 @@ currypp/.cpm/packages/cass-0.0.1
currypp/.cpm/packages/cass-analysis-0.0.4
currypp/.cpm/packages/currycheck-1.0.1
currypp/.cpm/packages/rewriting-0.0.1
currypp/.cpm/packages/verify-0.0.2
currypp/.cpm/packages/abstract-curry-1.0.0
currypp/.cpm/packages/flatcurry-1.0.0
currypp/.cpm/packages/xml-0.0.1
......
# curry-verify - A Tool to Support the Verification of Curry Programs
This package contains the tool `curry-verify` that supports
the verification of Curry programs
with the help of other theorem provers or proof assistants.
Currently, only Agda is supported as
a target language for verification (but more target languages
may be supported in future releases).
## Installing the tool
The tool can be directly installed by the command
> cpm installbin verify
This installs the executable `curry-verify` in the bin directory of CPM.
## Using the tool
If the bin directory of CPM (default: `~/.cpm/bin`) is in your path,
execute the tool with the module containing properties to be verified, e.g.,
> curry-verify -t agda -s choice Double
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
---------------------------------------------------------------------------
This directory contains some documention for the curry-verify tool:
main.tex:
A short description of the tool.
manual.tex:
A short description to be included in the main manual of the Curry system.
-- 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 = ?
---------------------------------------------------------------------------
\documentclass[11pt,fleqn]{article}
\usepackage[T1]{fontenc}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{xspace}
\usepackage{graphicx}
\setlength{\textwidth}{16.5cm}
\setlength{\textheight}{23cm}
\renewcommand{\baselinestretch}{1.1}
\setlength{\topmargin}{-1cm}
\setlength{\oddsidemargin}{0cm}
\setlength{\evensidemargin}{0cm}
\setlength{\marginparwidth}{0.0cm}
\setlength{\marginparsep}{0.0cm}
\newlength{\figurewidth}
\setlength{\figurewidth}{\textwidth}
\addtolength{\figurewidth}{-0.4cm}
% font for program texts
\renewcommand{\tt}{\usefont{OT1}{cmtt}{m}{n}\selectfont}
\newcommand{\codefont}{\small\tt}
\usepackage{listings}
\lstset{aboveskip=1.5ex,
belowskip=1.5ex,
showstringspaces=false, % no special string space
mathescape=true,
flexiblecolumns=false,
xleftmargin=2ex,
basewidth=0.52em,
basicstyle=\small\ttfamily}
\lstset{literate={->}{{$\rightarrow{}\!\!\!$}}3
}
\lstnewenvironment{curry}{}{}
\lstnewenvironment{currynomath}{\lstset{mathescape=false}}{} % Curry w/o math
\newcommand{\listline}{\vrule width0pt depth1.75ex}
% program text in normal text
\newcommand{\code}[1]{\mbox{\codefont #1}}
% program text in normal text with apostrophs
\newcommand{\ccode}[1]{``\code{#1}''}
\newcommand{\pindex}[1]{\index{#1@{\tt #1}}} % program elements in index
\begin{document}
\sloppy
\input{manual}
\begin{thebibliography}{10}
\bibitem{AntoyHanusLibby17EPTCS}
S.~Antoy, M.~Hanus, and S.~Libby.
\newblock Proving non-deterministic computations in {Agda}.
\newblock In {\em Proc. of the 24th International Workshop on Functional and
(Constraint) Logic Programming (WFLP 2016)}, volume 234 of {\em Electronic
Proceedings in Theoretical Computer Science}, pages 180--195. Open Publishing
Association, 2017.
\bibitem{Norell09}
U.~Norell.
\newblock Dependently typed programming in {Agda}.
\newblock In {\em Proceedings of the 6th International Conference on Advanced
Functional Programming (AFP'08)}, pages 230--266. Springer, 2009.
\end{thebibliography}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
\section{CurryVerify: A Tool to Support the Verification of Curry Programs}
\label{sec-curry2verify}
CurryVerify\index{CurryVerify}\index{verifying programs}\index{program!verification}
is a tool that supports the verification of Curry programs
with the help of other theorem provers or proof assistants.
Basically, CurryVerify extends CurryCheck (see Section~\ref{sec-currycheck}),
which tests given properties of a program,
by the possibility to verify these properties.
For this purpose, CurryVerify translates properties
into the input language of other theorem provers or proof assistants.
This is done by collecting all operations directly or indirectly
involved in a given property and translating them together with
the given property.
Currently, only Agda \cite{Norell09} is supported as
a target language for verification (but more target languages
may be supported in future releases).
The basic schemes to translate Curry programs into Agda programs
are presented in \cite{AntoyHanusLibby17EPTCS}.
That paper also describes the limitations of this approach.
Since Curry is a quite rich programming language,
not all constructs of Curry are currently supported
in the translation process (e.g., no case expressions,
local definitions, list comprehensions, do notations, etc).
Only a kernel language, where the involved rules
correspond to a term rewriting system, are translated into Agda.
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{Installation}
The current implementation of CurryVerify is a package
managed by the Curry Package Manager CPM
(see also Section~\ref{sec-cpm}).
Thus, to install the newest version of CurryVerify, use the following commands:
%
\begin{curry}
> cpm update
> cpm install verify
\end{curry}
%
This downloads the newest package, compiles it, and places
the executable \code{curry-verify} into the directory \code{\$HOME/.cpm/bin}.
Hence it is recommended to add this directory to your path
in order to execute CurryVerify as described below.
\subsection{Basic Usage}
To translate the properties of a Curry program stored
in the file \code{prog.curry} into Agda,
one can invoke the command\pindex{curry-verify}\pindex{verify}
%
\begin{curry}
curry-verify prog
\end{curry}
%
This generates for each property $p$ in module \code{prog}
an Agda program \ccode{TO-PROVE-$p$.agda}.
If one completes the proof obligation in this file,
the completed file should be renamed into
\ccode{PROOF-$p$.agda}.
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}
> curry-verify 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{AntoyHanusLibby17EPTCS}.
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{curry-verify} can be parameterized
with various options.
The available options can also be shown by executing
\begin{curry}
curry-verify --help
\end{curry}
The options are briefly described in the following.
\begin{description}
\item{\code{-h}, \code{-?}, \code{--help}}
These options trigger the output of usage information.
\item{\code{-q}, \code{--quiet}}
Run quietly and produce no informative output.
However, the exit code will be non-zero if some translation error occurs.
\item{\code{-v[$n$]}, \code{--verbosity[=$n$]}}
Set the verbosity level to an optional value.
The verbosity level \code{0} is the same as option \code{-q}.
The default verbosity level \code{1} shows the translation progress.
The verbosity level \code{2} (which is the same as omitting the level)
shows also the generated (Agda) program.
The verbosity level \code{3} shows also more details about
the translation process.
\item{\code{-n}, \code{--nostore}}
Do not store the translated program in a file but show it only.
\item{\code{-p $p$}, \code{--property=$p$}}
As a default, all properties occurring in the source program are
translated. If this option is provided, only property $p$ is translated.
\item{\code{-t $t$}, \code{--target=$t$}}
Define the target language of the translation.
Currently, only $t = \code{Agda}$ is supported, which is also the
default.
\item{\code{-s $s$}, \code{--scheme=$s$}}
Define the translation scheme used to represent Curry programs
in the target language.
For the target \code{Agda}, the following schemes are supported:
\begin{description}
\item[\code{choice}]
Use the ``planned choice'' scheme, see \cite{AntoyHanusLibby17EPTCS}
(this is the default).
In this scheme, the choices made in a non-deterministic computation
are abstracted by passing a parameter for these choices.
\item[\code{nondet}]
Use the ``set of values'' scheme, see \cite{AntoyHanusLibby17EPTCS},
where non-deterministic values are represented in a tree structure.
\end{description}
\end{description}
% LocalWords: CurryCheck
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)))
-- Mutual recursive definition of even:
import Nat
import Test.Prop
double x = add x x
coin x = x ? S x
even :: Nat -> Bool
even Z = True
even (S n) = odd n
odd :: Nat -> Bool
odd Z = False
odd (S n) = even n
odddoublecoin x = odd (double (coin x)) <~> False
import Nat
import Test.Prop
data Move = L | R
len [] = Z
len (_:xs) = S (len xs)
main = solve (S (S Z)) (S (S Z))
solve Z Z = []
solve (S x) y = L : solve x y
solve x (S y) = R : solve x y
-- Originally, we want to prove:
-- gamelength x y = len (solve x y) -=- add x y
-- If we are interested in the spine, i.e., the list structure of
-- calls to solve, we see that solve is strict in both arguments, i.e.,
-- (len (solve _|_ y)) and (len (solve x _|_)) have no values.
-- Thus, we can expand rules with variable arguments to rules with
-- all constructors:
solve1 Z Z = []
solve1 (S x) Z = L : solve1 x Z
solve1 (S x) (S y) = L : solve1 x (S y)
solve1 Z (S y) = R : solve1 Z y
solve1 (S x) (S y) = R : solve1 (S x) y
-- Finally, we join the rules with identical left-hand sides:
solve2 Z Z = []
solve2 (S x) Z = L : solve2 x Z
solve2 Z (S y) = R : solve2 Z y
solve2 (S x) (S y) = L : solve2 x (S y) ? R : solve2 (S x) y
-- and prove:
gamelength x y = len (solve2 x y) -=- add x y
import Test.Prop
data List a = Empty | Cons a (List a)
append Empty ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
appendIsAssoc xs ys zs = append (append xs ys) zs -=- append xs (append ys zs)
-- Agda program using the Iowa Agda library
open import bool
module PROOF-appendIsAssoc
(Choice : Set)
(choose : Choice → 𝔹)
(lchoice : Choice → Choice)
(rchoice : Choice → Choice)
where
open import eq
open import bool
open import nat
open import list
open import maybe
---------------------------------------------------------------------------
-- Translated Curry operations:
data List (a : Set) : Set where
Empty : List a
Cons : a → List a → List a
append : {a : Set} → List a → List a → List a
append Empty x = x
append (Cons y z) u = Cons y (append z u)
---------------------------------------------------------------------------
appendIsAssoc : {a : Set} → (x : List a) → (y : List a) → (z : List a)
→ (append (append x y) z) ≡ (append x (append y z))
appendIsAssoc Empty y z = refl
appendIsAssoc (Cons x xs) y z rewrite appendIsAssoc xs y z = refl
---------------------------------------------------------------------------
-- 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