Commit 40441970 authored by Michael Hanus 's avatar Michael Hanus

Names of proof files changed so that module names are included

parent a7704c48
......@@ -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]
......
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:
......
......@@ -2,7 +2,7 @@
open import bool
module PROOF-appendAddLengths
module PROOF-ListProp-appendAddLengths
(Choice : Set)
(choose : Choice → 𝔹)
(lchoice : Choice → Choice)
......
......@@ -2,7 +2,7 @@
open import bool
module PROOF-sortPreservesLength
module PROOF-SortSpec-sortPreservesLength
(Choice : Set)
(choose : Choice → 𝔹)
(lchoice : Choice → Choice)
......
......@@ -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))
......
......@@ -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" ]
},
......
......@@ -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")
......
......@@ -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).
......
......@@ -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
------------------------------------------------------------------------
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