Hets is the main analysis tool for the specification

language heterogeneous CASL. Heterogeneous CASL (HetCASL, see

<http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/index_e.htm>) 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 <http://www.haskell.org> and

<http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/developers_e.htm>)

The general background of Hets is explained in /Heterogeneous

specification and the heterogeneous tool set/

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

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

<http://haskell.org/hawiki/ExistentialTypes>. 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 sets, maps and 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 (see

<http://www.nomaware.com/monads/html> for an introduction to monads).

The folder "ATC" is

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 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>. The UniForm

Workbench provides an event system and encapsulations of TclTk

<http://www.informatik.uni-bremen.de/htk/> and uDraw(Graph)

<http://www.informatik.uni-bremen.de/uDrawGraph/en/index.html> (see

module "GraphDisp").

The workbench documentation generated by haddock starts in

<www/index.html>;

unfortunately, the Workbench does not use hierarchical module names

yet.

Visit "Driver.Version" for the date of this documentation.