| Copyright | (c) Till Mossakowski, Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | till@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | non-portable(Logic) |
| Safe Haskell | None |
Static.AnalysisLibrary
Description
Static analysis of CASL specification libraries Follows the verification semantics sketched in Chap. IV:6 of the CASL Reference Manual.
- anaLibFileOrGetEnv :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> Maybe LibName -> FilePath -> ResultT IO (LibName, LibEnv)
- anaLibDefn :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LIB_DEFN -> FilePath -> ResultT IO (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
- anaSourceFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> FilePath -> ResultT IO (LibName, LibEnv)
- anaLibItem :: LogicGraph -> HetcatsOpts -> LNS -> LibName -> LibEnv -> DGraph -> ExpOverrides -> LIB_ITEM -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
- anaViewDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts -> ExpOverrides -> IRI -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range -> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
- type LNS = Set LibName
Documentation
anaLibFileOrGetEnv :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> Maybe LibName -> FilePath -> ResultT IO (LibName, LibEnv)
lookup or read a library
anaLibDefn :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LIB_DEFN -> FilePath -> ResultT IO (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
analyze a LIB_DEFN. Parameters: logic graph, default logic, opts, library env, LIB_DEFN. Call this function as follows:
do Result diags res <- runResultT (anaLibDefn ...)
mapM_ (putStrLn . show) diagsanaSourceFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> FilePath -> ResultT IO (LibName, LibEnv)
parsing and static analysis for files Parameters: logic graph, default logic, file name
anaLibItem :: LogicGraph -> HetcatsOpts -> LNS -> LibName -> LibEnv -> DGraph -> ExpOverrides -> LIB_ITEM -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
analyse a LIB_ITEM
anaViewDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts -> ExpOverrides -> IRI -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range -> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
analyse genericity and view type and construct gmorphism