Hets is the main analysis tool for the specification

language heterogeneous CASL. Heterogeneous CASL (HetCASL) 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.

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 detailed background, see /Heterogeneous

specification and the heterogeneous tool set/

(<http://www.tzi.de/~till/papers/habil.ps>).

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. 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. 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: "ATC"

for conversion from and to the

ATerm format

(<http://catamaran.labs.cs.uu.nl/twiki/pt/bin/view/Tools/ATermFormat>)

- most of the

modules have been automatically created using /DriFT/ from the

/utils/ folder. The latter also contains a module

/inlineAxioms/ that can be used to write the axioms for

theoroidal comorphisms in a concise way, namely in the input syntax of

the respective target logic (the identifiers will turn into Haskell

variables and can hence be used for easily producing instances of

axiom schemes). The folder "Common" contains general purpose

libraries, e.g. for sets, maps and relations, and for parsing and

pretty printing. The command line interface is contained in

"Driver", the graphical interface in "GUI".

The latter is based on the

UniForM Workbench <http://www.informatik.uni-bremen.de/uniform/wb>.

There are lots of top-level modules listed below belonging to the Workbench;

unfortunately, the Workbench does not use hierarchical module names yet.