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 |

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) Source #

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]) Source #

Extracts the axioms and the signature of a basic spec

anaBasicItem :: (Sign, Int) -> Annoted BASIC_ITEM -> Result ((Sign, Int), Maybe (Named CMD)) Source #

Add a single basic item to the signature. EP_defvals cannot be added if the corresponding EP_decl is not yet defined.

basicCSLAnalysis :: (BASIC_SPEC, Sign, a) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source #

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