Search code examples
c#.netcode-contractsspecificationsspec#

How to define preconditions on extrinsic state using Code Contracts?


How do I place a precondition on the Invoke method in the following interface stating that the object denoted by ObjectId must exist?:

interface IDeleteObjectCommand {
   Guid ObjectId { get; }
   void Invoke();
}

Attempt #1

I already have a command called IObjectExistsCommand which can be used to determine if objects exist. These commands can be instantiated via an IObjectExistsCommandFactory . I have thought about doing the following, but this adds undesirable noise to the command's interface (IMO):

interface IDeleteObjectCommand {
   IObjectExistsCommandFactory ObjectExistsCommandFactory { get; }
   Guid ObjectId { get; }

   // Contract.Requires(ObjectExistsCommandFactory.Create(ObjectId).Invoke());
   void Invoke();
}

Attempt #2

Similar to above, except use ServiceLocator. Undesirable for obvious reasons, but is cleaner:

interface IDeleteObjectCommand {
   Guid ObjectId { get; }

   // Contract.Requires(ServiceLocator.Get<ObjectExistsCommandFactory>().Create(ObjectId).Invoke());
   void Invoke();
}

EDIT: Similarly, how would you define post-conditions on extrinsic state? I.e. saying that this method results in the existence of a new file.


Solution

  • I think this is a bad idea. This is one of those contracts that is subject to a race condition and I don't like those (two callers verify that the contract is satisfied, then one wins the race to delete the object, and then the second gets a contract violation exception when it tries to delete the object).

    Throw an exception if the object to be deleted doesn't exist.