Here comes another post about Code Contracts. Remember my post First Steps with Code Contracts?
Let’s just recall which class we have been working on last time:
1: namespace Vehicles
3: class Car : IVehicle
5: string name;
6: int speed;
8: public Car(string name, int speed)
10: this.name = name.ToUpper();
11: this.speed = speed;
14: void IVehicle.Drive(int speed)
16: Console.WriteLine("Car " + name +
17: " is driving at a speed of " + speed);
20: public bool IsFasterThan(Car c2)
22: Console.WriteLine(name.ToUpper() +
23: " is faster than "
24: + c2.name.ToUpper());
25: if (this.speed > c2.speed)
26: return true;
27: else return false;
31: void ObjectInvariant()
33: Contract.Invariant(name != null);
Snippet 1: The Car class from the First Steps with Code Contracts example.
After completing all the steps from that example, in the end we should have ended up with at least one warning generated by Code Contracts:
Code Contracts: Possibly calling a method on a null reference ‘c2.name’
with respect to line 24.
Now, if we review the usage of Object Invariants (First Steps with Code Contracts), we would see immediately that the purpose of Objects invariants is to provide us a mechanism to perform the checking in ObjectInvariant() in all instances (and instances of subclasses) of Car.
It seems there are no assumptions generated for the Objects Invariants of objects of the same type passed as a parameter (at least not yet, maybe it’ll come).
In order to avoid the warning, we can do 2 things:
- Assumption:Contract.Assume(!String.IsNullOrEmpty(name)) or
- Postcondition: Create a property w/ getter postcondition ensuring the result is not null
That should about do the trick!
Enjoy and see you next time!