Code Contracts
Postconditions
Invariants
Defining Contracts on Interface
Preconditions