PAKCS
Exported names: Imported modules:

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: April 2019

Summary of exported operations:

checkContractUsage :: String -> [(String,TypeExpr)] -> [((String,String),String)]   
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)]   

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.