Code Contracts Transformation Specification

Back to top Code Contracts Developer Documentation

The program transformation specification is broken down in the following sections:

1. Function Contracts Reminder
2. Program Transformation Overview
3. Generating GOTO Functions From Contract Clauses
4. Rewriting Declarative Assign and Frees Specification Functions

1. Rewriting User-Defined Memory Predicates
2. Dynamic Frame Condition Checking
3. Proof Harness Intrumentation
4. Checking a Contract Against a Function

1. Checking a Contract Against a Recursive Function
2. Replacing a Function by a Contract

---

Prev	Next
Code Contracts Developer Documentation	Function Contracts Reminder