Abstract
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 is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
K. Beck. Extreme Programming Explained: Embrace Change. Addison-Wesley, Pearson Education, 2000. ISBN 201-61641-6.
H. Ehrig, F. Orejas, and J. Padberg. Relevance, intergration and classification of specification formalism and formal specification techniques. In Proc. FORMS, Formale Techniken für die Eisenbahnsicherung, Fortschritt-Berichte VDI, Reihe 12,Nr. 436, VDI Verlag, 2000, pages 31–54, 1999.
M. Fowler, K. Beck, J. Brant, and W. Opdyke. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 1999.
E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns-Elements of Reusable Object Oriented Software. Addison-Wesley, 1995.
A. Herranz, J. Moreno, and N. Maya. Declarative reflection and its application as a pattern language. In M. Comini and M. Falaschi, editors, 11th. InternationalWorkshop on Functional and Logic Programming (WFLP’02), Grado, Italy, June 2002. University of Udine.
A. Herranz and J. J. Moreno. Generation of and debugging with logical pre and post conditions. In M. Ducasse, editor, Workshop onAutomated and Algorithmic Debugging 2000.TUMunich, 2000.
A. Herranz and J. J. Moreno. On the design of an object-oriented formal notation. In Fourth Workshop on Rigorous Object Oriented Methods, ROOM 4. King’s College, London, March 2002.
C. B. Jones. Systematic Software Development Using VDM. Prentice Hall, 1986.
The SLAM website. http://lml.ls.fi.upm.es/slam.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.
J. B. Wordsworth. Software Development with Z. Addison-Wesley, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herranz, Á., Moreno-Navarro, J.J. (2003). Formal Extreme (and Extremely Formal) Programming. In: Marchesi, M., Succi, G. (eds) Extreme Programming and Agile Processes in Software Engineering. XP 2003. Lecture Notes in Computer Science, vol 2675. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44870-5_12
Download citation
DOI: https://doi.org/10.1007/3-540-44870-5_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40215-2
Online ISBN: 978-3-540-44870-9
eBook Packages: Springer Book Archive