Commit 6ca41157 authored by Michael Hanus's avatar Michael Hanus
Browse files

Examples for combining testing and verification added

parent 01923685
--- This module contains some contracts for list operations.
import Test.Prop
-- The well-known list concatenation. We give it another name,
-- otherwise we cannot specify contracts for it.
append :: [a] -> [a] -> [a]
append xs ys = xs ++ ys
-- Postcondition: append add length of input lists.
append'post xs ys zs = length xs + length ys == length zs
-- We formulate the postcondition as a property:
appendAddLengths xs ys = length xs + length ys -=- length (append xs ys)
-- Agda program using the Iowa Agda library
open import bool
module PROOF-appendAddLengths
(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:
++ : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
++ [] x = x
++ (y :: z) u = y :: (++ z u)
append : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
append x y = ++ x y
---------------------------------------------------------------------------
appendAddLengths : {a : Set} → (x : 𝕃 a) → (y : 𝕃 a)
→ ((length x) + (length y)) ≡ (length (append x y))
appendAddLengths [] y = refl
appendAddLengths (x :: xs) y rewrite appendAddLengths xs y = refl
---------------------------------------------------------------------------
-- Agda program using the Iowa Agda library
open import bool
module PROOF-sortPreservesLength
(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:
insert : ℕ → 𝕃 ℕ → 𝕃 ℕ
insert x [] = x :: []
insert y (z :: u) = if y ≤ z then y :: (z :: u) else z :: (insert y u)
sort : 𝕃 ℕ → 𝕃 ℕ
sort [] = []
sort (x :: y) = insert x (sort y)
---------------------------------------------------------------------------
insertIncLength : (x : ℕ) → (xs : 𝕃 ℕ)
→ length (insert x xs) ≡ suc (length xs)
insertIncLength x [] = refl
insertIncLength x (y :: ys) with (x ≤ y)
... | tt = refl
... | ff rewrite insertIncLength x ys = refl
sortPreservesLength : (xs : 𝕃 ℕ) → length (sort xs) ≡ length xs
sortPreservesLength [] = refl
sortPreservesLength (x :: xs)
rewrite insertIncLength x (sort xs) | sortPreservesLength xs = refl
---------------------------------------------------------------------------
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 for which
a proof exists, i.e., a file named `proof-p` (the name
is case independent), then:
1. Property `p` is not checked by CurryCheck
2. The property is translated into a simplification rule
in order to simplify other postconditions before checking them.
-------------------------------------------------------------------------
Example for applying the available Curry tools
----------------------------------------------
Consider the program `ListProp.curry` which contains a postcondition
for the list concatenation. The postcondition ensures that the length
of the concatenated list is the sum of the lengths of the input lists:
append'post xs ys zs = length xs + length ys == length zs
We can statically simplify this postcondition by proving it.
To do so, we first formulate it as a property:
appendAddLengths xs ys = length xs + length ys -=- length (append xs ys)
To get some confidence in its general correctness, we test it:
> currycheck ListProp
...
Executing all tests...
appendAddLengths_ON_BASETYPE (module ListProp, line 14):
OK, passed 100 tests.
appendSatisfiesPostCondition_ON_BASETYPE (module ListProp, line 7):
OK, passed 100 tests.
Since everything looks fine, we try to prove it with Agda.
For this purpose, we translate the property and all involved
functions into an Agda program:
> curry2verify ListProp
...
Agda module 'TO-PROVE-appendAddLengths.agda' written.
If you completed the proof, rename it to 'PROOF-appendAddLengths.agda'.
Now, we complete the Agda program `TO-PROVE-appendAddLengths.agda`
by a straightforward induction on the first argument of `appendAddLengths`.
Since the proof is complete, we rename the Agda module into
`PROOF-appendAddLengths.agda`.
To see the effect of this proof for program testing, we run CurryCheck again:
> currycheck ListProp
Analyzing module 'ListProp'...
>
Hence, CurryCheck does not perform any test since the property
`appendAddLengths` has been proved and this theorem is used to
simplify the postcondition to `True` so that it trivially holds.
This simplification process can be visualized with option `-v`:
> currycheck ListProp -v
Analyzing module 'ListProp'...
...
POSTCONDITION: append'post(a, b, c) → ==(+(length(a), length(b)), length(c))
...
SIMPPOSTCOND: append'post(a, b, c) → True
>
-------------------------------------------------------------------------
-- A specification of sorting a list and an implementation based
-- on insertion sort.
-- CurryCheck generates and checks properties which states
-- that the implementation is satisfies the specification
-- and the post-condition.
--
-- To demonstrate the use of statically proven properties,
-- we include a theorem that is used to simplify the postcondition
-- of sort.
import Test.Prop
perm [] = []
perm (x:xs) = ndinsert x (perm xs)
where
ndinsert x ys = x : ys
ndinsert x (y:ys) = y : ndinsert x ys
sorted [] = True
sorted [_] = True
sorted (x:y:ys) | x<=y && sorted (y:ys) = True
-- Postcondition: input and output lists should have the same length
sort'post xs ys = length xs == length ys && sorted ys
-- Specification of sort:
-- A list is a sorted result of an input if it is a permutation and sorted.
sort'spec :: [Int] -> [Int]
sort'spec xs | ys == perm xs && sorted ys = ys where ys free
-- An implementation of sort with quicksort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = insert x (sort xs)
insert :: Int -> [Int] -> [Int]
insert x [] = [x]
insert x (y:ys) = if x<=y then x : y : ys
else y : insert x ys
-- A theorem about the length of sorting a list.
-- If this theorem is proved (i.e., if there is a file
-- `proof-sort-preserves-length.*`),
-- it is not checked but used to simplify the postcondition sort'post.
sortPreservesLength xs = length (sort xs) <~> length xs
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