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.
source to share
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.
source to share
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?
source to share