Agile Processes and Formal Methods (FM), water and oil, impossible mixture? Yes at first sight. Nevertheless, being formal methods weight processes and being agile processes informal approaches to software development, it is worth to study how much formal can be an agile process like Extreme Programming (XP) and how much agile can be a formal method. On our view, some XP practices are suitable for a formal approach.
In this paper the authors study a pair of constructs in a formal specification language that can be directly translated into readable and relatively efficient code. Those constructs are algebraic types and (an extended concept of logical) quantification. The translation is guided by object oriented design patterns that makes the synthesised code easily understandable by ordinary developers. Efficiency can be achieved thanks to the effort of the user during the specification refinement process, specification transformations and implementation issues of the the design patterns.
The paper shows the outlines of the SLAM system, that allows for an effective use of Formal Methods (FM) in Rapid Application Development (RAD) and other prototyping processes. The SLAM system, includes an expressive object oriented specification language and a development environment that, among other features, is able to generate efficient and readable code in a high level object oriented language (Java, C++, ...). SLAM is able to generate prototypes that can be used to validate the requirements with the user. The additional advantage is that the prototype is not throw-away because most part of the generated code can be directly used and the other part can be optimised with the additional help of assertions automatically included.
This paper is an exploratory work were the authors study how the technology of Formal Methods (FM) can interact with agile process in general and with Extreme Programming (XP) in particular. Our thesis is that most of XP practices (pair programming, daily build, the simplest design or the metaphor) are technology independent and therefore can be used in FM based developments. Additionally, other essential pieces like test first, incremental development and refactoring can be improved by using FM. In the paper we explore in a certain detail those pieces: when you write a formal specification you are saying what your code must do, when you write a test you are doing the same so the idea is to use formal specifications as tests. Incremental development is quite similar to the refinement process in FM: specifications evolve to code maintaining previous functionality. Finally FM can help to remove redundancy, eliminate unused functionality and transform obsolete designs into new ones, and this is refactoring.
This file was generated by bibtex2html 1.98.