When defining the correctness of a program, it is helpful to do it in steps. First, consider the invariant of the program and a fixed point. If the program reaches the fixed point, it terminates. If the program terminates, then we know both the conditions are satisfied - the invariant and the termination.
The second step of the program is to establish that the program indeed terminates. This step involves finding a metric. A metric should be guaranteed to change eventually otherwise the program does not progress. Further a metric should be non-decreasing and bounded below or non-increasing and bounded above for it to indicate that the fixed point has been reached.
Skilled programmers can easily correlate this to the recursive functions. The termination condition for the recursion is specified first so that the function can terminate. The metric is the condition on which the recursion continues. The condition is enforcing that there is a convergence to the fixed point.
Take the example of the Earliest meeting time. This problem consists of finding the first time at which three people are all simultaneously available. The three people are named A, B and C. With each person, we associate a function f, g and h respectively. These functions represent the earliest time each is available. For example, f.t is the earliest time at or after time t at which A is available.
f.t = t => A being available at time t.
The earliest that all three can meet is represented by M which is the minimum time at which all the f.t = g.t = h.t
To calculate this M, we define a metric r that denotes time. We try different values of time. We initialize it to zero. We assign r to f.r or g.r or h.r
The goal is to get to a fixed point which we define as
r = f.r = h.r = g.r
This fixed point implies that r >= MThe r is guaranteed not to decrease because f.t > t.
The invariant we define as r <= M
Therefore at termination r = M
The steps above are in the order in which we stated earlier to discuss the correctness of the program. It follows the metric. We already noted the fixed point and the invariant. We guarantee that r will change if r is below M because we consider the case where r is < M. In this case, one of the persons is not available otherwise all would be available and this would be M (proof by contradiction) Therefore f.r > r so the action r = f.r increases the metric.
Since r increases and r reaches M, we know that the program terminates.
The second step of the program is to establish that the program indeed terminates. This step involves finding a metric. A metric should be guaranteed to change eventually otherwise the program does not progress. Further a metric should be non-decreasing and bounded below or non-increasing and bounded above for it to indicate that the fixed point has been reached.
Skilled programmers can easily correlate this to the recursive functions. The termination condition for the recursion is specified first so that the function can terminate. The metric is the condition on which the recursion continues. The condition is enforcing that there is a convergence to the fixed point.
Take the example of the Earliest meeting time. This problem consists of finding the first time at which three people are all simultaneously available. The three people are named A, B and C. With each person, we associate a function f, g and h respectively. These functions represent the earliest time each is available. For example, f.t is the earliest time at or after time t at which A is available.
f.t = t => A being available at time t.
The earliest that all three can meet is represented by M which is the minimum time at which all the f.t = g.t = h.t
To calculate this M, we define a metric r that denotes time. We try different values of time. We initialize it to zero. We assign r to f.r or g.r or h.r
The goal is to get to a fixed point which we define as
r = f.r = h.r = g.r
This fixed point implies that r >= MThe r is guaranteed not to decrease because f.t > t.
The invariant we define as r <= M
Therefore at termination r = M
The steps above are in the order in which we stated earlier to discuss the correctness of the program. It follows the metric. We already noted the fixed point and the invariant. We guarantee that r will change if r is below M because we consider the case where r is < M. In this case, one of the persons is not available otherwise all would be available and this would be M (proof by contradiction) Therefore f.r > r so the action r = f.r increases the metric.
Since r increases and r reaches M, we know that the program terminates.
No comments:
Post a Comment