|
definition:
|
checkContractUsage :: String -> [(String,TypeExpr)] -> [(QName,String)]
checkContractUsage mn allopsforall =
let allops = map (\ (n,t) -> (n, stripForall t)) allopsforall
allopsnames = map fst allops
specops = map (\ (n,t) ->
(fromSpecName (decodeContractName n), t))
(filter (isSpecName . fst) allops)
preops = map (\ (n,t) ->
(fromPreCondName (decodeContractName n), t))
(filter (isPreCondName . fst) allops)
postops = map (\ (n,t) ->
(fromPostCondName (decodeContractName n), t))
(filter (isPostCondName . fst) allops)
nonfailops = map (\ (n,t) ->
(fromNonFailName (decodeContractName n), t))
(filter (isNonFailName . fst) allops)
onlyprecond = map fst preops \\ allopsnames
onlypostcond = map fst postops \\ allopsnames
onlyspec = map fst specops \\ allopsnames
onlynonfail = map fst nonfailops \\ allopsnames
errmsg = "No implementation for this "
preerrs = map (\ n -> ((mn, toPreCondName n), errmsg ++ "precondition"))
onlyprecond
posterrs = map (\ n -> ((mn, toPostCondName n),errmsg ++ "postcondition"))
onlypostcond
specerrs = map (\ n -> ((mn, toSpecName n), errmsg ++ "specification"))
onlyspec
nferrs = map (\ n -> ((mn, toNonFailName n),
errmsg ++ "non-fail condition"))
onlynonfail
in preerrs ++ posterrs ++ specerrs ++ nferrs ++
checkNonFailTypes mn allops nonfailops ++
checkPreTypes mn allops preops ++
checkPostTypes mn allops postops ++
checkSpecTypes mn allops specops
|
|
documentation:
|
--- Checks the intended usage of contracts, i.e., whether
--- contracts types correspond to types of functions.
--- The parameter are the module and the list of names and (FlatCurry) types
--- of all functions defined in this module.
--- The result is a list of error messages for qualified function names.
|