Commit b329749b authored by Michael Hanus 's avatar Michael Hanus

Static checking of contracts and equivalence properties improved

parent 5bea7b80
......@@ -4,17 +4,20 @@
-- that the implementation is satisfies the specification
-- and the post-condition.
perm :: [a] -> [a]
perm [] = []
perm (x:xs) = insert x (perm xs)
where
insert x ys = x : ys
insert x (y:ys) = y : insert x ys
sorted :: Ord a => [a] -> Bool
sorted [] = True
sorted [_] = True
sorted (x:y:ys) | x<=y && sorted (y:ys) = True
-- Postcondition: input and output lists should have the same length
sort'post :: [Int] -> [Int] -> Bool
sort'post xs ys = length xs == length ys
-- Specification of sort:
......
......@@ -8,6 +8,7 @@ append :: [a] -> [a] -> [a]
append xs ys = xs ++ ys
-- Postcondition: append add length of input lists.
append'post :: [a] -> [a] -> [a] -> Bool
append'post xs ys zs = length xs + length ys == length zs
-- We formulate the postcondition as a property:
......
......@@ -10,17 +10,20 @@
import Test.Prop
perm :: [a] -> [a]
perm [] = []
perm (x:xs) = ndinsert x (perm xs)
where
ndinsert x ys = x : ys
ndinsert x (y:ys) = y : ndinsert x ys
sorted :: Ord a => [a] -> Bool
sorted [] = True
sorted [_] = True
sorted (x:y:ys) | x<=y && sorted (y:ys) = True
-- 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
-- Specification of sort:
......
......@@ -10,6 +10,7 @@
"ansi-terminal" : ">= 0.0.1",
"cass-analysis" : ">= 2.0.0",
"cass" : ">= 2.0.0",
"contracts" : ">= 0.0.1",
"currypath" : ">= 0.0.1",
"easycheck" : ">= 0.0.1",
"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 @@
--- (together with possible preconditions).
---
--- @author Michael Hanus, Jan-Patrick Baye
--- @version January 2019
--- @version April 2019
-------------------------------------------------------------------------
import Char ( toUpper )
......@@ -33,6 +33,7 @@ import qualified AbstractCurry.Pretty as ACPretty
import AbstractCurry.Transform ( renameCurryModule, trCTypeExpr, updCProg
, updQNamesInCProg, updQNamesInCFuncDecl )
import Analysis.Termination ( Productivity(..) )
import Contract.Names
import qualified FlatCurry.Types as FC
import FlatCurry.Files
import qualified FlatCurry.Goodies as FCG
......@@ -48,7 +49,7 @@ import CC.Config ( packagePath, packageVersion )
import CC.Helpers ( ccLoadPath )
import CC.Options
import CheckDetUsage ( checkDetUse, containsDetOperations)
import ContractUsage
import Contract.Usage ( checkContractUsage )
import DefaultRuleUsage ( checkDefaultRules, containsDefaultRules )
import PropertyUsage
import SimplifyPostConds ( simplifyPostConditionsWithTheorems )
......@@ -61,7 +62,7 @@ ccBanner :: String
ccBanner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++
packageVersion ++ " of 02/01/2019)"
packageVersion ++ " of 29/04/2019)"
bannerLine = take (length bannerText) (repeat '-')
-- Help text
......@@ -476,7 +477,8 @@ classifyTest opts prog test =
EquivTest tname f1 f2 (defaultingType qtexp) 0
(CTyped (CSymbol f1) qtexp, CTyped (CSymbol f2) _) ->
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
defaultingType = poly2defaultType opts . typeOfQualType . defaultQualType
......@@ -873,13 +875,16 @@ staticProgAnalysis :: Options -> String -> String -> CurryProg
-> IO ([String],[(QName,String)])
staticProgAnalysis opts modname progtxt prog = do
putStrIfDetails opts "Checking source code for static errors...\n"
fcyprog <- readFlatCurry modname
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 []
let defruleerrs = if optSource opts then checkDefaultRules prog else []
untypedprog <- readUntypedCurry modname
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]
missingCPP =
if (containsDefaultRules prog || containsDetOperations untypedprog)
......
......@@ -3,7 +3,7 @@
--- a Curry program.
---
--- @author Michael Hanus
--- @version January 2019
--- @version April 2019
------------------------------------------------------------------------
module PropertyUsage
......@@ -12,7 +12,8 @@ module PropertyUsage
) where
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,
......@@ -40,8 +41,15 @@ isPropIOType texp = case texp of
isEquivProperty :: CFuncDecl -> Maybe (CExpr,CExpr)
isEquivProperty fdecl =
case funcRules fdecl of
[CRule [] (CSimpleRhs (CApply (CApply (CSymbol prop) e1) e2) [])]
-> if isEquivSymbol prop then Just (e1,e2) else Nothing
[CRule args (CSimpleRhs (CApply (CApply (CSymbol prop) e1) e2) [])]
-> 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
where
isEquivSymbol (qn,mn) = isCheckModule qn && mn=="<=>"
......
......@@ -21,6 +21,7 @@ module SimplifyPostConds
import AbstractCurry.Types
import AbstractCurry.Select
import AbstractCurry.Build
import Contract.Names
import List (last, maximum)
import Maybe (maybeToList)
import ReadShowTerm (readQTerm)
......@@ -30,8 +31,6 @@ import Rewriting.Position
import Rewriting.Substitution
import Rewriting.Rules
import ContractUsage
-- Simplify the postconditions contained in the third argument w.r.t. a given
-- list of theorems (second argument).
-- 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