Exercise: Checking invariants and conditions using Microsoft Code Contracts

In this exercise you will use Microsoft Code Contracts to set up Pre-conditions, Post-condictions, and Object Invariants on a class.

Install the plugin Code Contracts for .NET

First you must install the Visual Studio plugin Code Contracts for .NET.

Getting ready

1. In Visual Studio create a new project, named CodeContractsExercise (or something similar).
2. In Vusla Studio right-click the project node, and choose Properties (at the very bottom of the menu).
3. Go into the "Code Contracts" tab.
4. Make sure that both of these are checked
   "Perform Runtime Contract Checking"
   "Perform Static Contract Checking"
   

Object invariant

Create a simple class Book with a property String Title.

The Title property must have an object invariant: The length of the title must be at least 2 characters.

Make a Main to try it out: With legal and illegal titles.

Unit test it!

Another object invariant

Add another property to the class Book: double Price.

The Price propety must have an object invariant: Price >= 0.0.

Adapt the Main to try it out: With legal and illegal prices.

Unit test it!

Pre- and post-conditions

Add a method to the class Book

• public void RaisePriceTo(double newPrice)
  This method must change the price.
  Pre-condiction: newPrice > Price
  Post-condition: Price > old price

Try it in Main ... + Unit test it!

Pre- and post-condition, more ...

Add yet another method to the class Book

• public void LowerPriceTo(double newPrice)
  This method must change the price
  Pre-condiction: newPrice > Price
  Post-condition: old Price > Price

Try it in Main ... + Unit test it!