After studying this chapter you will be able to understand: What is a formal specification, logical theories as specifications, the schema notation, moving towards object-Z language, what is a program specification,. | Formal Methods Qaisar Javaid Assistant Professor Aims and Objectives It aims to illustrate: Basic approaches to formal specification. .: “state-based” and “class-based” approaches This part of the course is about formal specifications and their role in (formal) development of software systems. Derivations of formal specifications from informal requirements. Refinement of formal specifications into program structures and specification of programs. Basic techniques for reasoning about programs and their correctness with respect to the specifications. . product meets its requirements This course focuses on formal development of software systems. By formal development we mean development processes that make use of formal techniques for defining system requirements, specifying programs and reason about the correctness of programs with respect to given formal requirements. We will therefore look at different types of formal specifications, chosen according to the development stage under consideration and/or the type of development approach adopted (. “state based” or “object” based approaches). We will also see how some of these different types of formal specifications can be related with each other. The aims are: Illustrate the role of formal specifications within the development process of computer systems, in terms of helping understand what the system is supposed to achieve and why. Show the basic principles and logical ideas underlying state-based formal specifications. Conventional logic will be used, adopting some of the most common features of Z specification language. Extend the principles of state-based specifications to class-based formal specifications. Show how some standard object-oriented features (., inheritance and polymorphism) can be captured in class-based formal specifications. A specific language, called Object-Z, will be used, which builds upon notations introduced in the state-based specifications. Show how class-based . | Formal Methods Qaisar Javaid Assistant Professor Aims and Objectives It aims to illustrate: Basic approaches to formal specification. .: “state-based” and “class-based” approaches This part of the course is about formal specifications and their role in (formal) development of software systems. Derivations of formal specifications from informal requirements. Refinement of formal specifications into program structures and specification of programs. Basic techniques for reasoning about programs and their correctness with respect to the specifications. . product meets its requirements This course focuses on formal development of software systems. By formal development we mean development processes that make use of formal techniques for defining system requirements, specifying programs and reason about the correctness of programs with respect to given formal requirements. We will therefore look at different types of formal specifications, chosen according to the .
