Pestana, João Miguel Alves2010-09-132010-09-132009http://hdl.handle.net/10400.13/78This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.engSoftware developmentSoftware correctnessFormal methodsDesign by contractJava Modelling Language (JML)JML-based strategyInformal functional requirementsSemi-formal functional requirementsInvariantsFormal specificationsAbstract variablesJava.Centro de Ciências Exatas e da Engenhariamaster thesis