Module Contract.Usage

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.

Author: Michael Hanus

Version: May 2021

Summary of exported operations:

checkContractUsage :: String -> [(String,TypeExpr)] -> [((String,String),String)]  Deterministic 
Checks the intended usage of contracts, i.e., whether contracts types correspond to types of functions.

Exported operations:

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.