On Verifying Resource Contracts using Code Contracts

In this paper we present an approach to check resource consumption contracts using an off-the-shelf static analyzer. We propose a set of annotations to support resource usage specifications, in particular, dynamic memory consumption constraints. Since dynamic memory may be recycled by a memory manager, the consumption of this resource is not monotone. The specification language can express both memory consumption and lifetime properties in a modular fashion. We develop a proof-of-concept implementation by extending CODE CONTRACTS ’ specification language. To verify the correctness of these annotations we rely on the CODE CONTRACTS static verifier and a points-to analysis. We also briefly discuss possible extensions of our approach to deal with non-linear expressions. 1 Problem statement Design by contract [24] is a programming discipline that prescribes that software designers should define formal, precise and verifiable interface specifications for software components, extending the ordinary definition of abstract data types with preconditions, postconditions and invariants. While there has been some success in the adoption of contracts for enforcing functional requirements and design decisions [23, 25], there have not been many signs of their usage to express non-functiona