Formal methods are mathematically based languages, tools and techniques for the specification, development and verification of systems [12]. Although most effort is being spent on specifying systems and verifying their properties, a final goal of most formal methods is achieving correct code from formal specifications. In this direction we find two representative strategies: (ⅰ) one is based on proposing refinements until a certain concrete design is achieved and then an almost direct mapping from mathematical elements to the source code of some programming language is made [17]; and (ⅱ) another is using some refinement calculus in which specification and programming constructs are available in a single language and code is achieved by removing the specification elements by applying specific refinement rules [9]. Both strategies depend on developers experience.
展开▼
