Universität Bremen  
  FB 3  
  Group BKB > Research > Formal Methods > Formal specification > Hets > Deutsch
English
 

Hets: download and installation

 

Installers for Hets

needs Sun Java 1.4.2 or later (install with java -jar file.jar)

The installer is available for

A Hets-Live-CD is available for download,too.

It runs on any computer with x86 architecture. Just boot from the CD. This life CD is in an early stage of developement, so you might encounter bugs. The Hets-Live-CD is based on Knoppix.

Hets binaries are available here:

(these are not needed if you used one of the installers from above)

How to install Hets:

Just download the binary and put it somewhere in the $PATH. Download the CASL libraries and set $HETS_LIB to the folder containing these.
Hets is called with

    hets filename.casl

or

    hets filename.het

For entering the command line mode, just call

    hets

For a short description of the options, call

    hets --help

How to install software needed for theorem proving with Hets:

  • For displaying development graphs (with the -g option), you need to install Tcl/Tk (which probably has been already installed on your computer anyway) and uDraw(Graph) (formerly known as daVinci). Set $UNIWISH to the wish binary (which is part of Tcl/Tk), and $UNIDAVINCI to the uDrawGraph binary (if they are not in your $PATH).
  • For interactive theorem proving you may install Isabelle and set $HETS_ISABELLE to the Isabelle binary.
  • For automatic theorem proving you may install SPASS and/or Darwin.
  • The connection of Hets to other theorem provers is under development
 
   
Author: Dr. Christian Maeder
 
  Group BKB 
Last updated: July 3, 2008   impressum