This README belongs to a Hets release (and does not apply to

sources directly obtained via cvs).

The subject of this release is a binary "hets" that is able to analyse

heterogeneous and in particular CASL specifications.

The sources need to be compiled with ghc Glasgow Haskell Compiler

(www.haskell.org/ghc).

The output of hets, if the input is successfully accepted, can be

displayed by "daVinci".

daVinci is maintained by b-novative and b-novative holds all rights.

This release may be accompanied with free binary releases of daVinci

Version 2.1, but daVinci 2.1 is no longer supported or maintained!

However, you are encouraged to obtain the latest version of daVinci

Presenter (currently 3.0.5) from http://www.b-novative.com that is

free for academic purposes.

Linux: the linux binary release of daVinci 2.1 relies on the old

shlibs5 that must be installed on your system (if ./daVinci cannot be

found/executed, then shlibs5 are missing)

Solaris: the solaris binary release of daVinci 2.1 should work without

problems

Macintosh (Darwin): there is no release of daVinci for Macintosh, but

b-novative may have one in the mean time

For best quality, get the latest version of daVinci from b-novative.

For hets to find daVinci, the environment variables DAVINCIHOME and

UNIDAVINCI must be set to the installation directory of daVinci and to

the actual executable, respectively.

export DAVINCIHOME=<path>/daVinci_V2.1

export UNIDAVINCI=<path>/daVinci_V2.1/daVinci

A typical call of hets is then: <path>/hets -g Basic/Numbers.casl

If you need to rebuild the hets binary follow the instructions in INSTALL

(This README belongs a to release created by "make release", in case

that you obtained the HetCATS sources as CVS tree)

The heterogeneous tool set (Hets) is mainly maintained by

Christian Maeder (maeder@tzi.de) and Till Mossakowski

(till@tzi.de). The mailing list is hets@tzi.de.

Files in the Tools/Hets/src directory:

--------------------------------------

LICENCE.txt Licence information (english)

LIZENZ.txt Licence information (german)

INSTALL Installation and compilation instructions

Makefile GNU-Makefile to compile sources

README This file

hets.hs Top-level Haskell module for hets

version_nr

ATC/ Conversion from and to ATerms (specific)

CASL/ Instance of Logic: CASL

Common/ Modules common to all logics

Common/ATerm/ Conversion from and to ATerms (general)

Common/Lib/ Third-party modules

Common/Lib/Parsec/ Parsec combinator parser

Comorphisms/ Comorphisms of the logic graph

CspCASL/ Instance of Logic: CspCASL

ghc/ Some ghc-specific stuff

GUI/ GUI for displaying development graphs

HasCASL/ Instance of Logic: HasCASL

Haskell/ Instance of Logic: Haskell

Haskell/Hatchet/ Static anaylsis of Haskell

Haskell/Language/ Haskell syntax in Haskell

hetcats/ Command line interface

hugs/ Some hugs-specific stuff

Logic/ Infrastructure for logic independence

Proofs/ Heterogeneous proof engine

Static/ Heterogeneous development graphs and static analysis

Syntax/ Heterogeneous syntax and parsing

utils/ Utilities

utils/DrIFT-src/ DrIFT (for polytpyic conversion functions)

utils/GenerateRules/ generate files to be DRIFTed