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

Hets - the Heterogeneous Tool Set

 
Hets is a parsing, static analysis and proof management tool incorporating various provers and different specification languages, thus providing a tool for heterogeneous specifications. Logic translations are first-class citizens.

Supported languages

The following provers have been connected to Hets:

The structuring constructs of the heterogeneous specification language are those of the language CASL, plus some constructs to select languages (logics) and language translations. The heterogeneous specification language of Hets is called HetCASL. However, Hets can also read other structuring constructs, like those of Haskell, Maude or OWL. All these are mapped to so-called development graphs and processed with a proof calculus for heterogeneous development graphs that allows to decompose global proof obligations into local ones (during this, Hets also needs to compute colimits of theories over the involved logics).

Hets is based on a graph of logics and logic translations. The overall architecture is depicted below. Adding new logics and logic translations to Hets can be done with moderate effort by adding some Haskell code to the Hets source. With the Latin project, this becomes much easier: logics (and in the near future also logic translations) can be declaratively specified in LF.

Obtaining Hets

Documentation

Source code and information for developers

Architecture of Hets
 
   
Author: Dr. Till Mossakowski
 
  Group BKB 
Last updated: July 1, 2014   impressum