Hets is the main analysis tool for the specification language heterogeneous CASL. Heterogeneous CASL (HetCASL, see ) combines the specification language CASL with CASL extensions and sublanguages, as well as completely different logics and even programming languages such as Haskell, including its module system. Hets provides parsing, static analysis and proof management (via development graphs), as well as many other functionalities. Hets is written in Haskell (see and ) The general background of Hets is explained in /Heterogeneous specification and the heterogeneous tool set/ (). A short introduction is given in . The Hets modules are grouped using hierarchical modules (where modules can be grouped into folders); we here only discuss the top view on this hierarchy. For a more details, look at the descriptions of the folders or the individual modules. The folder "Logic" contains the infrastructure needed for presenting a logic to Hets. This is complemented by folders working at the heterogeneous level --- the code in modules in these folders is parameterized over an arbitrary but fixed logic graph. Existential types are used for implementing the heterogeneity, see . The folder /Syntax/ (see "Syntax.ADoc") provides abstract syntax and parsing of heterogeneous structured specifications. "Static" is for the static analysis, based on the verification static semantics for Heterogeneous CASL. "Static.DevGraph" contains the data structures for heterogeneous development graphs, including proof management. Finally, the folder "Proofs" contains an implementation of the proof calculus for heterogeneous development graphs. The folders "CASL", "CoCASL", "HasCASL", "Haskell", "CspCASL", "Modal", "Isabelle" contain different instances of the type class 'Logic.Logic.Logic' of the module "Logic.Logic". These instances always are contained in a module named /Logic_xxx/, where /xxx/ is the name of the language at hand. Since the integration of a new logic into Hets requires writing a new instantiation of the type class 'Logic.Logic.Logic', it is advisable to consult the module /Logic_xxx/ (and the modules imported there) for some logic that is in some sense similar to the new logic to be integrated. In particular, we have implemented the CASL logic in such a way that much of the folder "CASL" can be re-used for CASL extensions as well; this is achieved via /holes/ (realized via polymorphic variables) in the types for signatures, morphisms, abstract syntax etc. This eases integration of CASL extensions and keeps the effort quite moderate. The folder "Comorphisms" contains various comorphisms and other translations that constitute the logic graph. Note that these modules can be compiled independently of the logic independent heterogeneous modules listed above. The module "Comorphisms.LogicList" assembles all the logics into one (heterogeneous) list, while "Comorphisms.LogicGraph" builds up the logic graph, i.e. it assembles all the (co)morphisms among the logics, and also specifies which ones are standard inclusions. This module also provides a partial union for logics, which is crucial for the static analysis of unions of specifications (which may occur explicitly or implicitly). Last but not least, there are general purpose folders. The most important one is the folder "Common". It contains general purpose libraries, e.g. for relations, and for parsing and pretty printing. "Common.Result" provides a monad for error handling and error messages that is used at many places throughout Hets. The folder "ATC" is for conversion from and to shared ATerms . The /utils/ folder contains tools like /DriFT/. The command line interface is contained in "Driver", the graphical interface in "GUI". The latter is based on the UniForM Workbench that provides an event system and encapsulations of TclTk and uDraw(Graph) , . Hets is also based on the following third-party libraries: * expat for fast XML parsing, see * The combinator parser library Parsec, see , and "Propositional.Parse_AS_Basic" for a sample use * finite sets and maps, see * finite graphs from the functional graph library (fgl), see and * the xml light package, see Visit "Driver.Version" for the date of this documentation.