Formal SpecificationSpecification in the Software ProcessSpecification and DesignFormal Specification on TrialWhy Aren’t Formal Methods Used?Slide 6Advantages of Formal SpecificationSlide 8Seven Myths of Formal MethodsSlide 10The Verdict!Use of Formal MethodsDevelopment Costs with Formal SpecificationSpecifying Functional AbstractionsSpecification with Pre and Post ConditionsSpecification DevelopmentThe Specification of a SearchFormal Specification ApproachesFormal Specification LanguagesSet Theory ReviewImplicationPre/Post Condition ExamplesSlide 23Pre/Post Condition Examples(2)Slide 25Pre/Post Condition Examples(3)Slide 27Pre/Post Condition Examples(4)Slide 29Pre/Post Conditions with JavaSlide 31Stack Implementation in JavaPre/Post Conditions for C functions strlen()Pre/Post Conditions for C functions strchr() solutionSlide 35Pre/Post Conditions for C functions strcmp()Slide 37Model-based SpecificationSlide 39Z as a Specification LanguageZ SchemasZ Schema HighlightingAn Indicator SpecificationStorage Tank SpecificationFull Specification of a Storage TankZ ConventionsSlide 47Operation SpecificationA Partial Specification of a Fill OperationStorage Tank Fill OperationThe Z Specification ProcessData Dictionary SpecificationGiven SetsType DefinitionsSpecification Using FunctionsThe Function SmallSquareData Dictionary ModelingData Dictionary EntryData Dictionary as a FunctionData Dictionary - Initial StateAdd and Lookup OperationsSlide 62Function Overriding OperatorReplace OperationDeleting an EntryDelete EntrySpecifying Ordered CollectionsA Z SequenceData Dictionary Extract OperationThe Extract OperationExtract PredicateSlide 72Z ExamplesZ Examples (2)Z Examples (3)Z Examples (4)Symbol Sheet©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 1Formal SpecificationTechniques for the unambiguous specification of software©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 2Specification in the Software ProcessSpecification and design are intermingled.Architectural design is essential to structure a specification.Formal specifications are expressed in a mathematical notation with precisely defined vocabulary, syntax and semantics.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 3Specification and DesignArchitecturaldesignRequir ementsspecificationRequir ementsdefinitionSoftwarespecificationHigh-leveldesignIncreasing contractor involvementDecreasin g client involvementSpecificationDesign©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 4Formal Specification on TrialFormal techniques are not widely used in industrial software development.Given the relevance of mathematics in other engineering disciplines, why is this the case?©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 5Why Aren’t Formal Methods Used?Inherent management conservatism. It is hard to demonstrate the advantages of formal specification in an objective way.Many software engineers lack the training in discrete math necessary for formal specification.System customers may be unwilling to fund specification activities.Some classes of software (particularly interactive systems and concurrent systems) are difficult to specify using current techniques.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 6Why Aren’t Formal Methods Used?There is widespread ignorance of the applicability of formal specifications.There is little tool support available for formal notations.Some computer scientists who are familiar with formal methods lack knowledge of the real-world problems to which these may be applied and therefore oversell the technique.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 7Advantages of Formal SpecificationIt provides insights into the software requirements and the design. Formal specifications may be analyzed mathematically for consistency. It may be possible to prove that the implementation satisfies the specification.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 8Advantages of Formal SpecificationFormal specifications may be used to guide the tester of the component in identifying appropriate test cases.Formal specifications may be processed using software tools. It may be possible to animate the specification to provide a software prototype.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 9Seven Myths of Formal MethodsPerfect software results from formal methods–Nonsense - the formal specification is a model of the real-world and may incorporate misunderstandings, errors and omissions.Formal methods means program proving–Formally specifying a system is valuable without formal program verification as it forces a detailed analysis early in the development process.Formal methods can only be justified for safety-critical systems.–Industrial experience suggests that the development costs for all classes of system are reduced by using formal specification.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 10Seven Myths of Formal MethodsFormal methods are for mathematicians–Nonsense - only simple math is needed.Formal methods increase development costs–Not proven. However, formal methods definitely push development costs towards the front-end of the life cycle.Clients cannot understand formal specifications–They can if they are paraphrased in natural language.Formal methods have only been used for trivial systems–There are now many published examples of experience with formal methods for non-trivial software systems.©Ian Sommerville 1995/2000