Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
currypackages
currycheck
Commits
264273cf
Commit
264273cf
authored
May 08, 2019
by
Michael Hanus
Browse files
Update examples for equivalent operations
parent
b329749b
Changes
13
Hide whitespace changes
Inline
Sidebyside
docs/manual.tex
View file @
264273cf
...
...
@@ 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 nonalphanumberic characters
...
...
examples/equivalent_operations/BacciEtAl12.curry
0 → 100644
View file @
264273cf
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. 2534

 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 Nondeterministic Operations
 Proc. 14th Int. Symp. on Functional and Logic Programming (FLOPS 2018),
 Springer LNCS 10818, pp. 149165, 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 counterexample 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
examples/equivalent_operations/Intersperse.curry
View file @
264273cf
...
...
@@ 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
examples/equivalent_operations/Ints12.curry
View file @
264273cf
 Testing the equivalence of nonterminating operations:
import Data.Nat
import Test.Prop
 Two different infinite lists:
...
...
examples/equivalent_operations/NDInsert.curry
View file @
264273cf
...
...
@@ 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
examples/equivalent_operations/Perm.curry
0 → 100644
View file @
264273cf
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
examples/equivalent_operations/README.md
View file @
264273cf
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 counterexamples, 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 (nondeterministic 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])
...
...
examples/equivalent_operations/RevRev.curry
View file @
264273cf
...
...
@@ 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
examples/equivalent_operations/SimpleExample.curry
deleted
100644 → 0
View file @
b329749b
import Test.Prop
 This is an example which shows the "nonreferentiality" 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'
examples/equivalent_operations/SortPermute.curry
0 → 100644
View file @
264273cf
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])
examples/equivalent_operations/Take.curry
View file @
264273cf
 Example to show the nonequivalence 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 report
ed by the 11th test:

Equivalence is falsifi
ed by the 11th test:
take_equiv = take1 <=> take2
 With termination information, equivalence is falsified by the 2nd test:
take_equiv'TERMINATE = take1 <=> take2
examples/equivalent_operations/Unzip.curry
View file @
264273cf
...
...
@@ 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 equivalen
t:

Equivalence falsified by 27th tes
t:
unzipEquiv = unzip1 <=> unzip2
 Equivalence falsified by 6th test:
unzipEquiv'TERMINATE = unzip1 <=> unzip2
 Ground equivalence is not falsified:
unzipEquiv'GROUND xs = unzip1 xs <~> unzip2 xs
package.json
View file @
264273cf
...
...
@@ 15,15 +15,14 @@
"easycheck"
:
">= 0.0.1"
,
"flatcurry"
:
">= 2.0.0"
,
"frontendexec"
:
">= 0.0.1"
,
"peano"
:
">= 1.0.0"
,
"profiling"
:
">= 1.0.0"
,
"rewriting"
:
">= 2.0.0"
,
"setfunctions"
:
">= 0.0.1"
,
"wlpprint"
:
">= 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"
:
{
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment