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 and a fragment of German.
OCLNL is integrated into the KeY system. The implementation is based on the Grammatical Framework, a generic tool that combines linguistic and logical methods.
There are currently two prototype versions of the tool:
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 on the OCLNL download page.
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.
Get OCLNL binaries and sources from the OCLNL download page.
An informal introduction to the OCLNL tool in the context of the KeY system is given in the chapter “Natural Language Specifications” of the forthcoming KeY book. A preliminary version of this chapter is available as a part of the PhD thesis of Kristofer Johannisson.
The troubleshooting page lists some common problems when using KeY with OCLNL.
There is also some technical documentation on OCLNL, e.g. information on the implementation of OCLNL as well as how to make use of the command line tools.
For more information, a number of theses and papers related to OCLNL are available:
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, preprint pdf ).
Hans-Joachim Daniels’ 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.
The Master’s thesis of Burke is also the basis of the paper “Translating Formal Software Specifications to Natural Language / A Grammar-Based Approach” (preprint pdf) by D. A. Burke and K. Johannisson. In Logical Aspects of Computational Linguistics (LACL 2005), ed. by P. Blace, E. Stabler, J. Busquets and R. Moot, Springer LNAI 3402, pp. 51-66, 2005. .
The Master’s thesis “Multilingual Syntax Editing for Software Specifications” of Hans-Joachim Daniels describes the work of adapting the generic GF syntax editor to the editing of OCL and natural language in the context of KeY.
The PhD thesis “Formal and informal software specifications” of Kristofer Johannisson contains some of the papers mentioned above in addition to other material related to OCLNL.
The following people have been involved in work related to OCLNL:
Last update: 2006-08-17 by Kristofer Johannisson