PAKCS
Exported names: Imported modules:

Module ContractUsage

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

Summary of exported operations:

checkContractUse :: CurryProg -> [((String,String),String)]   
Checks the intended usage of contracts.
isSpecName :: String -> Bool   
toSpecName :: String -> String   
Transform a name into a name of the corresponding specification by adding the suffix "'spec".
fromSpecName :: String -> String   
isPreCondName :: String -> Bool   
toPreCondName :: String -> String   
Transform a name into a name of the corresponding precondition by adding the suffix "'pre".
fromPreCondName :: String -> String   
isPostCondName :: String -> Bool   
toPostCondName :: String -> String   
Transform a name into a name of the corresponding prostcondition by adding the suffix "'post".
fromPostCondName :: String -> String   

Exported operations:

checkContractUse :: CurryProg -> [((String,String),String)]   

Checks the intended usage of contracts.

isSpecName :: String -> Bool   

toSpecName :: String -> String   

Transform a name into a name of the corresponding specification by adding the suffix "'spec".

fromSpecName :: String -> String   

isPreCondName :: String -> Bool   

toPreCondName :: String -> String   

Transform a name into a name of the corresponding precondition by adding the suffix "'pre".

fromPreCondName :: String -> String   

isPostCondName :: String -> Bool   

toPostCondName :: String -> String   

Transform a name into a name of the corresponding prostcondition by adding the suffix "'post".

fromPostCondName :: String -> String