A formal system for specifying and verifying program performance

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.