Ben Wegbreit
Abstract
It is shown that specifications of program performance can be formally verified. Formal verification techniques, in particular, the method of inductive assertions, can be adapted to show that a program's maximum or mean execution time is correctly described by specifications supplied with the program. To formally establish the mean execution time, branching probabilities are expressed using inductive assertions which involve probability distributions. Verification conditions are formed and proved which establish that if the input distribution is correctly described by the input specifications, then the inductive assertions correctly describe the probability distributions of the data during execution. Once the inductive assertions are shown to be correct, branching probabilities are obtained and mean computation time is computed.
- 1 FLOYD, R Asslgnmg meanings to programs Proc Symp in Apphed Mathematms, Vol 19, J T Schwartz, Ed , Amer Math Soc , Providence, R.I , 1967, pp 19-32Google Scholar
- 2 KNUTH, D E. The Art of Computer Programming, Vol 3, Sonmg and Searching Addison-Wesley, Reading, Mass, 1973. Google Scholar
- 3 WEGBREIT, B. Mechamcal program analysis Comm ACM 18, 9 (Sept 1975), 528-539. Google Scholar
Index Terms
- Verifying Program Performance
Recommendations
A strategy for efficiently verifying requirements
This paper describes a compositional proof strategy for verifying properties of requirements specifications. The proof strategy, which may be applied using either a model checker or a theorem prover, uses known state invariants to prove state and ...
A unified proof technique for verifying program correctness with big-step semantics
AbstractThe deductive verification of computer programs helps ascertain the absence of errors for all possible inputs and executions. Computer programs can be written in a plethora of languages. The identification of mechanisms for reasoning ...
Highlights- A language-independent technique for formally proving the correctness of programs
Comments