JFly: A JML-Based Strategy for Incorporating Formal Specifications into the Software Development Process

Abstract. This paper presents JFly, a JML-based strategy for incor-porating formal specifications into the software development of object oriented programs. The strategy consists in evolving functional require-ments into a semi-formal requirements form, and then expressing these requirements as JML formal specifications. What makes our strategy different from existing strategies is the particular use of JML we make all along the way from requirements to validation-and-verification. We validate our strategy with the formal development of a smart card ap-plication for managing medical information.