Example
namespace CodeContractsDemo
{
using System;
using System.Diagnostics.Contracts;
public class Point
{
public int X { get; set; }
public int Y { get; set; }
public Point()
{
}
public Point(int x, int y)
{
this.X = x;
this.Y = y;
}
public void Set(int x, int y)
{
this.X = x;
this.Y = y;
}
public void Test(int x, int y)
{
for (int dx = -x; dx <= x; dx++) {
this.X = dx;
Console.WriteLine("Current X = {0}", this.X);
}
for (int dy = -y; dy <= y; dy++) {
this.Y = dy;
Console.WriteLine("Current Y = {0}", this.Y);
}
Console.WriteLine("X = {0}", this.X);
Console.WriteLine("Y = {0}", this.Y);
}
[ContractInvariantMethod]
private void ValidateCoordinates()
{
Contract.Invariant(this.X >= 0);
Contract.Invariant(this.Y >= 0);
}
}
}