Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
Chapter 18c - Correctness of object-oriented programs. The main contents of this chapter include all of the following: Design by contract, the class invariant, correctness of a queue application, final observations. | Programming Languages 2nd edition Tucker and Noonan Chapter 18 Program Correctness To treat programming scientifically, it must be possible to specify the required properties of programs precisely. Formality is certainly not an end in itself. The importance of formal specifications must ultimately rest in their utility - in whether or not they are used to improve the quality of software or to reduce the cost of producing and maintaining software. J. Horning Contents 18.1 Axiomatic Semantics 18.2 Formal Methods Tools: JML 18.2.1 JML Exception Handling 18.3 Correctness of Object-Oriented Programs 18.3.1 Design by Contract 18.3.2 The Class Invariant 18.3.3 Correctness of a Queue Application 18.3.4 Final Observations 18.4 Correctness of Functional Programs Review JML JML Expression Meaning requires p; p is a precondition for the call ensures p; p is a postcondition for the call signals (E e) p; when exception e is raised by the call, p is a postcondition loop_invariant p; p is a loop invariant invariant p; p is a class invariant \result == e; e is the result returned by the call \old v the value of v at entry to the call (\product int x ; p(x); e(x)) the product of e(x) for all x that satisfy p(x) (\sum int x ; p(x); e(x)) the sum of e(x) for all x that satisfy p(x) p ==> q p q 18.3.1 Design by Contract The contract for a Stack class 18.3.2 The Class Invariant A class C is formally specified if: 1. Every constructor and public method M in the class has preconditions and postconditions, and 2. C has a special predicate called its class invariant INV which, for every object o in C, argument x and call o.M(x), must be true both before and after the call. Note: During a call, INV may temporarily become false. Why are we doing this??? Formal specifications provide a foundation for rigorous OO system design (e.g., “design by contract”). They enable static and dynamic assertion checking of an entire OO system. They enable formal correctness proof of an OO system. 18.3.3 . | Programming Languages 2nd edition Tucker and Noonan Chapter 18 Program Correctness To treat programming scientifically, it must be possible to specify the required properties of programs precisely. Formality is certainly not an end in itself. The importance of formal specifications must ultimately rest in their utility - in whether or not they are used to improve the quality of software or to reduce the cost of producing and maintaining software. J. Horning Contents 18.1 Axiomatic Semantics 18.2 Formal Methods Tools: JML 18.2.1 JML Exception Handling 18.3 Correctness of Object-Oriented Programs 18.3.1 Design by Contract 18.3.2 The Class Invariant 18.3.3 Correctness of a Queue Application 18.3.4 Final Observations 18.4 Correctness of Functional Programs Review JML JML Expression Meaning requires p; p is a precondition for the call ensures p; p is a postcondition for the call signals (E e) p; when exception e is raised by the call, p is a postcondition loop_invariant p; p is a loop .
