Module ToVerifier

A transformation of Curry programs into verification tools.

Author: Michael Hanus

Version: October 2016

Summary of exported operations:

cvBanner :: String   
usageText :: String   
main :: IO ()   
generateTheoremsForModule :: Options -> String -> IO ()   
generateTheorems :: Options -> IO ()   
generateTheorem :: Options -> (String,String) -> IO ()   
getAllTypeDecls :: Options -> [CurryProg] -> [(String,String)] -> [CTypeDecl] -> IO [CTypeDecl]   
Extract all type declarations that are refererred in the types of the given functions.
sortTypeDecls :: [CTypeDecl] -> [CTypeDecl]   
getAllFunctions :: Options -> [CFuncDecl] -> [CurryProg] -> [(String,String)] -> IO (Options,[CurryProg],[CFuncDecl])   
Extract all functions that might be called by a given function.
standardConstructors :: [(String,String)]   

Exported operations:

cvBanner :: String   

usageText :: String   

main :: IO ()   

generateTheoremsForModule :: Options -> String -> IO ()   

generateTheorems :: Options -> IO ()   

generateTheorem :: Options -> (String,String) -> IO ()   

getAllTypeDecls :: Options -> [CurryProg] -> [(String,String)] -> [CTypeDecl] -> IO [CTypeDecl]   

Extract all type declarations that are refererred in the types of the given functions.

getAllFunctions :: Options -> [CFuncDecl] -> [CurryProg] -> [(String,String)] -> IO (Options,[CurryProg],[CFuncDecl])   

Extract all functions that might be called by a given function.

standardConstructors :: [(String,String)]   

Further infos:
  • solution complete, i.e., able to compute all solutions