Generating Indexed Formal Software Documents


Ms. Li Wang

Abstract

Precise software documentation can be written as a set of mathematical expressions, but in practice, people require a mixture of informal (English) material and formal mathematical expressions. Furthermore, most documents for real software comprise hundreds of tables. Appropriate indices are required to efficiently search for information. In this work we consider the problem of automatic preparation of indices for such software documents. The user is able to prepare text and diagrams using a system such as LaTeX, while using the TTS system to produce the tables. The TTS system will then produce LaTeX representations of the tables to be inserted in the document using a tool called TLT (Table LaTeX Tool). Finally, the DIT (Document Indexing Tool) will provide a set of indices indicating the table, row, column and page number where each symbol appears.

This work describes the design and development of TLT and DIT for generating indexed software documents. The indices generated by DIT can also be used for efficiently editing tabular expressions, and checking tabular documentation for correctness.