PDA 4.5.3 (courtesy Eric Macaulay)
7 views
Skip to first unread message
Jeremy Weissmann
Nov 28, 2007, 1:21:22 PM11/28/07
to Calculationa...@googlegroups.com
Hey all.
A few weeks ago, Eric Macaulay submitted a note on a programming problem for public review on a different board. I thought I would attach the note here, and post comments, for a slightly larger audience.
------
PAGE 1
------
* You begin your solution with the phrase "We begin by tackling an easier problem..." , which I find to be an understatement. You are in fact separating the concerns of computing a certain value, and computing an index for said value. There is a well-established pattern for computing indices: first design a program to compute the value, then augment that program by introducing auxiliary variables to stand for the indices. So you are not just tackling "an easier problem" , but an important subproblem of the problem you are trying to solve!
* In the first program, the first assertion in the loop has conjunct n ≠ 0 , but I think you meant n ≠ N .
* A slight typographical note, but it would be nice to have your 'semi' (;) sticking out to the left a little. (If you are typing this in Plain TeX , I can show you how to do this.)
* I like the 'query' convention, borrowed from Feijen and van Gasteren's On A Method Of Multiprogramming . However, you should be aware that your use of it is not entirely correct. In that book, an assertion is queried when its partial correctness has yet to be proven. Part of your program reads:
"Establish r = F.(n+1) "
{ ? r = F.(n+1) , Note 0 } .
The problem is, the way you have written it, the assertion does not need a query, because it is preceded by a statement which, by assumption, establishes it! What you do in Note 0 is rather to refine "Establish..." , to show that it terminates, to aid in its implementation, etc. I'm not sure if there's a better notation to use, but it's worth pointing out.
* The First Termination Lemma is not correct. You may verify that the following program fits your program scheme, but does not terminate:
n := 0 ; do n ≠ 1 -> n := n+2 od .
In order to make your Lemma correct, you should add that the loop maintains n ≤ N as invariant. In that case the initial assignment to n is overspecific. You could just write: For increasing f , the following program terminates:
{ inv: n ≤ N } do n ≠ N -> ... ; n := f.n od ,
where "..." does not contain assignments to n . (Notice I omitted the word 'clearly' .) I might also add that there is a similar Termination Lemma for decreasing f .
* At the bottom of the page, there is a huge amount of space around the equals sign. (This is one of the few typographically ugly things in your note.)
------
PAGE 2
------
* At the top of Page 2 , you laconically begin: "We observe" . This is too terse for my liking. What are you observing? What are you calculating? Why? You can answer these questions with a single sentence, which would help direct and orient your readers. Remember, every calculation occurs in a context, so you need to either give the context explicitly, or let your readers know what you are doing, so they know where your assumptions come from.
* The spacing on the second line of the calculation could be improved; you might want to put some space around the binary ↑ .
* Your program fragment has the semi in the wrong place. It should precede "Establish..." .
* First of all, I think this program fragment should be preceded by { s = G.n } , for clarity. Second of all, why is "Establish s = G.(n+1) " part of the refinement of "Establish r = F.(n+1) " ? The former really has nothing to do with the latter. It is a separate concern, and I think it should be dealt with separately.
------
PAGE 3
------
* Again, for this Sidebar Calculation , please introduce the calculation. Remind the reader what you are calculating and why.
* The range of quantification 0 ≤ p < n remains the same for the entire calculation, so put this in the context. (I think this should always be done, where possible. But certainly it should be done when your calculation is long, wide, and involved, like this one is.)
* I am surprised you don't exploit the fact that absolute value (or 'positive value' , the concept you so nicely introduce) distributes over * . This would lead to a simpler calculation, and overall program!! In this calculation I use a postfixed ⁺ to denote absolute (positive) value:
〈max p :: (A.p * A.n)⁺ 〉
= { ⁺ over * }
〈max p :: (A.p)⁺ * (A.n)⁺ 〉
= { property of max }
〈max p :: (A.p)⁺ 〉 * (A.n)⁺
= { introducing G }
G.n * (A.n)⁺ .
This avoids a case distinction.
------
PAGE 4
------
* If you used the above calculation, the selection statement on Page 4 would become simply:
r := r ↑ s*(A.n)⁺ .
* After the program on this page, you say "Next we strengthen..." . This is too sudden! I feel you owe it to the reader to announce that you have completed the design of a program to compute the value you were looking for. Then announce that you are going to introduce some new variables to track the indices, and strengthen the invariant accordingly. Even better, tell the reader which variables will track which indices.
* In handling the initialization, there is a mysterious 2 which appears. The reader is supposed to figure out that you have changed the initialization of n to n := 2 . If this happens for a reason, then tell the reader that reason! Is it possible that you could still initialize with n := 0 ? For that to happen, you'd need to introduce "thought values" for A , namely A.(-2) and A.(-1) . These would have to act as a sort of "minus infinity" . If we call that value BOT , then I believe BOT should satisfy:
A.(-2) = BOT = A.(-1)
BOT * BOT = BOT
BOT⁺ = BOT
BOT ↑ x = x .
If that's really the case (you should check my work), then that's not too unobjectionable, and you might want to consider that approach.
------
PAGE 5
------
* The first calculation on this page is a bit convoluted. For four steps, you just manipulate the righthand side of the equality. So you should pull that out as a separate (narrow) calculation, then use the result in the main (wide) calculation. Perhaps you could do something like this:
s * (A.n)⁺
= { introducing i }
(A.i)⁺ * (A.n)⁺
= { ⁺ over * }
(A.i * A.n)⁺
= { assuming i = x and n = y }
(A.x * A.y)⁺ .
It turns out that you don't even need a wide calculation!
* Obviously your code will be simplified here, since you won't have a selection statement to deal with.
-------------
This is a note of good quality, but you should take the opportunity to make some of the improvements I've outlined above, both in terms of the mathematics, and in terms of the exposition. Make it perfect!
+j
A few weeks ago, Eric Macaulay submitted a note on a programming problem for public review on a different board. I thought I would attach the note here, and post comments, for a slightly larger audience.
------
PAGE 1
------
* You begin your solution with the phrase "We begin by tackling an easier problem..." , which I find to be an understatement. You are in fact separating the concerns of computing a certain value, and computing an index for said value. There is a well-established pattern for computing indices: first design a program to compute the value, then augment that program by introducing auxiliary variables to stand for the indices. So you are not just tackling "an easier problem" , but an important subproblem of the problem you are trying to solve!
* In the first program, the first assertion in the loop has conjunct n ≠ 0 , but I think you meant n ≠ N .
* A slight typographical note, but it would be nice to have your 'semi' (;) sticking out to the left a little. (If you are typing this in Plain TeX , I can show you how to do this.)
* I like the 'query' convention, borrowed from Feijen and van Gasteren's On A Method Of Multiprogramming . However, you should be aware that your use of it is not entirely correct. In that book, an assertion is queried when its partial correctness has yet to be proven. Part of your program reads:
"Establish r = F.(n+1) "
{ ? r = F.(n+1) , Note 0 } .
The problem is, the way you have written it, the assertion does not need a query, because it is preceded by a statement which, by assumption, establishes it! What you do in Note 0 is rather to refine "Establish..." , to show that it terminates, to aid in its implementation, etc. I'm not sure if there's a better notation to use, but it's worth pointing out.
* The First Termination Lemma is not correct. You may verify that the following program fits your program scheme, but does not terminate:
n := 0 ; do n ≠ 1 -> n := n+2 od .
In order to make your Lemma correct, you should add that the loop maintains n ≤ N as invariant. In that case the initial assignment to n is overspecific. You could just write: For increasing f , the following program terminates:
{ inv: n ≤ N } do n ≠ N -> ... ; n := f.n od ,
where "..." does not contain assignments to n . (Notice I omitted the word 'clearly' .) I might also add that there is a similar Termination Lemma for decreasing f .
* At the bottom of the page, there is a huge amount of space around the equals sign. (This is one of the few typographically ugly things in your note.)
------
PAGE 2
------
* At the top of Page 2 , you laconically begin: "We observe" . This is too terse for my liking. What are you observing? What are you calculating? Why? You can answer these questions with a single sentence, which would help direct and orient your readers. Remember, every calculation occurs in a context, so you need to either give the context explicitly, or let your readers know what you are doing, so they know where your assumptions come from.
* The spacing on the second line of the calculation could be improved; you might want to put some space around the binary ↑ .
* Your program fragment has the semi in the wrong place. It should precede "Establish..." .
* First of all, I think this program fragment should be preceded by { s = G.n } , for clarity. Second of all, why is "Establish s = G.(n+1) " part of the refinement of "Establish r = F.(n+1) " ? The former really has nothing to do with the latter. It is a separate concern, and I think it should be dealt with separately.
------
PAGE 3
------
* Again, for this Sidebar Calculation , please introduce the calculation. Remind the reader what you are calculating and why.
* The range of quantification 0 ≤ p < n remains the same for the entire calculation, so put this in the context. (I think this should always be done, where possible. But certainly it should be done when your calculation is long, wide, and involved, like this one is.)
* I am surprised you don't exploit the fact that absolute value (or 'positive value' , the concept you so nicely introduce) distributes over * . This would lead to a simpler calculation, and overall program!! In this calculation I use a postfixed ⁺ to denote absolute (positive) value:
〈max p :: (A.p * A.n)⁺ 〉
= { ⁺ over * }
〈max p :: (A.p)⁺ * (A.n)⁺ 〉
= { property of max }
〈max p :: (A.p)⁺ 〉 * (A.n)⁺
= { introducing G }
G.n * (A.n)⁺ .
This avoids a case distinction.
------
PAGE 4
------
* If you used the above calculation, the selection statement on Page 4 would become simply:
r := r ↑ s*(A.n)⁺ .
* After the program on this page, you say "Next we strengthen..." . This is too sudden! I feel you owe it to the reader to announce that you have completed the design of a program to compute the value you were looking for. Then announce that you are going to introduce some new variables to track the indices, and strengthen the invariant accordingly. Even better, tell the reader which variables will track which indices.
* In handling the initialization, there is a mysterious 2 which appears. The reader is supposed to figure out that you have changed the initialization of n to n := 2 . If this happens for a reason, then tell the reader that reason! Is it possible that you could still initialize with n := 0 ? For that to happen, you'd need to introduce "thought values" for A , namely A.(-2) and A.(-1) . These would have to act as a sort of "minus infinity" . If we call that value BOT , then I believe BOT should satisfy:
A.(-2) = BOT = A.(-1)
BOT * BOT = BOT
BOT⁺ = BOT
BOT ↑ x = x .
If that's really the case (you should check my work), then that's not too unobjectionable, and you might want to consider that approach.
------
PAGE 5
------
* The first calculation on this page is a bit convoluted. For four steps, you just manipulate the righthand side of the equality. So you should pull that out as a separate (narrow) calculation, then use the result in the main (wide) calculation. Perhaps you could do something like this:
s * (A.n)⁺
= { introducing i }
(A.i)⁺ * (A.n)⁺
= { ⁺ over * }
(A.i * A.n)⁺
= { assuming i = x and n = y }
(A.x * A.y)⁺ .
It turns out that you don't even need a wide calculation!
* Obviously your code will be simplified here, since you won't have a selection statement to deal with.
-------------
This is a note of good quality, but you should take the opportunity to make some of the improvements I've outlined above, both in terms of the mathematics, and in terms of the exposition. Make it perfect!
+j
Reply all
Reply to author
Forward
0 new messages