Module ToVerifier

A transformation of Curry programs into verification tools.

Author: Michael Hanus

Version: April 2021

Summary of exported operations:

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

Exported operations:

cvBanner :: String  Deterministic 

usageText :: String  Non-deterministic 

main :: IO ()  Non-deterministic 

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

generateTheorems :: Options -> IO ()  Non-deterministic 

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

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

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

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

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

standardConstructors :: [(String,String)]  Deterministic 

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