| Copyright | (c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Ewaryst.Schulz@dfki.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
CSL.Analysis
Contents
Description
Static Analysis for EnCL
- withName :: Annoted CMD -> Int -> Named CMD
- analyzeFormula :: Sign -> Annoted CMD -> Int -> Result (Named CMD)
- splitSpec :: BASIC_SPEC -> Sign -> Result (Sign, [Named CMD])
- anaBasicItem :: (Sign, Int) -> Annoted BASIC_ITEM -> Result ((Sign, Int), Maybe (Named CMD))
- addTokens :: Sign -> [Token] -> Sign
- addVarDecls :: Sign -> [VAR_ITEM] -> Sign
- addEPDecls :: Sign -> [(Token, EPDomain)] -> Sign
- addEPDomDecls :: Sign -> [(Token, APInt)] -> Sign
- addEPDefVals :: Sign -> [(Token, APInt)] -> Sign
- addPairsToSig :: (Sign -> a -> b -> Sign) -> Sign -> [(a, b)] -> Sign
- basicCSLAnalysis :: (BASIC_SPEC, Sign, a) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
Basic Analysis Functions
analyzeFormula :: Sign -> Annoted CMD -> Int -> Result (Named CMD)
takes a signature and a formula and a number. It analyzes the formula and returns a formula with diagnosis
splitSpec :: BASIC_SPEC -> Sign -> Result (Sign, [Named CMD])
Extracts the axioms and the signature of a basic spec
anaBasicItem :: (Sign, Int) -> Annoted BASIC_ITEM -> Result ((Sign, Int), Maybe (Named CMD))
Add a single basic item to the signature. EP_defvals cannot be added if the corresponding EP_decl is not yet defined.
addVarDecls :: Sign -> [VAR_ITEM] -> Sign
adds the specified var items to the signature
addEPDecls :: Sign -> [(Token, EPDomain)] -> Sign
addEPDomDecls :: Sign -> [(Token, APInt)] -> Sign
addEPDefVals :: Sign -> [(Token, APInt)] -> Sign
addPairsToSig :: (Sign -> a -> b -> Sign) -> Sign -> [(a, b)] -> Sign
basicCSLAnalysis :: (BASIC_SPEC, Sign, a) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
stepwise extends an initially empty signature by the basic spec bs. The resulting spec contains analyzed axioms in it. The result contains: (1) the basic spec (2) the new signature + the added symbols (3) sentences of the spec