So, continuing on last night's idea, there's the issue of just what can and can't be proved via Axiomatic Semantics. The short answer is that the "can't prove" set contains just about everything we care about. Dijkstra's Predicate Transformer is nice from a mathematical standpoint but, as a tool, it's pretty limited because proving total correctness for most programs is a fools errand: they aren't totally correct!
Hoare's Proof System relaxes the constraint on loops having to finish, which makes it a lot easier to prove many things work and, while infinite loops do happen, they are usually pretty easy to find and fix. However, even Hoare's system becomes unwieldy once you're talking about a decent sized system. Even taken in unit-test-sized chunks, it's a lot of work.
What I'm suggesting isn't formal validation at all, but rather using the test data to suggest the implementation (rather than the other way around). This is at the heart of Test Driven Design (TDD). The problem I have with Test Driven Design (and, I don't think it's a fundamental problem, just a symptom of a relatively young paradigm) is that it ignores a lot of information in the problem statement when devising a solution. A set of inputs and assertions can be viewed as a contract, but usually these are just examples of a more complex business problem. What I think is missing is a methodical way of looking at the patterns of the test data and determining which design patterns are appropriate for the solution. Refactoring is a very big part of TDD, but it never hurts to start off on the right foot.
No comments:
Post a Comment