1
Download Hets User Guide
Transcript
Figure 8: Architecture of the heterogeneous tool set. The static analysis is based on the static analysis of basic specifications, and transforms an abstract syntax tree to a development graph (cf. Sect. 7 above). Starting with a node corresponding to the empty theory, it successively extends (using the static analysis of basic specifications) and/or translates (along the intra- and inter-logic translations) the theory, while simultaneously adding nodes and links to the development graph. Heterogeneous proof management is done using heterogeneous development graphs, as described in Sect. 7. For local proof goals, logic-specific provers are invoked, see Sect. 10. HETS can store development graphs, including their proofs. Therefore, HETS uses the so-called ATerm format [8], which is used as interchange format for interfacing with other tools. More details can be found in [20, 26] and in the overview of modules provided in the developers section of the HETS home page at http://www.dfki.de/sks/ hets. HETS is mainly maintained by Christian Maeder ([email protected]) and Till Mossakowski ([email protected]). The mailing list is [email protected] the homepage is 23
