A flow calculus ofmwp-bounds for complexity analysis
Neil Deaton Jones, Lars Bjørlykke Kristiansen · ACM Transactions on Computational Logic · 2009
We present a method for certifying that the values computed by an imperative program will be bounded by polynomials in the program's inputs. To this end, we introducemwp-matrices and define a semantic relation ⊧ C :M, where C is a program andMis anmwp-matrix. It follows straightforwardly from our definitions that there existsMsuch that ⊧ C :Mholds iff every value computed by C is bounded by a polynomial in the inputs. Furthermore, we provide a syntactical proof calculus and define the relation ⊢ C :Mto hold iff there exists a derivation in the calculus where C :Mis the bottom line. We prove that ⊢ C :Mimplies ⊧ C :M. By means of exhaustive proof search, an algorithm can decide if there existsMsuch that the relation ⊢ C :Mholds, and thus, our results yield a computational method.