| definition: |
genSpecTest :: Options -> [QName] -> [QName] -> [String] -> CFuncDecl
-> [CFuncDecl]
genSpecTest opts prefuns specops prooffnames (CmtFunc _ qf ar vis texp rules) =
genSpecTest opts prefuns specops prooffnames (CFunc qf ar vis texp rules)
genSpecTest opts prefuns specops prooffnames
(CFunc qf@(mn,fn) _ _ (CQualType clscon texp) _)
| qf `notElem` specops || existsProofFor (orgQName sptname) prooffnames
= []
| optEquiv opts == Ground
= [genSpecGroundEquivTest prefuns qf clscon texp]
| otherwise
= [CFunc sptname 0 Public
(emptyClassType (propResultType unitType))
[simpleRule [] (applyF (easyCheckModule,"<=>")
[constF qf, constF (mn,toSpecName fn)])]]
where
sptname = (mn, fn ++ satSpecSuffix) -- name of generated specification test
|
| demand: |
argument 5 |
| deterministic: |
deterministic operation |
| documentation: |
-- Transforms a function declaration into a specification test if -- there is a specification for this function (i.e., an operation named -- f'spec). The generated specification test has the form -- fSatisfiesSpecification = f <=> f'spec |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| name: |
genSpecTest |
| precedence: |
no precedence defined |
| result-values: |
{:,[]}
|
| signature: |
CC.Options.Options -> [(String, String)] -> [(String, String)] -> [String] -> AbstractCurry.Types.CFuncDecl -> [AbstractCurry.Types.CFuncDecl] |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |