How can I define preconditions in an external state using code contracts?

How do I place a precondition in a method Invoke

in the following interface, specifying that the object denoted by a symbol ObjectId

must exist ?:

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

      

Attempt # 1

I already have a command called IObjectExistsCommand

that can be used to determine the existence of objects. These commands can be created with IObjectExistsCommandFactory

. I thought about doing the following, but this adds unwanted noise to the command interface (IMO):

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

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

      

Attempt # 2

Likewise above, except for use ServiceLocator

. Undesirable for obvious reasons, but cleaner:

interface IDeleteObjectCommand {
   Guid ObjectId { get; }

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

      

The EDIT: . How would you define postconditions on the outward state? That is, saying that this method results in a new file being created.

+3


source to share


2 answers


I think this is a bad idea. This is one of those contracts that fall under the race conditions, and I don't like it (two callers confirm that the contract is satisfied, then one wins the race to delete the object, and then the other gets a contract violation exception when he tries to delete the object).



Throw an exception if the object to be deleted does not exist.

+1


source


I decided to create a "Prerequisites" enum

that defines the external preconditions. Then I defined a separate interface method that returns enum

, thus hinting that the external state bits are invalid:

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

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

enum DeleteObjectPreconditions { ObjectExists, ObjectUnlocked };

      

Am I totally bullying for this? The only drawback of this, of course, is that users do not have provable means that satisfy the preconditions forever ...



EDIT: I really prefer the service location method. At least with this approach, users can prove that preconditions are met through a contractual (albeit service) interface.

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

0


source







All Articles