Seminal though this letter is, the anniversary was nine months ago.
It happens that I cited this in a talk I gave three hours ago, describing the path that took me to building Java by Contract. Dijkstra’s formal approach to programming as evinced by publications such as A Discipline of Programming relied on the fact that given knowledge of the state of a computer at some point in the program’s execution, you could assert the state after it executed the next statement. Then, by induction, the subsequent state, and so on to build a proof of the state at the end of the program: you could build the program’s contract.
Go to statements make this much harder because you can’t know that the state now is the result of executing the preceding program: you might have got further then jumped back here. If control flow is limited to things like loops, conditionals and subroutine application, then those limited things can be turned into “black boxes” and the proof of the behaviour of all of the internal statements replaced substituted for a statement about the overall effect of the box. It’s an important step on the way to both Z-style formal methods and Design by Contract.
It’s interesting to bear that modularity and substitutability in mind when reading Goodenough’s papers on exception handling, because it’s very easy for lightly-thought exception mechanisms to leave modules in inconsistent states.
Seminal though this letter is, the anniversary was nine months ago.
It happens that I cited this in a talk I gave three hours ago, describing the path that took me to building Java by Contract. Dijkstra’s formal approach to programming as evinced by publications such as A Discipline of Programming relied on the fact that given knowledge of the state of a computer at some point in the program’s execution, you could assert the state after it executed the next statement. Then, by induction, the subsequent state, and so on to build a proof of the state at the end of the program: you could build the program’s contract.
Go to statements make this much harder because you can’t know that the state now is the result of executing the preceding program: you might have got further then jumped back here. If control flow is limited to things like loops, conditionals and subroutine application, then those limited things can be turned into “black boxes” and the proof of the behaviour of all of the internal statements replaced substituted for a statement about the overall effect of the box. It’s an important step on the way to both Z-style formal methods and Design by Contract.
It’s interesting to bear that modularity and substitutability in mind when reading Goodenough’s papers on exception handling, because it’s very easy for lightly-thought exception mechanisms to leave modules in inconsistent states.