Markov chains and formal proofs
I’ve posted this link before, when this blog was on the late lamented Posterous, but when I went looking for it again, it had disappeared - so here it is again, for good measure. Hat tip to Kent Beck for originally tweeting about this article explaining Markov chains.
I’m reading some interesting follow-on papers, in particular, a pair by James A Whittaker (Yes, that James A Whittaker) “A Markov Chain Model for Statistical Software Testing” and “Markov Analysis of Software Specifications” as well as a graduate thesis by Ivan S. Zapreev entitled “Model Checking Markov Chains: Techniques and Tools”. I’m interested in the effect of a program’s cyclomatic complexity on the feasibility of using Markov chains for testing purposes.
Until now, I haven’t found formal proofs of anything other than trivial software systems to be convincing; they appear to rely on a perfect test oracle, namely a specification that’s so well specified that it may as well be the software system itself. Formal approaches such as Dijkstra’s tend to approach software systems in some idealised way, not as gloriously nonlinear entities executing on top of preemptively multi-tasking operating systems and making use of imperfect APIs over unreliable networks… and even if I concede that it’s possible to prove that a software system is internally perfectly consistent, that tells me nothing about how well that system actually solves the needs of the customer paying for it.
But in any case, I think Markov chains are worth exploring.