From 404419708999ff88fd61e2909664e88911aae1fe Mon Sep 17 00:00:00 2001 From: Michael Hanus Date: Tue, 30 Oct 2018 23:22:54 +0100 Subject: [PATCH] Names of proof files changed so that module names are included --- docs/manual.tex | 2 +- .../{DetOperations.curry => DetOps.curry} | 0 ...> Proof-DetOps-last-is-deterministic.agda} | 2 +- ...a => PROOF-ListProp-appendAddLengths.agda} | 2 +- ...> PROOF-SortSpec-sortPreservesLength.agda} | 2 +- examples/withVerification/README | 14 ++--- package.json | 2 +- src/CurryCheck.curry | 56 ++++++++++++------- src/SimplifyPostConds.curry | 1 - src/TheoremUsage.curry | 29 +++++----- 10 files changed, 62 insertions(+), 48 deletions(-) rename examples/{DetOperations.curry => DetOps.curry} (100%) rename examples/{Proof-last-is-deterministic.agda => Proof-DetOps-last-is-deterministic.agda} (97%) rename examples/withVerification/{PROOF-appendAddLengths.agda => PROOF-ListProp-appendAddLengths.agda} (95%) rename examples/withVerification/{PROOF-sortPreservesLength.agda => PROOF-SortSpec-sortPreservesLength.agda} (96%) diff --git a/docs/manual.tex b/docs/manual.tex index 0a295e3..0f814dd 100644 --- a/docs/manual.tex +++ b/docs/manual.tex @@ -661,7 +661,7 @@ sort'post xs ys = length xs == length ys -- Specification: -- A correct result is a permutation of the input which is 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/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 e704334..d433c6f 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 5294fa5..69f3608 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 1e75a12..5204f93 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 4bec2ae..2090e2b 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/package.json b/package.json index 757eb18..bc39aa8 100644 --- a/package.json +++ b/package.json @@ -25,7 +25,7 @@ "testsuite": [ { "src-dir": "examples", "options": "-m70", - "modules": [ "DefaultRulesTest", "DetOperations", "ExampleTests", + "modules": [ "DefaultRulesTest", "DetOps", "ExampleTests", "ExamplesFromManual", "FloatTest", "HigherOrder", "Nats", "SEBF", "Sum", "SortSpec", "Tree" ] }, diff --git a/src/CurryCheck.curry b/src/CurryCheck.curry index 321a548..13d099d 100644 --- a/src/CurryCheck.curry +++ b/src/CurryCheck.curry @@ -31,8 +31,8 @@ import AbstractCurry.Files import AbstractCurry.Select import AbstractCurry.Build import qualified AbstractCurry.Pretty as ACPretty -import AbstractCurry.Transform ( renameCurryModule, trCTypeExpr - , updCProg, updQNamesInCProg ) +import AbstractCurry.Transform ( renameCurryModule, trCTypeExpr, updCProg + , updQNamesInCProg, updQNamesInCFuncDecl ) import Analysis.Termination ( Productivity(..) ) import qualified FlatCurry.Types as FC import FlatCurry.Files @@ -56,7 +56,7 @@ ccBanner :: String ccBanner = unlines [bannerLine,bannerText,bannerLine] where bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++ - packageVersion ++ " of 16/10/2018)" + packageVersion ++ " of 30/10/2018)" bannerLine = take (length bannerText) (repeat '-') -- Help text @@ -482,17 +482,17 @@ classifyTest opts prog test = -- 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 tuple consisting of all actual tests, -- all ignored tests, the name of all operations with defined preconditions -- (needed to generate meaningful equivalence tests), -- and the public version of the original module. -transformTests :: Options -> String -> CurryProg +transformTests :: Options -> String -> [CFuncDecl] -> CurryProg -> IO ([CFuncDecl],[CFuncDecl],[QName],CurryProg) -transformTests opts srcdir +transformTests opts srcdir theofuncs prog@(CurryProg mname imps dfltdecl clsdecls instdecls 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) @@ -691,13 +691,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 @@ -707,14 +707,16 @@ genDetProp prefuns (CmtFunc _ qf ar vis texp rules) = genDetProp prefuns (CFunc qf ar vis texp rules) genDetProp prefuns (CFunc (mn,fn) ar _ (CQualType clscon texp) _) = CFunc (mn, forg ++ isDetSuffix) ar Public - (CQualType (addShowContext clscon) (propResultType texp)) + (CQualType (foldr addEqShowContext (addShowContext clscon) rtypevars) + (propResultType texp)) [simpleRule (map CPVar cvars) $ addPreCond prefuns [(mn,forg)] cvars rnumcall ] where - forg = take (length fn - 9) fn - cvars = map (\i -> (i,"x"++show i)) [1 .. ar] - forgcall = applyF (mn,forg) (map CVar cvars) - rnumcall = applyF (easyCheckModule,"#<") [forgcall, cInt 2] + rtypevars = tvarsOfType (resultType texp) + forg = take (length fn - 9) fn + cvars = map (\i -> (i,"x"++show i)) [1 .. ar] + forgcall = applyF (mn,forg) (map CVar cvars) + rnumcall = applyF (easyCheckModule,"#<") [forgcall, cInt 2] -- Generates auxiliary (base-type instantiated) test functions for -- polymorphically typed test function. @@ -792,11 +794,16 @@ defaultQualType (CQualType (CContext allclscon) ftype) = isTVar te = case te of CTVar _ -> True _ -> False --- Add a "Show" class context to all types occurring in the context. +-- Adds a "Show" class context to all types occurring in the context. addShowContext :: CContext -> CContext addShowContext (CContext clscons) = CContext (nub (clscons ++ (map (\t -> (pre "Show",t)) (map snd clscons)))) +-- Adds `Eq` and `Show` class contexts for the given type variable. +addEqShowContext :: CTVarIName -> CContext -> CContext +addEqShowContext tvar (CContext clscons) = + CContext (nub (clscons ++ map (\c -> (pre c, CTVar tvar)) ["Eq","Show"])) + ------------------------------------------------------------------------- -- Transforms a possibly changed test name (like "test_ON_BASETYPE") @@ -871,9 +878,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,preCondOps,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 92a7144..1782f28 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 c3a4004..ca36f1e 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 October 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 ------------------------------------------------------------------------ -- GitLab