README revision f946026468db3a4a74f5f7651a86b22c58a708d1
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.
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederThe 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
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederIf you need to rebuild the hets binary follow the instructions in INSTALL
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maeder(This README belongs a to release created by "make release", in case
f946026468db3a4a74f5f7651a86b22c58a708d1Christian 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--------------------------------------
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederLICENCE.txt Licence information (english)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederLIZENZ.txt Licence information (german)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederINSTALL Installation and compilation instructions
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederMakefile GNU-Makefile to compile sources
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederREADME This file
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederhets.hs Top-level Haskell module for hets
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederATC/ Conversion from and to ATerms (specific)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCASL/ Instance of Logic: CASL
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCommon/ Modules common to all logics
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCommon/ATerm/ Conversion from and to ATerms (general)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCommon/Lib/ Third-party modules
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCommon/Lib/Parsec/ Parsec combinator parser
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederComorphisms/ Comorphisms of the logic graph
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCspCASL/ Instance of Logic: CspCASL
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederghc/ Some ghc-specific stuff
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederGUI/ GUI for displaying development graphs
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederHasCASL/ Instance of Logic: HasCASL
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederHaskell/ Instance of Logic: Haskell
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederHaskell/Hatchet/ Static anaylsis of Haskell
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederHaskell/Language/ Haskell syntax in Haskell
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederhetcats/ Command line interface
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederhugs/ Some hugs-specific stuff
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederLogic/ Infrastructure for logic independence
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederProofs/ Heterogeneous proof engine
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederStatic/ Heterogeneous development graphs and static analysis
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederSyntax/ Heterogeneous syntax and parsing
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederutils/ Utilities
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederutils/DrIFT-src/ DrIFT (for polytpyic conversion functions)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederutils/GenerateRules/ generate files to be DRIFTed