From 264273cf423483a98b476b2c77872df7be7fea2c Mon Sep 17 00:00:00 2001 From: Michael Hanus Date: Wed, 8 May 2019 12:45:31 +0200 Subject: [PATCH] Update examples for equivalent operations --- docs/manual.tex | 6 +-- .../equivalent_operations/BacciEtAl12.curry | 46 +++++++++++++++++++ .../equivalent_operations/Intersperse.curry | 8 +++- examples/equivalent_operations/Ints12.curry | 1 - examples/equivalent_operations/NDInsert.curry | 3 ++ examples/equivalent_operations/Perm.curry | 30 ++++++++++++ examples/equivalent_operations/README.md | 7 ++- examples/equivalent_operations/RevRev.curry | 8 ++++ .../equivalent_operations/SimpleExample.curry | 27 ----------- .../equivalent_operations/SortPermute.curry | 42 +++++++++++++++++ examples/equivalent_operations/Take.curry | 7 ++- examples/equivalent_operations/Unzip.curry | 10 +++- package.json | 5 +- 13 files changed, 160 insertions(+), 40 deletions(-) create mode 100644 examples/equivalent_operations/BacciEtAl12.curry create mode 100644 examples/equivalent_operations/Perm.curry delete mode 100644 examples/equivalent_operations/SimpleExample.curry create mode 100644 examples/equivalent_operations/SortPermute.curry diff --git a/docs/manual.tex b/docs/manual.tex index 395f29c..73258e9 100644 --- a/docs/manual.tex +++ b/docs/manual.tex @@ -745,13 +745,13 @@ 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.*}, +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.*}, +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.*}, +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 diff --git a/examples/equivalent_operations/BacciEtAl12.curry b/examples/equivalent_operations/BacciEtAl12.curry new file mode 100644 index 0000000..f3139a2 --- /dev/null +++ b/examples/equivalent_operations/BacciEtAl12.curry @@ -0,0 +1,46 @@ +import Test.Prop + +-- This is an example from +-- +-- G. Bacci, M. Comini, M.A. Feliu, A. Villanueva: +-- Automatic Synthesis of Specifications for First Order Curry +-- Proc. Principles and Practice of Declarative Programming (PPDP'12), +-- ACM Press, pp. 25-34 +-- +-- It shows that two operations, which compute the same values, +-- might compute different results in larger contexts. +-- This example is also used in the introduction of the paper +-- explaining the equivalence checking features implemented in CurryCheck: +-- +-- Antoy, S., Hanus, M.: +-- Equivalence Checking of Non-deterministic Operations +-- Proc. 14th Int. Symp. on Functional and Logic Programming (FLOPS 2018), +-- Springer LNCS 10818, pp. 149-165, 2018 + +data AB = A | B + deriving (Eq,Show) + +data C = C AB + deriving (Eq,Show) + +h :: AB -> AB +h A = A + +f :: AB -> C +f x = C (h x) + +g :: AB -> C +g A = C A + + +-- The computed result equivalence of f and g on ground values +-- always holds, i.e., f and g always compute same values. +-- Since the domain is finite, this property is actually proved by CurryCheck. +f_and_g :: AB -> Prop +f_and_g x = f x <~> g x + +-- The contextual equivalence of f and g does not hold. +-- The counter-example is found by CurryCheck with the 2nd test +-- (or with the 1st test when option "--equivalence=autoselect" is used). +f_equiv_g :: Prop +f_equiv_g = f <=> g diff --git a/examples/equivalent_operations/Intersperse.curry b/examples/equivalent_operations/Intersperse.curry index 1d93da8..8b458d1 100644 --- a/examples/equivalent_operations/Intersperse.curry +++ b/examples/equivalent_operations/Intersperse.curry @@ -22,5 +22,11 @@ intersperse2 sep (x:xs) = x : go xs go (y:ys) = sep : y : go ys --- These operations are not equivalent: +-- These operations are not equivalent (falsified by 43th test): intersperseEquiv = intersperse1 <=> intersperse2 + +-- These operations are not equivalent (falsified by 4th test): +intersperseEquiv'TERMINATE = intersperse1 <=> intersperse2 + +-- Ground equivalence testing is successful: +intersperseEquiv'GROUND x xs = intersperse1 x xs <~> intersperse2 x xs diff --git a/examples/equivalent_operations/Ints12.curry b/examples/equivalent_operations/Ints12.curry index 4ea999b..c47a4e4 100644 --- a/examples/equivalent_operations/Ints12.curry +++ b/examples/equivalent_operations/Ints12.curry @@ -1,6 +1,5 @@ -- Testing the equivalence of non-terminating operations: -import Data.Nat import Test.Prop -- Two different infinite lists: diff --git a/examples/equivalent_operations/NDInsert.curry b/examples/equivalent_operations/NDInsert.curry index 2c2ac43..4fcc493 100644 --- a/examples/equivalent_operations/NDInsert.curry +++ b/examples/equivalent_operations/NDInsert.curry @@ -23,3 +23,6 @@ ndinsert_groundequiv x xs = ndinsert1 x xs <~> ndinsert2 x xs -- In PAKCS, the counter example is reported by the 7th test: ndinsert_equiv = ndinsert1 <=> ndinsert2 +-- With termination info, the counter example is reported by the 1st test: +ndinsert_equiv'TERMINATE = ndinsert1 <=> ndinsert2 + diff --git a/examples/equivalent_operations/Perm.curry b/examples/equivalent_operations/Perm.curry new file mode 100644 index 0000000..4118d21 --- /dev/null +++ b/examples/equivalent_operations/Perm.curry @@ -0,0 +1,30 @@ +import Test.Prop + +-- Definition of permute from library Combinatorial +-- Note that this definition is "spine strict", i.e., it does not return +-- any partial value for partial lists, e.g., +-- head (permute (1:failed)) ---> no value! +permute :: [a] -> [a] +permute [] = [] +permute (x:xs) = ndinsert (permute xs) + where ndinsert [] = [x] + ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys) + +-- An alternative, less strict definition of permutations, e.g., +-- head (perm (1:failed)) ---> 1 +perm :: [a] -> [a] +perm [] = [] +perm (x:xs) = ndinsert x (perm xs) + where ndinsert x ys = x : ys + ndinsert x (y:ys) = y : ndinsert x ys + +------------------------------------------------------------------ + +-- Equivalence falsified by 13th test: +permEquiv = perm <=> permute + +-- Equivalence falsified by 3rd test: +permEquiv'TERMINATE = perm <=> permute + +-- Ground equivalence not falsified: +permEquiv'GROUND xs = perm xs <~> permute xs diff --git a/examples/equivalent_operations/README.md b/examples/equivalent_operations/README.md index cc8957d..84f7d91 100644 --- a/examples/equivalent_operations/README.md +++ b/examples/equivalent_operations/README.md @@ -1,15 +1,20 @@ +Equivalence checking with CurryCheck +==================================== + This directory contains some examples for the use of CurryCheck to check the equivalence of operations. Since most of these are examples to test whether CurryCheck is able to report counter-examples, their test fails intentionally. These are the programs +- BacciEtAl12 (simple example from Bacci et al PPDP'12) - Intersperse (inserting separators in a list [Christiansen/Seidel'11]) - Ints12 (generators for infinite lists) - NDInsert (non-deterministic list insertion) +- Perm (permutation from library Combinatorial vs. less strict version) - RevRev (double reverse) -- SimpleExample - SortEquiv (two variants of permutation sort) +- SortPermute (two variants of permutation sort with a stricter permutation) - Take (two variants of take [Foner/Zhang/Lampropoulos'18]) - Unzip (two variants of unzip [Chitil'11]) diff --git a/examples/equivalent_operations/RevRev.curry b/examples/equivalent_operations/RevRev.curry index ff84210..006add7 100644 --- a/examples/equivalent_operations/RevRev.curry +++ b/examples/equivalent_operations/RevRev.curry @@ -6,4 +6,12 @@ revrev xs = reverse (reverse xs) -- Test: is double reverse equivalent to the identity? -- This is not the case if both are applied to the context -- head (... (1:failed)) + +-- Equivalence falsified by 13th test: +revrevid = revrev <=> id + +-- Equivalence falsified by 3rd test: revrevid'TERMINATE = revrev <=> id + +-- Ground equivalence not falsified: +revrevid'GROUND xs = revrev xs <~> id xs diff --git a/examples/equivalent_operations/SimpleExample.curry b/examples/equivalent_operations/SimpleExample.curry deleted file mode 100644 index fdc22db..0000000 --- a/examples/equivalent_operations/SimpleExample.curry +++ /dev/null @@ -1,27 +0,0 @@ -import Test.Prop - --- This is an example which shows the "non-referentiality" of Curry (according --- to [Bacci et al. PPDP'12]), i.e., it shows that two operations, which --- compute the same values, might compute different results in larger --- contexts: - -data AB = A | B - deriving (Eq,Show) - -data C = C AB - deriving (Eq,Show) - -h A = A - -g x = C (h x) - -g' A = C A - - --- The computed result equivalence of g and g' on ground values --- always holds, i.e., g and g' always compute same values: -g_and_g' :: AB -> Prop -g_and_g' x = g x <~> g' x - --- The contextual equivalence of g and g' does not hold: -g_equiv_g' = g <=> g' diff --git a/examples/equivalent_operations/SortPermute.curry b/examples/equivalent_operations/SortPermute.curry new file mode 100644 index 0000000..ed4bbbc --- /dev/null +++ b/examples/equivalent_operations/SortPermute.curry @@ -0,0 +1,42 @@ +import Test.Prop + +-- Definition of permute from library `Combinatorial` (part of PAKCS +-- distribution up to version 2.0.2 and contained in Curry package +-- `combinatorial` version 1.0.0). +-- +-- Note that this definition is "spine strict", i.e., it does not return +-- any partial value for partial lists, e.g., +-- head (permute (1:failed)) ---> no value! +permute :: [a] -> [a] +permute [] = [] +permute (x:xs) = ndinsert (permute xs) + where ndinsert [] = [x] + ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys) + +------------------------------------------------------------------ + +sorted :: Ord a => [a] -> Bool +sorted [] = True +sorted [_] = True +sorted (x:y:zs) = x<=y && sorted (y:zs) + +psort :: Ord a => [a] -> [a] +psort xs | sorted ys = ys where ys = permute xs + +------------------------------------------------------------------ + +idSorted :: Ord a => [a] -> [a] +idSorted [] = [] +idSorted [x] = [x] +idSorted (x:y:zs) | x<=y = x : idSorted (y:zs) + +isort :: Ord a => [a] -> [a] +isort xs = idSorted (permute xs) + +------------------------------------------------------------------ + +-- Equivalence falsified by 1174th test: +equiv = psort <=> (isort :: [Int] -> [Int]) + +-- Equivalence falsified by 46th test: +equiv'TERMINATE = psort <=> (isort :: [Int] -> [Int]) diff --git a/examples/equivalent_operations/Take.curry b/examples/equivalent_operations/Take.curry index b13abfb..0aede3d 100644 --- a/examples/equivalent_operations/Take.curry +++ b/examples/equivalent_operations/Take.curry @@ -1,7 +1,7 @@ --- Example to show the non-equivalence of two versions of the --- `take` operation, taken from --- ---- Foner, K. and Zhang, H. and Lampropoulos, L.: {Keep Your Laziness in Check +--- Foner, K. and Zhang, H. and Lampropoulos, L.: Keep Your Laziness in Check --- ICFP 2018, --- DOI: 10.1145/3236797 @@ -27,5 +27,8 @@ take_groundequiv x xs = take1 x xs <~> take2 x xs -- by evaluating `take... failed [])` or `take... 0 failed`. -- Thus, we check the equivalence with CurryCheck: --- In PAKCS, the counter example is reported by the 11th test: +-- Equivalence is falsified by the 11th test: take_equiv = take1 <=> take2 + +-- With termination information, equivalence is falsified by the 2nd test: +take_equiv'TERMINATE = take1 <=> take2 diff --git a/examples/equivalent_operations/Unzip.curry b/examples/equivalent_operations/Unzip.curry index 032d2a5..b4a0374 100644 --- a/examples/equivalent_operations/Unzip.curry +++ b/examples/equivalent_operations/Unzip.curry @@ -14,7 +14,13 @@ unzip1 ((x,y):ps) = (x:xs,y:ys) where (xs,ys) = unzip1 ps --- Definition from Chitil'11: unzip2 :: [(a,b)] -> ([a],[b]) -unzip2 xs = foldr (\(a,b) (as,bs) -> (a:as,b:bs)) ([],[]) xs +unzip2 xs = foldr (\ (a,b) (as,bs) -> (a:as,b:bs)) ([],[]) xs --- These operations are not equivalent: +-- Equivalence falsified by 27th test: unzipEquiv = unzip1 <=> unzip2 + +-- Equivalence falsified by 6th test: +unzipEquiv'TERMINATE = unzip1 <=> unzip2 + +-- Ground equivalence is not falsified: +unzipEquiv'GROUND xs = unzip1 xs <~> unzip2 xs diff --git a/package.json b/package.json index 37ae2b2..50324a5 100644 --- a/package.json +++ b/package.json @@ -15,15 +15,14 @@ "easycheck" : ">= 0.0.1", "flatcurry" : ">= 2.0.0", "frontend-exec" : ">= 0.0.1", - "peano" : ">= 1.0.0", "profiling" : ">= 1.0.0", "rewriting" : ">= 2.0.0", "setfunctions" : ">= 0.0.1", "wl-pprint" : ">= 0.0.1" }, "compilerCompatibility": { - "pakcs": ">= 2.0.0", - "kics2": ">= 2.0.0" + "pakcs": ">= 2.0.0, < 3.0.0", + "kics2": ">= 2.0.0, < 3.0.0" }, "configModule": "CC.Config", "executable": { -- GitLab