README revision f63a335a037098b08817e7137087d42240be74c1
f63a335a037098b08817e7137087d42240be74c1Christian MaederThis README belongs to a "The heterogeneous tool set" (Hets) release
f63a335a037098b08817e7137087d42240be74c1Christian Maeder(and does not apply to sources directly obtained via cvs).
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
87e1c83f10355e0fe80761367b75f83bc682770aTill MossakowskiInformation not contained here can be found in the Hets user guide
87e1c83f10355e0fe80761367b75f83bc682770aTill Mossakowski(doc/UserGuide.pdf) or on the Hets web page (www.tzi.de/cofi/hets).
87e1c83f10355e0fe80761367b75f83bc682770aTill Mossakowski
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till MossakowskiThe subject of this release is a binary "hets" that is able to analyse
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederheterogeneous and in particular CASL specifications.
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
f63a335a037098b08817e7137087d42240be74c1Christian MaederThe sources need to be compiled with ghc Glasgow Haskell Compiler
f63a335a037098b08817e7137087d42240be74c1Christian Maeder(www.haskell.org/ghc). Haskell is also a part of Hets via
f63a335a037098b08817e7137087d42240be74c1Christian Maeder"Programatica" (www.cse.ogi.edu/PacSoft/projects/programatica).
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
f63a335a037098b08817e7137087d42240be74c1Christian MaederBeside output written to the console (stdout) or to files hets can
f63a335a037098b08817e7137087d42240be74c1Christian Maederdisplay graphs using "uDraw(Graph)", formerly "daVinci"
f63a335a037098b08817e7137087d42240be74c1Christian Maeder(www.informatik.uni-bremen.de/uDrawGraph)
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
f63a335a037098b08817e7137087d42240be74c1Christian MaederFor hets to find "uDrawGraph", the environment variables UDG_HOME and
f63a335a037098b08817e7137087d42240be74c1Christian MaederUNIDAVINCI must be set to the installation directory of uDraw(Graph) and to
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederthe actual executable, respectively.
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
f63a335a037098b08817e7137087d42240be74c1Christian Maederexport UNIDAVINCI=$UDG_HOME/bin/uDrawGraph
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
f63a335a037098b08817e7137087d42240be74c1Christian MaederA typical call of hets is then: hets -g Basic/Numbers.casl
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
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)
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maeder
2295e38944bfcd91b9507e2fa9abe5a561817648Till MossakowskiThe heterogeneous tool set (Hets) is mainly maintained by
f63a335a037098b08817e7137087d42240be74c1Christian MaederChristian Maeder (maeder@tzi.de, initials CM) and Till Mossakowski
f63a335a037098b08817e7137087d42240be74c1Christian Maeder(till@tzi.de, initials TM). The mailing list is hets-devel@tzi.de.
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowski
87e1c83f10355e0fe80761367b75f83bc682770aTill MossakowskiOverview of source modules, with maintainers:
87e1c83f10355e0fe80761367b75f83bc682770aTill MossakowskiFor more details, see the Haddock documentation in docs/
87e1c83f10355e0fe80761367b75f83bc682770aTill Mossakowski(after generation with "make doc")
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski--------------------------------------------------------
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till Mossakowski
f63a335a037098b08817e7137087d42240be74c1Christian MaederLICENCE.txt Licence information (english) (TM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederLIZENZ.txt Licence information (german) (TM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederINSTALL Installation and compilation instructions (CM)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiMakefile GNU-Makefile to compile sources (Klaus Luettich)
f63a335a037098b08817e7137087d42240be74c1Christian MaederREADME This file (TM/CM)
f63a335a037098b08817e7137087d42240be74c1Christian Maederhets.hs Top-level Haskell module for hets (TM)
f63a335a037098b08817e7137087d42240be74c1Christian Maederversion_nr Current version (TM)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiATC/ Conversion from and to ATerms (Klaus Luettich)
f63a335a037098b08817e7137087d42240be74c1Christian MaederCASL/ Instance of Logic: CASL (TM/CM/Martin Kuehl)
f63a335a037098b08817e7137087d42240be74c1Christian MaederCoCASL/ Instance of Logic: CoCASL (CM/TM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederCOL/ Instance of Logic: COL (TM)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCommon/ Modules common to all logics
f63a335a037098b08817e7137087d42240be74c1Christian MaederCommon/ATerm/ Conversion from and to ATerms (CM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederCommon/Lib/ Set, Map, Graph, Rel modules (CM)
f5f33d4959160b579024d387d0235ed338341dc5Till MossakowskiCommon/PrettyPrint.hs pretty printing (Klaus Luettich)
f5f33d4959160b579024d387d0235ed338341dc5Till Mossakowski pretty printing should get an own directory
f63a335a037098b08817e7137087d42240be74c1Christian MaederComorphisms/ Comorphisms of the logic graph (TM)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiCspCASL/ Instance of Logic: CspCASL (Markus Roggenbach)
f63a335a037098b08817e7137087d42240be74c1Christian Maederdoc/ Documentation (TM)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskidocs/ Haddock generated documentation (Klaus Luettich)
f63a335a037098b08817e7137087d42240be74c1Christian Maederghc/ ghc-specific "coerce" (CM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederGUI/ GUI for displaying development graphs
f63a335a037098b08817e7137087d42240be74c1Christian Maeder (TM/Jorina Gerken)
f63a335a037098b08817e7137087d42240be74c1Christian MaederHasCASL/ Instance of Logic: HasCASL (CM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederHaskell/ Instance of Logic: Haskell
f63a335a037098b08817e7137087d42240be74c1Christian Maeder based on Programatica (CM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederHatchet/ old Haskell Logic (CM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederDriver/ Command line interface (Klaus Luettich)
f63a335a037098b08817e7137087d42240be74c1Christian MaederIsabelle/ Instance of Logic: Isabelle (CM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederLogic/ Infrastructure for logic independence (TM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederModal/ Instance of Logic: ModalCASL (TM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederProofs/ Heterogeneous proof engine (TM/Jorina Gerken)
f63a335a037098b08817e7137087d42240be74c1Christian MaederStatic/ Heterogeneous development graphs and
f63a335a037098b08817e7137087d42240be74c1Christian Maeder static analysis (TM/Maciek Makowski)
f63a335a037098b08817e7137087d42240be74c1Christian MaederSyntax/ Heterogeneous syntax and parsing (TM/CM)
f63a335a037098b08817e7137087d42240be74c1Christian MaederToHaskell/ translation to Haskell (CM)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederutils/ Utilities
f63a335a037098b08817e7137087d42240be74c1Christian Maederutils/DrIFT-src/ DrIFT for polytpyic conversion functions
f63a335a037098b08817e7137087d42240be74c1Christian Maeder (Klaus Luettich)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiutils/GenerateRules/ generate files to be DRIFTed (Klaus Luettich)
f63a335a037098b08817e7137087d42240be74c1Christian Maederutils/InlineAxioms parse inline axioms (TM/CM)