A formal system for specifying and verifying program performance

<p>Formal techniques for specifying performance properties of programs (e.g., execution time) and for verifying the correctness of these specifications are developed. These techniques are extensions of well-known predicate transformer techniques for specifying and verifying purely functional properties of programs.</p>