Module Contract.Usage

Author
Michael Hanus
Version
May 2021

This module contains some operations to check the correct usage of contracts (i.e., the occurrences and types of specification and pre/postconditions) in a FlatCurry program.

Exported Functions:
checkContractUsage

Exported Functions

checkContractUsage :: String -> [(String, TypeExpr)] -> [((String, String), String)]  Deterministic 

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.