# Static Contract Simplification

## TL;DR

This paper introduces a static program transformation technique to simplify contracts in code, reducing runtime overhead of contract checks while maintaining behavior, through contract propagation and merging.

## Contribution

It proposes a novel static transformation method that reduces runtime contract checking overhead by propagating and merging contracts at compile time, preserving program behavior.

## Key findings

- Transformations never increase contract checks
- Effective contract propagation and merging reduces runtime overhead
- Supports different levels of blame preservation

## Abstract

Contracts and contract monitoring are a powerful mechanism for specifying properties and guaranteeing them at run time. However, run time monitoring of contracts imposes a significant overhead. The execution time is impacted by the insertion of contract checks as well as by the introduction of proxy objects that perform delayed contract checks on demand. Static contract simplification attacks this issue using program transformation. It applies compile-time transformations to programs with contracts to reduce the overall run time while preserving the original behavior. Our key technique is to statically propagate contracts through the program and to evaluate and merge contracts where possible. The goal is to obtain residual contracts that are collectively cheaper to check at run time. We distinguish different levels of preservation of behavior, which impose different limitations on the admissible transformations: Strong blame preservation, where the transformation is a behavioral equivalence, and weak blame preservation, where the transformed program is equivalent up to the particular violation reported. Our transformations never increase the overall number of contract checks.