GF for Informal and Formal Requirements Specifications

This is the home page of a tool that supports authoring of informal and formal software requirements specifications simultaneously and from a single source. The tool is an attempt to bridge the gap between completely informal requirements specifications (as found in practice) and formal ones (as needed in formal methods). The user is supported by an interactive syntax-directed editor, parsers and linearizers. As a formal specification language we realize the Object Constraint Language, a substandard of the UML, on the informal side a fragment of English.

The implementation is based on the Grammatical Framework, a generic tool that combines linguistic and logical methods. It is being integrated into the KeY project.

Documentation

• The foundations and design principles of the tool are described in the paper An Authoring Tool for Informal and Formal Requirements Specifications by Reiner Hähnle, Kristofer Johannisson and Aarne Ranta (published in LNCS 2306).
• Hans-Joachim Daniel's Study thesis Eine deutsche Grammatik für OCL (note: thesis written in English) describes the work of adding a German grammar to the system, as well as updating all grammars for utilizing the GF 2.0 module system.
• The Master's thesis Improving the natural language translation of formal software specifications by David Burke describes the result of improving and extending the system to handle a larger case study.

Current Status

There are currently two prototype versions of the tool:

1. A version which is integrated into the KeY system. This version is focused on syntax editing. To try it out, you need the following:
   • The KeY tool and its accompanying tutorial. KeY download page, with download and installation instructions.
   • Three external programs, as described here.
2. A command-line application for batch translation from OCL to English text. As described in David Burke's Master's thesis, it has been used for translating OCL specifications of the JavaCard API into English. A source distribution is available here.

Feedback to krijo@cs.chalmers.se. Last modified 2005-04-07.