From English to formal specifications

Specifications provide the foundation upon which a system can be formally developed. If a specification is wrong, then no matter what method of design is used, or what quality assurance procedures are in place, they willnot result in a system that meets the requirements.The specification of a system involves people of different profiles who favour different representations. At the beginning natural language is used because the specification document acts as a contract between the user and the developers. Most of the time, the only representation that users understand and agree on is natural language. At the other end, developers findnatural language specifications ambiguous and incomplete and may therefore prefer formal specifications. The transition from informal specifications to formal ones is an error prone and time consuming process. This transitionmust be supported to ensure that the formal specifications are consistent with the informal ones.In this research we propose an interactive approach for producing formal specifications from English specifications. The approach uses research in the area of natural language understanding to analyse English specifications in order to detect ambiguities. The method used for analysing natural language text is based on McCord’s approach. This method consists oftranslating natural language sentences into a logical form language representation.This helps to identify ambiguities present in natural language specifications and to identify the entities and relationships. These entities and relationships are used as a basis for producing VDM data types.We also investigate the production of data type invariants for restricted sentences and the production of some common specifications.We test our approach by implementing it in Prolog-2 and apply it to an independent case study