Commit c3aee946 authored by Michael Hanus 's avatar Michael Hanus

Names of proof files changed so that module names are included

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