Commit b329749b authored by Michael Hanus 's avatar Michael Hanus

Static checking of contracts and equivalence properties improved

parent 5bea7b80
...@@ -4,17 +4,20 @@ ...@@ -4,17 +4,20 @@
-- that the implementation is satisfies the specification -- that the implementation is satisfies the specification
-- and the post-condition. -- and the post-condition.
perm :: [a] -> [a]
perm [] = [] perm [] = []
perm (x:xs) = insert x (perm xs) perm (x:xs) = insert x (perm xs)
where where
insert x ys = x : ys insert x ys = x : ys
insert x (y:ys) = y : insert x ys insert x (y:ys) = y : insert x ys
sorted :: Ord a => [a] -> Bool
sorted [] = True sorted [] = True
sorted [_] = True sorted [_] = True
sorted (x:y:ys) | x<=y && sorted (y:ys) = True sorted (x:y:ys) | x<=y && sorted (y:ys) = True
-- Postcondition: input and output lists should have the same length -- Postcondition: input and output lists should have the same length
sort'post :: [Int] -> [Int] -> Bool
sort'post xs ys = length xs == length ys sort'post xs ys = length xs == length ys
-- Specification of sort: -- Specification of sort:
......
...@@ -8,6 +8,7 @@ append :: [a] -> [a] -> [a] ...@@ -8,6 +8,7 @@ append :: [a] -> [a] -> [a]
append xs ys = xs ++ ys append xs ys = xs ++ ys
-- Postcondition: append add length of input lists. -- Postcondition: append add length of input lists.
append'post :: [a] -> [a] -> [a] -> Bool
append'post xs ys zs = length xs + length ys == length zs append'post xs ys zs = length xs + length ys == length zs
-- We formulate the postcondition as a property: -- We formulate the postcondition as a property:
......
...@@ -10,17 +10,20 @@ ...@@ -10,17 +10,20 @@
import Test.Prop import Test.Prop
perm :: [a] -> [a]
perm [] = [] perm [] = []
perm (x:xs) = ndinsert x (perm xs) perm (x:xs) = ndinsert x (perm xs)
where where
ndinsert x ys = x : ys ndinsert x ys = x : ys
ndinsert x (y:ys) = y : ndinsert x ys ndinsert x (y:ys) = y : ndinsert x ys
sorted :: Ord a => [a] -> Bool
sorted [] = True sorted [] = True
sorted [_] = True sorted [_] = True
sorted (x:y:ys) | x<=y && sorted (y:ys) = True sorted (x:y:ys) | x<=y && sorted (y:ys) = True
-- Postcondition: input and output lists should have the same length -- Postcondition: input and output lists should have the same length
sort'post :: [Int] -> [Int] -> Bool
sort'post xs ys = length xs == length ys && sorted ys sort'post xs ys = length xs == length ys && sorted ys
-- Specification of sort: -- Specification of sort:
......
...@@ -10,6 +10,7 @@ ...@@ -10,6 +10,7 @@
"ansi-terminal" : ">= 0.0.1", "ansi-terminal" : ">= 0.0.1",
"cass-analysis" : ">= 2.0.0", "cass-analysis" : ">= 2.0.0",
"cass" : ">= 2.0.0", "cass" : ">= 2.0.0",
"contracts" : ">= 0.0.1",
"currypath" : ">= 0.0.1", "currypath" : ">= 0.0.1",
"easycheck" : ">= 0.0.1", "easycheck" : ">= 0.0.1",
"flatcurry" : ">= 2.0.0", "flatcurry" : ">= 2.0.0",
......
------------------------------------------------------------------------
--- This module contains some operations to access contracts (i.e.,
--- specification and pre/postconditions) in a Curry program and
--- an operation to check the correct usage of specifications and
--- and pre/postconditions.
---
--- @author Michael Hanus
--- @version October 2016
------------------------------------------------------------------------
module ContractUsage
( checkContractUse
, isSpecName, toSpecName, fromSpecName
, isPreCondName, toPreCondName, fromPreCondName
, isPostCondName, toPostCondName, fromPostCondName
) where
import AbstractCurry.Types
import AbstractCurry.Select
import AbstractCurry.Build (boolType)
import List
--- Checks the intended usage of contracts.
checkContractUse :: CurryProg -> [(QName,String)]
checkContractUse prog =
let mn = progName prog
allops = map nameArityOfFunDecl (functions prog)
specops = map (\ (n,a) -> (fromSpecName n, a))
(funDeclsWithNameArity isSpecName prog)
preops = map (\ (n,a) -> (fromPreCondName n, a))
(funDeclsWithNameArity isPreCondName prog)
postops = map (\ (n,a) -> (fromPostCondName n, a-1))
(funDeclsWithNameArity isPostCondName prog)
onlyprecond = preops \\ allops
onlypostcond = postops \\ allops
onlyspec = specops \\ allops
errmsg = "No implementation (of right arity) for this "
preerrs = map (\ (n,_) -> ((mn, n++"'pre"), errmsg ++ "precondition"))
onlyprecond
posterrs = map (\ (n,_) -> ((mn, n++"'post"), errmsg ++ "postcondition"))
onlypostcond
specerrs = map (\ (n,_) -> ((mn, n++"'spec"), errmsg ++ "specification"))
onlyspec
in preerrs ++ posterrs ++ specerrs ++ checkPrePostResultTypes prog
checkPrePostResultTypes :: CurryProg -> [(QName,String)]
checkPrePostResultTypes prog =
let allops = functions prog
preops = filter (isPreCondName . snd . funcName) allops
postops = filter (isPostCondName . snd . funcName) allops
errmsg c = c ++ " has illegal type"
preerrs = map (\fd -> (funcName fd, errmsg "Precondition"))
(filter (not . hasBoolResultType) preops)
posterrs = map (\fd -> (funcName fd, errmsg "Postcondition"))
(filter (not . hasBoolResultType) postops)
in preerrs ++ posterrs
hasBoolResultType :: CFuncDecl -> Bool
hasBoolResultType fd = resultType (typeOfQualType (funcType fd)) == boolType
-- Get function names from a Curry module with a name satisfying the predicate:
funDeclsWithNameArity :: (String -> Bool) -> CurryProg -> [(String,Int)]
funDeclsWithNameArity pred prog =
map nameArityOfFunDecl
(filter (pred . snd . funcName) (functions prog))
-- Computes the unqualified name and the arity from the type of the function.
nameArityOfFunDecl :: CFuncDecl -> (String,Int)
nameArityOfFunDecl fd =
(snd (funcName fd), length (argTypes (typeOfQualType (funcType fd))))
-- Is this the name of a specification?
isSpecName :: String -> Bool
isSpecName f = "'spec" `isSuffixOf` f
--- Transform a name into a name of the corresponding specification
--- by adding the suffix "'spec".
toSpecName :: String -> String
toSpecName = (++"'spec")
-- Drop the specification suffix "'spec" from the name:
fromSpecName :: String -> String
fromSpecName f =
let rf = reverse f
in reverse (drop (if take 5 rf == "ceps'" then 5 else 0) rf)
-- Is this the name of a precondition?
isPreCondName :: String -> Bool
isPreCondName f = "'pre" `isSuffixOf` f
--- Transform a name into a name of the corresponding precondition
--- by adding the suffix "'pre".
toPreCondName :: String -> String
toPreCondName = (++"'pre")
-- Drop the precondition suffix "'pre" from the name:
fromPreCondName :: String -> String
fromPreCondName f =
let rf = reverse f
in reverse (drop (if take 4 rf == "erp'" then 4 else 0) rf)
-- Is this the name of a precondition?
isPostCondName :: String -> Bool
isPostCondName f = "'post" `isSuffixOf` f
--- Transform a name into a name of the corresponding prostcondition
--- by adding the suffix "'post".
toPostCondName :: String -> String
toPostCondName = (++"'post")
-- Drop the postcondition suffix "'post" from the name:
fromPostCondName :: String -> String
fromPostCondName f =
let rf = reverse f
in reverse (drop (if take 5 rf == "tsop'" then 5 else 0) rf)
------------------------------------------------------------------------
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
--- (together with possible preconditions). --- (together with possible preconditions).
--- ---
--- @author Michael Hanus, Jan-Patrick Baye --- @author Michael Hanus, Jan-Patrick Baye
--- @version January 2019 --- @version April 2019
------------------------------------------------------------------------- -------------------------------------------------------------------------
import Char ( toUpper ) import Char ( toUpper )
...@@ -33,6 +33,7 @@ import qualified AbstractCurry.Pretty as ACPretty ...@@ -33,6 +33,7 @@ import qualified AbstractCurry.Pretty as ACPretty
import AbstractCurry.Transform ( renameCurryModule, trCTypeExpr, updCProg import AbstractCurry.Transform ( renameCurryModule, trCTypeExpr, updCProg
, updQNamesInCProg, updQNamesInCFuncDecl ) , updQNamesInCProg, updQNamesInCFuncDecl )
import Analysis.Termination ( Productivity(..) ) import Analysis.Termination ( Productivity(..) )
import Contract.Names
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
...@@ -48,7 +49,7 @@ import CC.Config ( packagePath, packageVersion ) ...@@ -48,7 +49,7 @@ import CC.Config ( packagePath, packageVersion )
import CC.Helpers ( ccLoadPath ) import CC.Helpers ( ccLoadPath )
import CC.Options import CC.Options
import CheckDetUsage ( checkDetUse, containsDetOperations) import CheckDetUsage ( checkDetUse, containsDetOperations)
import ContractUsage import Contract.Usage ( checkContractUsage )
import DefaultRuleUsage ( checkDefaultRules, containsDefaultRules ) import DefaultRuleUsage ( checkDefaultRules, containsDefaultRules )
import PropertyUsage import PropertyUsage
import SimplifyPostConds ( simplifyPostConditionsWithTheorems ) import SimplifyPostConds ( simplifyPostConditionsWithTheorems )
...@@ -61,7 +62,7 @@ ccBanner :: String ...@@ -61,7 +62,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 02/01/2019)" packageVersion ++ " of 29/04/2019)"
bannerLine = take (length bannerText) (repeat '-') bannerLine = take (length bannerText) (repeat '-')
-- Help text -- Help text
...@@ -476,7 +477,8 @@ classifyTest opts prog test = ...@@ -476,7 +477,8 @@ classifyTest opts prog test =
EquivTest tname f1 f2 (defaultingType qtexp) 0 EquivTest tname f1 f2 (defaultingType qtexp) 0
(CTyped (CSymbol f1) qtexp, CTyped (CSymbol f2) _) -> (CTyped (CSymbol f1) qtexp, CTyped (CSymbol f2) _) ->
EquivTest tname f1 f2 (defaultingType qtexp) 0 EquivTest tname f1 f2 (defaultingType qtexp) 0
(e1,e2) -> error $ "Illegal equivalence property:\n" ++ (e1,e2) -> error $ "Illegal equivalence property '" ++
snd tname ++ "':\n" ++
showCExpr e1 ++ " <=> " ++ showCExpr e2 showCExpr e1 ++ " <=> " ++ showCExpr e2
defaultingType = poly2defaultType opts . typeOfQualType . defaultQualType defaultingType = poly2defaultType opts . typeOfQualType . defaultQualType
...@@ -873,13 +875,16 @@ staticProgAnalysis :: Options -> String -> String -> CurryProg ...@@ -873,13 +875,16 @@ staticProgAnalysis :: Options -> String -> String -> CurryProg
-> IO ([String],[(QName,String)]) -> IO ([String],[(QName,String)])
staticProgAnalysis opts modname progtxt prog = do staticProgAnalysis opts modname progtxt prog = do
putStrIfDetails opts "Checking source code for static errors...\n" putStrIfDetails opts "Checking source code for static errors...\n"
fcyprog <- readFlatCurry modname
useerrs <- if optSource opts then checkBlacklistUse prog else return [] useerrs <- if optSource opts then checkBlacklistUse prog else return []
seterrs <- if optSource opts then readFlatCurry modname >>= checkSetUse seterrs <- if optSource opts then checkSetUse fcyprog
else return [] else return []
let defruleerrs = if optSource opts then checkDefaultRules prog else [] let defruleerrs = if optSource opts then checkDefaultRules prog else []
untypedprog <- readUntypedCurry modname untypedprog <- readUntypedCurry modname
let detuseerrs = if optSource opts then checkDetUse untypedprog else [] let detuseerrs = if optSource opts then checkDetUse untypedprog else []
contracterrs = checkContractUse prog contracterrs = checkContractUsage modname
(map (\fd -> (snd (FCG.funcName fd), FCG.funcType fd))
(FCG.progFuncs fcyprog))
staticerrs = concat [seterrs,useerrs,defruleerrs,detuseerrs,contracterrs] staticerrs = concat [seterrs,useerrs,defruleerrs,detuseerrs,contracterrs]
missingCPP = missingCPP =
if (containsDefaultRules prog || containsDetOperations untypedprog) if (containsDefaultRules prog || containsDetOperations untypedprog)
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
--- a Curry program. --- a Curry program.
--- ---
--- @author Michael Hanus --- @author Michael Hanus
--- @version January 2019 --- @version April 2019
------------------------------------------------------------------------ ------------------------------------------------------------------------
module PropertyUsage module PropertyUsage
...@@ -12,7 +12,8 @@ module PropertyUsage ...@@ -12,7 +12,8 @@ module PropertyUsage
) where ) where
import AbstractCurry.Types import AbstractCurry.Types
import AbstractCurry.Select (funcType, resultType, typeOfQualType, funcRules) import AbstractCurry.Select ( funcName, funcRules, funcType, resultType
, typeOfQualType )
------------------------------------------------------------------------ ------------------------------------------------------------------------
--- Check whether a function definition is a property, --- Check whether a function definition is a property,
...@@ -40,8 +41,15 @@ isPropIOType texp = case texp of ...@@ -40,8 +41,15 @@ isPropIOType texp = case texp of
isEquivProperty :: CFuncDecl -> Maybe (CExpr,CExpr) isEquivProperty :: CFuncDecl -> Maybe (CExpr,CExpr)
isEquivProperty fdecl = isEquivProperty fdecl =
case funcRules fdecl of case funcRules fdecl of
[CRule [] (CSimpleRhs (CApply (CApply (CSymbol prop) e1) e2) [])] [CRule args (CSimpleRhs (CApply (CApply (CSymbol prop) e1) e2) [])]
-> if isEquivSymbol prop then Just (e1,e2) else Nothing -> if isEquivSymbol prop
then
if null args
then Just (e1,e2)
else error $ "Illegal equivalence property '" ++
snd (funcName fdecl) ++ "':\n" ++
"Non-empty parameter list!"
else Nothing
_ -> Nothing _ -> Nothing
where where
isEquivSymbol (qn,mn) = isCheckModule qn && mn=="<=>" isEquivSymbol (qn,mn) = isCheckModule qn && mn=="<=>"
......
...@@ -21,6 +21,7 @@ module SimplifyPostConds ...@@ -21,6 +21,7 @@ module SimplifyPostConds
import AbstractCurry.Types import AbstractCurry.Types
import AbstractCurry.Select import AbstractCurry.Select
import AbstractCurry.Build import AbstractCurry.Build
import Contract.Names
import List (last, maximum) import List (last, maximum)
import Maybe (maybeToList) import Maybe (maybeToList)
import ReadShowTerm (readQTerm) import ReadShowTerm (readQTerm)
...@@ -30,8 +31,6 @@ import Rewriting.Position ...@@ -30,8 +31,6 @@ import Rewriting.Position
import Rewriting.Substitution import Rewriting.Substitution
import Rewriting.Rules import Rewriting.Rules
import ContractUsage
-- 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).
-- If the verbosity (first argument) is greater than 1, the details -- If the verbosity (first argument) is greater than 1, the details
......
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