Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra

Two different methods of flow analysis are discussed, one a significant generalization of the other. It is shown that the two methods have significantly different intrinsic computational complexities. As an outgrowth of our observations it is shown that a feature of the programming language used by Dijkstra in A Discipline of Programming makes it unsuitable for compile-time type checking, thus suggesting that flow analysis is applicable to the design of programming languages, as well as to their implementation. It is also shown that program verification by the method of inductive assertions is very likely to lead to assertions whose lengths and proofs are not polynomially bounded in the size of the program being verified, even for very simple programs. This last observation casts further doubt on the practicality and relevance of mechanized verification of arbitrary programs.