Here, we look at program correctness.
A program can be viewed as a contract binding a precondition to a postcondition; let Pre(X) be the predicate denoting the precondition, where X is the input of the program, and Post(X) be the predicate denoting the postcondition. Then a program is correct if: on all X, such that X satisfies Pre(X), Post(X) holds after the program terminates.
In the context of iterative algorithms, this leads to the notion of a loop invariant with respect to these predicates. Hence, to prove total correctness of an iterative algorithm, we need to prove termination and partial correctness (the loop invariant holds). Both of these are proved inductively, separately.
To prove the correctness of recursive algorithms, we define a predicate expliciting its total correctness (that is that it terminates on valid input and that Pre(X) => Post(X) when it does). We then prove this predicate inductively, hence both termination and partial correctness are proved jointly.
It should be noted that termination analysis is not always possible because of the undecidability of the Halting Problem (given an arbitrary program, prove that it halts or not). The fact that there are such undecidable problems demonstrates a 'hole' in everything our field (CS) hopes to be able to compute, an incompleteness very much related to Godel's theorems.
A program can be viewed as a contract binding a precondition to a postcondition; let Pre(X) be the predicate denoting the precondition, where X is the input of the program, and Post(X) be the predicate denoting the postcondition. Then a program is correct if: on all X, such that X satisfies Pre(X), Post(X) holds after the program terminates.
In the context of iterative algorithms, this leads to the notion of a loop invariant with respect to these predicates. Hence, to prove total correctness of an iterative algorithm, we need to prove termination and partial correctness (the loop invariant holds). Both of these are proved inductively, separately.
To prove the correctness of recursive algorithms, we define a predicate expliciting its total correctness (that is that it terminates on valid input and that Pre(X) => Post(X) when it does). We then prove this predicate inductively, hence both termination and partial correctness are proved jointly.
It should be noted that termination analysis is not always possible because of the undecidability of the Halting Problem (given an arbitrary program, prove that it halts or not). The fact that there are such undecidable problems demonstrates a 'hole' in everything our field (CS) hopes to be able to compute, an incompleteness very much related to Godel's theorems.
No comments:
Post a Comment