We present preliminary work on an IDE for formal software development using tabular expressions as the basis for precise specifications and descriptions of software behaviour. 1 Motivation Formal software specification and design techniques, when combined with analysis and verification tools, can significantly increase the confidence that software will behave as required. Such techniques, however, usually require documents to be produced that include fairly complex mathematical expressions, which can often be effectively presented as tabular expressions. Traditional documentation tools have proven to be insufficient for this purpose. We hope to improve this situation by developing tools that support both the production and maintenance of good documentation and the application of this documentation to such tasks as design analysis, verification and testing. Although tabular expressions could be useful in many forms of documentation, our emphasis will be on documents that either ...
Dennis K. Peters, Mark Lawford, Baltasar Tranc&oac