| License | GPLv2 or higher, see LICENSE.txt |
|---|---|
| Maintainer | nevrenato@gmail.com |
| Stability | experimental |
| Portability | not portable |
| Safe Haskell | None |
TopHybrid.StatAna
Description
Description : Static analysis of hybrid logic with an arbitrary logic below.
Documentation
thAna :: (Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
Examining the list of formulas and collecting results
Analyses first the underlying spec; Then analyses the top spec (without the axioms) and merges the resulting sig with the underlying one. Also translates the underlying axioms into hybridized ones, so that in the end all axioms are of the same type; Next analyses the hybrid axioms and puts them together with the already translated axioms. Finnaly prepares the tuple format for outputting.