1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
------------------------------------------------------------------------
--- 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 May 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 (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 (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)
------------------------------------------------------------------------
|
