From English to Formal Specifications

TLDR

Formal methods enable design steps to be proven correct, yet when specifications are written in English and later translated into formal form, inaccuracies can arise, potentially undermining system requirements. Translating English requirements into formal specifications can introduce errors and inconsistencies.

Abstract

Formal methods provide an approach in which design steps can be shown to satisfy a specification. However, if a formal specification is wrong, then although the design steps may satisfy the formal specification, they are unlikely to satisfy the requirements of the system. Since most users are unfamiliar with formal methods, requirements specifications are often written in English. Such requirements, expressed in English, are then somehow translated to formal specifications. This transition has some potential for introducing errors and inconsistencies.