diff --git a/examples/DetOperations.curry b/examples/DetOps.curry similarity index 100% rename from examples/DetOperations.curry rename to examples/DetOps.curry diff --git a/examples/Proof-last-is-deterministic.agda b/examples/Proof-DetOps-last-is-deterministic.agda similarity index 97% rename from examples/Proof-last-is-deterministic.agda rename to examples/Proof-DetOps-last-is-deterministic.agda index e704334ca1e2c4189a3eeb8019b28623b8ab0ff9..d433c6f8db5d96b37b3f5b5eeb9bbd1ece1266d3 100644 --- a/examples/Proof-last-is-deterministic.agda +++ b/examples/Proof-DetOps-last-is-deterministic.agda @@ -1,4 +1,4 @@ -module Proof-last-is-deterministic where +module Proof-DetOps-last-is-deterministic where -- Show that last is a deterministic operation. -- The property to show is: diff --git a/examples/withVerification/PROOF-appendAddLengths.agda b/examples/withVerification/PROOF-ListProp-appendAddLengths.agda similarity index 95% rename from examples/withVerification/PROOF-appendAddLengths.agda rename to examples/withVerification/PROOF-ListProp-appendAddLengths.agda index 5294fa52d2ede43be95445194e5d3a6b5420f42b..69f36087ae14182a824ac5ea9e5bef36861cb08a 100644 --- a/examples/withVerification/PROOF-appendAddLengths.agda +++ b/examples/withVerification/PROOF-ListProp-appendAddLengths.agda @@ -2,7 +2,7 @@ open import bool -module PROOF-appendAddLengths +module PROOF-ListProp-appendAddLengths (Choice : Set) (choose : Choice → 𝔹) (lchoice : Choice → Choice) diff --git a/examples/withVerification/PROOF-sortPreservesLength.agda b/examples/withVerification/PROOF-SortSpec-sortPreservesLength.agda similarity index 96% rename from examples/withVerification/PROOF-sortPreservesLength.agda rename to examples/withVerification/PROOF-SortSpec-sortPreservesLength.agda index 1e75a12d9d1821a5bc73ae8844ad46d693e717f6..5204f93250f8c72cf5a014600315227d262dffae 100644 --- a/examples/withVerification/PROOF-sortPreservesLength.agda +++ b/examples/withVerification/PROOF-SortSpec-sortPreservesLength.agda @@ -2,7 +2,7 @@ open import bool -module PROOF-sortPreservesLength +module PROOF-SortSpec-sortPreservesLength (Choice : Set) (choose : Choice → 𝔹) (lchoice : Choice → Choice) diff --git a/examples/withVerification/README b/examples/withVerification/README index 4bec2ae66c3e0f8a159bfaf16b2bd2d1581160b4..2090e2bebcd7d83f69fc384808490350266650cb 100644 --- a/examples/withVerification/README +++ b/examples/withVerification/README @@ -4,8 +4,8 @@ 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 +If there are is a property `p` in a program `m` for which +a proof exists, i.e., a file named `proof-m-p` (the name is case independent), then: 1. Property `p` is not checked by CurryCheck @@ -31,7 +31,7 @@ To do so, we first formulate it as a property: To get some confidence in its general correctness, we test it: - > curry check ListProp + > curry-check ListProp ... Executing all tests... appendAddLengths_ON_BASETYPE (module ListProp, line 14): @@ -46,17 +46,17 @@ 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`. +`PROOF-ListProp-appendAddLengths.agda`. To see the effect of this proof for program testing, we run CurryCheck again: - > curry check ListProp + > curry-check ListProp Analyzing module 'ListProp'... > @@ -65,7 +65,7 @@ Hence, CurryCheck does not perform any test since the property simplify the postcondition to `True` so that it trivially holds. This simplification process can be visualized with option `-v`: - > curry check ListProp -v + > curry-check ListProp -v2 Analyzing module 'ListProp'... ... POSTCONDITION: append'post(a, b, c) → ==(+(length(a), length(b)), length(c)) diff --git a/examples/withVerification/SortSpec.curry b/examples/withVerification/SortSpec.curry index 73910f304f3d3cdf18530608c569e597f3daf4f0..130ddf5f584342917ce63b6a0d64fd1abfaa1b15 100644 --- a/examples/withVerification/SortSpec.curry +++ b/examples/withVerification/SortSpec.curry @@ -26,7 +26,8 @@ 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 +sort'spec xs | sorted ys = ys + where ys = perm xs -- An implementation of sort with quicksort: sort :: [Int] -> [Int] diff --git a/package.json b/package.json index 080a768c223f359d22f40c4496285c1a77de2eab..4de7993cea9041209438b647e54ceab63cb8e3eb 100644 --- a/package.json +++ b/package.json @@ -20,7 +20,7 @@ }, "testsuite": [ { "src-dir": "examples", - "modules": [ "DefaultRulesTest", "DetOperations", "ExampleTests", + "modules": [ "DefaultRulesTest", "DetOps", "ExampleTests", "ExamplesFromManual", "FloatTest", "ListSpecifications", "Nats", "SEBF", "Sum", "SortSpec", "Tree" ] }, diff --git a/src/CurryCheck.curry b/src/CurryCheck.curry index c0fb182bb8f9390ce64646f5d607fbb660354f8a..107e6a4e18db2c0935750456eb8ad52fdcda7d0b 100644 --- a/src/CurryCheck.curry +++ b/src/CurryCheck.curry @@ -30,8 +30,9 @@ import AbstractCurry.Types import AbstractCurry.Files import AbstractCurry.Select import AbstractCurry.Build -import AbstractCurry.Pretty (showCProg) -import AbstractCurry.Transform (renameCurryModule,updCProg,updQNamesInCProg) +import AbstractCurry.Pretty ( showCProg ) +import AbstractCurry.Transform ( renameCurryModule, updCProg + , updQNamesInCProg, updQNamesInCFuncDecl ) import qualified FlatCurry.Types as FC import FlatCurry.Files import qualified FlatCurry.Goodies as FCG @@ -51,7 +52,7 @@ ccBanner :: String ccBanner = unlines [bannerLine,bannerText,bannerLine] where bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++ - packageVersion ++ " of 08/10/2018)" + packageVersion ++ " of 30/10/2018)" bannerLine = take (length bannerText) (repeat '-') -- Help text @@ -387,14 +388,14 @@ classifyTests opts prog = map makeProperty -- Extracts all tests from a given Curry module and transforms -- all polymorphic tests into tests on a base type. +-- The third argument contains the list of function representing +-- proved properties. It is used to simplify post conditions to be tested. -- The result contains a triple consisting of all actual tests, -- all ignored tests, and the public version of the original module. -transformTests :: Options -> String -> CurryProg +transformTests :: Options -> String -> [CFuncDecl] -> CurryProg -> IO ([CFuncDecl],[CFuncDecl],CurryProg) -transformTests opts srcdir +transformTests opts srcdir theofuncs prog@(CurryProg mname imps typeDecls functions opDecls) = do - theofuncs <- if optProof opts then getTheoremFunctions srcdir prog - else return [] simpfuncs <- simplifyPostConditionsWithTheorems (optVerb opts) theofuncs funcs let preCondOps = preCondOperations simpfuncs postCondOps = map ((\ (mn,fn) -> (mn, fromPostCondName fn)) . funcName) @@ -541,13 +542,13 @@ revertDetOpTrans detops fdecl@(CFunc qf@(mn,fn) ar vis texp _) = -- for f. genDetOpTests :: [String] -> [QName] -> [CFuncDecl] -> [CFuncDecl] genDetOpTests prooffiles prefuns fdecls = - map (genDetProp prefuns) (filter isDetOrgOp fdecls) + map (genDetProp prefuns) (filter (isDetOrgOp . funcName) fdecls) where - isDetOrgOp fdecl = - let fn = snd (funcName fdecl) - in "_ORGNDFUN" `isSuffixOf` fn && - not (existsProofFor (determinismTheoremFor (take (length fn - 9) fn)) - prooffiles) + isDetOrgOp (mn,fn) = + "_ORGNDFUN" `isSuffixOf` fn && + not (existsProofFor (mnorg, determinismTheoremFor (take (length fn - 9) fn)) + prooffiles) + where mnorg = take (length mn - 10) mn -- remove _PUBLICDET suffix -- Transforms a declaration of a deterministic operation f_ORGNDFUN -- into a determinisim property test of the form @@ -668,9 +669,16 @@ analyseCurryProg opts modname orgprog = do let words = map firstWord (lines progtxt) staticerrs = missingCPP ++ map (showOpError words) staticoperrs putStrIfDetails opts "Generating property tests...\n" + theofuncs <- if optProof opts then getTheoremFunctions srcdir prog + else return [] + -- compute already proved theorems for public module: + let pubmodname = modname++"_PUBLIC" + rnm2pub mn@(mod,n) | mod == modname = (pubmodname,n) + | otherwise = mn + theopubfuncs = map (updQNamesInCFuncDecl rnm2pub) theofuncs (rawTests,ignoredTests,pubmod) <- - transformTests opts srcdir . renameCurryModule (modname++"_PUBLIC") - . makeAllPublic $ prog + transformTests opts srcdir theopubfuncs + . renameCurryModule pubmodname . makeAllPublic $ prog let (rawDetTests,ignoredDetTests,pubdetmod) = transformDetTests opts prooffiles . renameCurryModule (modname++"_PUBLICDET") diff --git a/src/SimplifyPostConds.curry b/src/SimplifyPostConds.curry index 12c017f66ad5288d1ed86ce013ab876d7dfe96b4..edac492762f671aa0a99343308e0bb698c8b92a3 100644 --- a/src/SimplifyPostConds.curry +++ b/src/SimplifyPostConds.curry @@ -31,7 +31,6 @@ import Rewriting.Substitution import Rewriting.Rules import ContractUsage -import TheoremUsage -- Simplify the postconditions contained in the third argument w.r.t. a given -- list of theorems (second argument). diff --git a/src/TheoremUsage.curry b/src/TheoremUsage.curry index 1a938dd5d51d1e16d9c56bbf56a8da8818873be8..fee42ec622e0f2ac490523446fe150aa06570a0e 100644 --- a/src/TheoremUsage.curry +++ b/src/TheoremUsage.curry @@ -9,18 +9,19 @@ --- --- * A theorem is considered as proven and, thus, not be checked --- by CurryCheck or the contract wrapper (see `currypp`), if there exists ---- a file named with prefix "Proof" and the name of the theorem, e.g., ---- `Proof-sortPreservesLength.agda`. The name is not case sensitive, ---- the file name extension is arbitrary and the special characters in the ---- name are ignored. Hence, a proof for `sortlength` could be also stored in ---- a file named `PROOF_sort-perserves-length.smt`. +--- a file named with prefix "Proof" and the qualified name of the theorem, +--- e.g., `Proof-Sort-sortPreservesLength.agda`. +--- The name is not case sensitive, the file name extension is arbitrary +--- and the special characters in the name are ignored. +--- Hence, a proof for `sortlength` could be also stored in +--- a file named `PROOF_Sort_sort_preserves_length.smt`. --- --- * A proof that some operation `f` is deterministic has the name --- `fIsDeterministic` so that a proof for `last` can be stored in --- `proof-last-is-deterministic.agda` (and also in some other files). --- --- @author Michael Hanus ---- @version August 2016 +--- @version October 2018 ------------------------------------------------------------------------ module TheoremUsage @@ -56,20 +57,20 @@ getProofFiles dir = do return (filter isProofFileName files) --- Does the list of file names (second argument) contain a proof of the ---- theorem given as the first argument? -existsProofFor :: String -> [String] -> Bool -existsProofFor propname filenames = - any (isProofFileNameFor propname) filenames +--- qualified theorem name given as the first argument? +existsProofFor :: QName -> [String] -> Bool +existsProofFor qpropname filenames = + any (isProofFileNameFor qpropname) filenames --- Is this a file name with a proof, i.e., start it with `proof`? isProofFileName :: String -> Bool isProofFileName fn = "proof" `isPrefixOf` (map toLower fn) --- Is this the file name of a proof of property `prop`? -isProofFileNameFor :: String -> String -> Bool -isProofFileNameFor prop fname = +isProofFileNameFor :: QName -> String -> Bool +isProofFileNameFor (mn,prop) fname = let lfname = map toLower (dropExtension fname) - lprop = map toLower prop + lprop = map toLower (mn ++ prop) in if "proof" `isPrefixOf` lfname then deleteNonAlphanNum (drop 5 lfname) == deleteNonAlphanNum lprop else False @@ -86,7 +87,7 @@ getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl] getTheoremFunctions proofdir (CurryProg _ _ _ functions _) = do let propfuncs = filter isProperty functions -- all properties prooffiles <- getProofFiles proofdir - return $ filter (\fd -> existsProofFor (snd (funcName fd)) prooffiles) + return $ filter (\fd -> existsProofFor (funcName fd) prooffiles) propfuncs ------------------------------------------------------------------------