結構化編程

請問如何論證：如果 0 ≤ r < dd 成立，經過這兩行程式後，0 ≤ r < dd 仍成立？

dd := dd / 2;
if dd ≤ r then r := r - dd

這個例子來自 Dahl, Dijkstra & Hoare 1972 年的 Structured Programming. 書名引起我的注意：「結構化程式設計」在 70, 80 年代曾被學界、業界視為軟體危機的解方、所有人寫程式該遵守的圭臬。但每個陣營對它是什麼都各有一套解釋。數十年過去，structured programming 卻以一種不知能否算功成而退的方式被遺忘：現在的學生們自然地把程式寫成塊狀的結構，許多人甚至已經不知有 goto 這個指令。但他們沒聽過 structured programming, 對於 Dijkstra 等人當年提倡的程式推論仍一樣地陌生。

我想知道這套概念的創始者們怎麼談它，因此好奇地想讀這本書。

「讓程式能依據其結構被理解、被證明」便是我心目中的「結構化編程」。而在那個時代，他們的挑戰便是設計語言、符號，使得這種編程與推論成為可能。