README revision 39debaf3f18854486e9c5d21fecf3eb2630e5aa7
2295e38944bfcd91b9507e2fa9abe5a561817648Till MossakowskiThis README belongs to a Hets release (and does not apply to
2295e38944bfcd91b9507e2fa9abe5a561817648Till Mossakowskisources directly obtained via cvs).
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till MossakowskiThe subject of this release is a binary "hets" that is able to analyse
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederheterogeneous and in particular CASL specifications.
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till MossakowskiThe sources need to be compiled with ghc Glasgow Haskell Compiler
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederThe output of hets, if the input is successfully accepted, can be
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederdisplayed by "daVinci".
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederdaVinci is maintained by b-novative and b-novative holds all rights.
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederThis release may be accompanied with free binary releases of daVinci
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederVersion 2.1, but daVinci 2.1 is no longer supported or maintained!
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederHowever, you are encouraged to obtain the latest version of daVinci
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederPresenter (currently 3.0.5) from http://www.b-novative.com that is
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederfree for academic purposes.
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederLinux: the linux binary release of daVinci 2.1 relies on the old
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maedershlibs5 that must be installed on your system (if ./daVinci cannot be
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederfound/executed, then shlibs5 are missing)
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederSolaris: the solaris binary release of daVinci 2.1 should work without
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederMacintosh (Darwin): there is no release of daVinci for Macintosh, but
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederb-novative may have one in the mean time
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederFor best quality, get the latest version of daVinci from b-novative.
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederFor hets to find daVinci, the environment variables DAVINCIHOME and
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederUNIDAVINCI must be set to the installation directory of daVinci and to
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederthe actual executable, respectively.
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederexport DAVINCIHOME=<path>/daVinci_V2.1
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederexport UNIDAVINCI=<path>/daVinci_V2.1/daVinci
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederA typical call of hets is then: <path>/hets -g Basic/Numbers.casl
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederIf you need to rebuild the hets binary follow the instructions in INSTALL
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder(This README belongs a to release created by "make release", in case
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederthat you obtained the HetCATS sources as CVS tree)
2295e38944bfcd91b9507e2fa9abe5a561817648Till MossakowskiThe heterogeneous tool set (Hets) is mainly maintained by
7b66a58641c3e6f6369c95d5bc16beaad20749a0Christian MaederChristian Maeder (maeder@tzi.de) and Till Mossakowski
7b66a58641c3e6f6369c95d5bc16beaad20749a0Christian Maeder(till@tzi.de). The mailing list is hets@tzi.de.
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till MossakowskiFiles in the Tools/Hets/src directory:
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowski--------------------------------------
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till MossakowskiREADME This file
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskihets Hets binary
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till MossakowskiUserGuide.ps Hets documentaion
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskidocs/ Overview and index for Hets sources
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/ Hets sources
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/ATC/ Conversion from and to ATerms (specific)
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/aterm_conv/ ATerm Conversion
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/CASL/ Instance of Logic: CASL
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Common/ Modules common to all logics
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Common/ATerm/ Conversion from and to ATerms (general)
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Common/Lib/ Third-party modules
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Common/Lib/Graph/ Functional Graph Library
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Common/Lib/Parsec/ Parsec combinator parser
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Comorphisms/ Comorphisms of the logic graph
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/CspCASL/ Instance of Logic: CspCASL
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/docs/ Haddock documentation
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/ghc/ Some ghc-specific stuff
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/GUI/ GUI for displaying development graphs
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/HasCASL/ Instance of Logic: HasCASL
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Haskell/ Instance of Logic: Haskell
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Haskell/Hatchet/ Static anaylsis of Haskell
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Haskell/Language/ Haskell syntax in Haskell
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/haterm-1.0/ ATerm Conversion
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/hetcats/ Command line interface
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/hugs/ Some hugs-specific stuff
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Logic/ Infrastructure for logic independence
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/mini/ Some toy version of Hets, used in a paper
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Modal/ Instance of logic: modal logic
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Proofs/ Heterogeneous proof engine
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Static/ Heterogeneous development graphs and static analysis
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/Syntax/ Heterogeneous syntax and parsing
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/ToHaskell/ Translation from HasCASL to Haskell
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/utils/AG-src/ Static analyser generator (not used by Hets)
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowskisrc/utils/DrIFT-src/ DrIFT (for polytpyic conversion functions)