Exit Criteria:

• We empower developers to articulate program contracts using a C-like language.

Deliverables:

• Description of C-like language to specify program contracts.