Q.e.d. Code

QED 10: The Two Generals Problem



Listener Richard Allen writes to ask about proving enough of a program correct to constrain the number of tests that must be written. I respond that you need both tests and proof. Otherwise, how could you know that the specification is what you intended? Two generals wish to reach consensus by sending messengers through enemy territory. How can this be achieved? You can prove, in fact, that it cannot. This has important rammifications on the design of distributed systems. To prove that prerequisites are satisfied before calling a method, you can use a factory method. By chaining these factory methods together, you can prove that an entire sequence of events must take place in the correct order. This makes a fluend API not only more readable, but also more provable.