How to define preconditions on extrinsic state using Code Contracts?

Question

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.

Answer 1

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.

Answer 2

I have decided to create a 'Preconditions' enum which defines extrinsic pre-conditions. I have then defined a separate method on the interface which returns the enum, thus hinting at which bits of extrinsic state are invalid:

interface IDeleteObjectCommand {
   Guid ObjectId { get; }
   DeleteObjectPreconditions? GetImpediments();

   // Contract.Requires(!this.GetImpediments().HasValue);
   void Invoke();
}

enum DeleteObjectPreconditions { ObjectExists, ObjectUnlocked };

Am I completely bonkers for doing this? The only downside to this of course is that users have no provable means for ever satisfying the preconditions...

EDIT: I actually prefer the service location method over this. At least with that approach users are able to prove that pre-conditions are being satisfied through a contracted (albeit service-located) interface.

EDIT 2: This raises an interesting question... how would you define post-conditions on extrinsic state?