Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
Chapter 18d - Correctness of functional programs. This section addresses the question of program correctness functional programming. We visit the question of how to prove a program conect for the special case when it is written in a pure functional program-one that is state-less and relies instead on functional composition and recursion as a foundation for its semantics. | 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.3 Correctness of Object-Oriented Programs 18.4 Correctness of Functional Programs 18.4.1 Recursion and Induction 18.4.2 Examples of Structural Induction 18.4 Correctness of Functional Programs Pure functional programs are more accessible to correctness proofs than imperative or OO programs. Three major reasons: Pure functional programs are state-free (no assignment), Functions and variables mathematical ideas, and Recursion aligns well with proof by induction. 18.4.1 Recursion and Induction Consider the Haskell function: > fact n > | n == 1 = 1 -- fact.1 > | n > 1 = n*fact(n-1) -- fact.2 Suppose we want to prove that this function correctly computes the factorial. I.e., that it computes: fact(1) = 1 fact(n) = 1 2 (n-1) n when n>1 Induction proof of a recursive function The induction proof is straightforward. We use the definition of the function directly in the proof. Basis step: The function computes the correct result for n = 1, using line fact.1 of the definition. Induction step: Assume the hypothesis that the function computes the correct result for some n = k > 1. That is, it computes fact(k) = 1 2 (k-1) k. Then for n = k+1, it computes fact(k+1) = (k+1)*fact(k) using line fact.2 of the definition. Thus, it computes fact(k+1) = 1 2 (k-1) k (k+1), which completes the induction step. 18.4.2 Examples of Structural Induction List concatenation and reversal: > cat [] ys = ys -- cat.1 > cat (x:xs) ys = x : (cat xs ys) -- cat.2 > rev [] = [] | 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.3 Correctness of Object-Oriented Programs 18.4 Correctness of Functional Programs 18.4.1 Recursion and Induction 18.4.2 Examples of Structural Induction 18.4 Correctness of Functional Programs Pure functional programs are more accessible to correctness proofs than imperative or OO programs. Three major reasons: Pure functional programs are state-free (no assignment), Functions and variables mathematical ideas, and Recursion aligns well with proof by induction. .
