https://futureofcoding.org/ logo
Join Slack
Powered by
This might be premature, but I think I finally und...
# thinking-together
k
This might be premature, but I think I finally understand Dijkstra's approach to deriving programs from post-conditions in "A Discipline of Programming". I've had this book on my bookshelf for almost 20 years, never understood it but also never quite worked up the will to toss it out. (For context, I only own like a dozen books over the long term.) Concretely, I've made it to the end of Chapter 7. I feel like I understand every bit up until this point. Parts of Chapter 6 and 7 feel very sloppily written! And this is Dijkstra! So either my leaps of interpretation are only leaps because I'm missing something, or my sense of understanding is an illusion 😅 Has anyone here made it this far and feel like they understood it? I'd love to talk to you. Incidentally: I wouldn't have made it in even this my probably 4th attempt, if it wasn't for LLMs. They're better than a rubber duck for talking things over with! It's amazing that they can all converse intelligently about the Dijkstra method, and all I need to do is mention 
wp
or 
wdec
. Or I know nothing and am incapable of judging anything about this book.
j
Hi, Kartik, I'd be very interested in having a conversation about Dijkstra's book. I still have my copy that I ordered as soon as I could after it was published. Working through that book (one works it instead of reading it 🙂) profoundly changed my perspective on programming. I find it highly ironic that some people who have been critical of formal methods (or even of Dijkstra's style and content) are also proponents of TDD. I have long thought that both ADoP and TDD emphasize using reasoning about correctness as part of the design process (although I continue to believe that Dijkstra's method is potentially more robust, for a variety of reasons). I'm curious as to what about chapters 6 (designing for termination) and 7 (Euclid's algorithm revisited) left you uncomfortable. I hope we can connect.
❤️ 1
k
Wonderful, thank you! Here's one thing I figured out this time after failing in the past, tell me if I got something wrong: In Chapter 7, when evaluating 
wdec("x := x + y")
under the metric 
t = abs(x-y)
, Dijkstra calculates:
Copy code
tmin(x, y) <= t(x, y) - 1
(I find it helpful to explicitly add the 
(x, y)
to remind myself that 
t
is a function.) This he then simplifies to:
Copy code
x <= abs(x-y) -1
If I understand correctly, the left hand side of the inequality is just the value of 
t
after 
x := x + y
has run.
Copy code
tmin(x, y) = abs(x+y - y) = abs(x)
=> x, since x > 0 by the preconditions of the chapter/problem
This I never understood until now, and I think I've always been thrown off by the "min" in the name "tmin". It seems to me clearer to call it 
t(x', y')
where 
x'
and 
y'
are the values of 
x
and 
y
after 
x := x + y
has run.
Copy code
t(x', y') <= t(x, y) - 1
abs(x+y - y) <= abs(x-y) - 1
etc.
I suppose my two questions are: • Am I on the right track? And, • Does this approach seem clearer to you? I don't really understand the name 
tmin
. Dijkstra introduces it in Chapter 6 as, "the lowest upper bound for the final value of `t`". There's a "min" and a "max" there, and also a "final". If I had to choose a new name, I'd call it 
t_after
or something like that. Perhaps the lack of subscripts affected the choice of name, since "after" starts with a vowel..
I did work through the rest of the chapter and manage to reproduce all his working (with one additional wrinkle that I might complain about next, after we discuss this one), so that gives me some confidence I'm on the right track..
j
tmin
is defined like a supremum (least upper bound). I don't know how Djikstra 1976 constructs that as a postcondition we can reason about, how exciting
k
Yes, indeed. After I posted my original post I ran into that connection. It's unclear to me why it's needed. Each statement is deterministic, the initial state is known. There isn't really a range of values 
t
can have.
j
Sorry to take so long replying. My minor excuse is a very busy work week. My major excuse is that I had to do some re-reading! Some of Dijkstra's writing is very "dense" (in information), so I had to go back and review to get context in my head. A couple of background thoughts come to mind: 1. Repetition in imperative programming seems frequently to be taught (and practiced) either in terms of explicit counting or in terms of iterating over some structure (array elements, linked nodes, file lines, etc.) In such cases, the argument for termination is fairly trivial. The bound on remaining work to be done seems "obvious".
💯 1
❤️ 1
2. In later discussions, Dijkstra went past a priori limits on number of iterations remaining by considering the notion of a "well-founded set" (a set with an ordering such that there are no infinite descending chains). That's a rabbit-trail to the side, but makes interesting context for going back and seeing the state of his thinking in 1976.
With all that said, I interpreted Dijkstra's introduction of tmin as a way to grapple with repetition when the reduction of "work remaining" doesn't happen by simply counting down, and even may be affected differently based on which guarded statement list is activated (when more than one has a true guard). Euclid's GCD algorithm makes a nice lab rat for that kind of thinking (especially when one introduces the remainder-based optimization). It makes an interesting exercise to code GCD based on Dijkstra's thought process and decorate the code with output that shows the changing value of the work-remaining metric as it runs. My recollection of my experience with the book is that of a very zig-zag journey. Sometimes a subsequent chapter or section would cause an "Aha!" that motivating going back to reconsider what I had previously read. I think that the fourth example on page 61 in chapter 8 can play that role relative to chapter 6 (especially after slogging through the detailed discussion of the third example!) And Dijkstra's note at the end of that fourth example illustrates that he sometimes throws in passing comments that actually require very deep thought on the distinction between correctness and performance!
💡 1
I hadn’t thought about your before-and-after interpretation in quite that way. I’ll have to ponder a bit. Regarding your reference to determinism, only some constructions in EWD’s wp-based notation are deterministic! While some cases (e.g. 
x := x-y
) are, EWD’s reasoning makes some kinds of determinism a not-very-interesting special case. The “Aha!” moment for me was his solution for 
max
in 
c := a max b
.
Copy code
if
   a >= b -> c := a
[]
   b >= a -> c :- b
fi
In the (again, uninteresting) special case that 
a = b
, both guards are true it is perfectly valid to “perform” either of the two guarded commands.
k
Yeah, after my original commented it occurred to me that Dijkstra is building a framework that includes even compound statements, even if the initial examples consider only simple ones. Supremum probably makes more sense if S is a loop. I'll keep going until I find examples like that. The key insight for me is that tmin is only in the context of a single iteration. It's not saying anything about the entire execution of the (containing) loop.
j
I have been reminded (more than once) of the compare-and-contrast possibilities of Dijkstra’s 1970s vision vs. general practice 50-ish years later. For example: • Both Dijklstra’s presentation of the wp-calculus and contemporary TDD rest on the idea of thinking first about verification and then letting those considerations guide the design. Property-based testing goes a large step further than simple unit testing. But we still haven’t gotten to the full-coverage rigor of EWD.
• The clean way that the if/fi and do/od constructs embraced non-determinism still looks cleaner to me than the contemporary toolkits of various mainstream languages and frameworks.
💯 1
k
I'm still trying to figure out how to do it for larger examples. My go to example is a text wrapping function I've endlessly stared at in the last 2 years. Maybe I'll figure out its invariants and preconditions by the time I'm done with the book.
🎯 1
j
I have found that human-perception-based problems are the hardest for me to describe precisely. (For example, creating a “nice” layout of a binary tree…) Assuming that you think of “text wrapping” the same way I do--breaking text on runs of whitespace into a list of tokens (maximal runs of non-whitespace characters), then “flowing” them into multiple lines such that the tokens appear in the same order, tokens in each line are separated by whitespace, each input token is contained in the output, no output line is more than a specified length limit… The basic properties seem feasible, but then the “what about”s start: What about forced breaks? What about justification? …
💯 2
4 Views
Open in Slack
PreviousNext
Powered by