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.

Add an `Object Object { get; }` property to the interface, that returns the object itself rather than the ID? — Rob, Mar 06 '12 at 14:53
Interesting question. I can't see that you have any alternatives other than providing the means to check through the interface itself (attempt #1), or providing a static means (attempt #2). But I might be wrong. — Rob, Mar 06 '12 at 14:57
Hmm, I'm not sure loading the entity upfront would be a workable compromise in all cases. Thanks for the suggestion though. — Lawrence Wagerfield, Mar 06 '12 at 16:51
This seems like more of an assertion then a contract check IMHO. I think a contract check would cover that ObjectId was not Guid.Empty, giving you the confidence to continue. — Davin Tryon, Mar 06 '12 at 17:41
The issue here is that users could still receive exceptions even if they obey all preconditions on the method. I thought the idea is to make methods deterministic so users can be 100% certain that no exceptions will be thrown when they obey preconditions.. — Lawrence Wagerfield, Mar 06 '12 at 17:49
Something about this doesn't really smell right to me. I have a feeling that if the caller can verify with metaphysical certitude that the GUID is valid, then they should also be able to call a concrete Delete method on some object or static class rather than calling Invoke on a abstract command interface. Maybe you could tell us more about this design so we could see what other options exist? — Jeffrey L Whitledge, Mar 06 '12 at 18:02

score 1 · Accepted Answer · answered Mar 09 '12 at 16:01

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.

answered Mar 09 '12 at 16:01

jason

236,483
35
423
525

I agree with what your saying, but doesn't this contradict with the notion that you shouldn't rely on exceptions to control application flow? Furthermore, isn't it the responsibility of the caller to ensure a lock is present on the resource, either via a TransactionScope or some other mechanism? – Lawrence Wagerfield Mar 09 '12 at 16:25
I think this is exactly what exceptions are for. Here's another, more obvious case: imagine a function that `Requires(File.Exists(someArg))` - there's absolutely no way for the caller to guarantee that, since it relies on third-party state that it can't control, so it's the perfect situation to throw an exception on failure instead of `Requires`. – porges Mar 14 '12 at 04:34

Lawrence Wagerfield · Answer 2 · 2012-03-09T15:48:49.790

0

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?

edited Mar 09 '12 at 15:48

answered Mar 09 '12 at 15:36

Lawrence Wagerfield

6,471
5
42
84

1

"The only downside to this of course is that users have no provable means for ever satisfying the preconditions..." So the only downside is that it's pointless? That sounds like a big "only" downside to me. – jason Mar 09 '12 at 15:51
+1 I think this was a brief moment of insanity brought on by desperation. I'm not actually going with this solution :) – Lawrence Wagerfield Mar 09 '12 at 15:52
If you can't ever satisfy the contracts 100% then they shouldn't be contracts. :) – porges Mar 14 '12 at 04:34
Since extrinsic state can be modified by someone else at any time, does this mean we should avoid placing pre/post conditions on such things? I.e. 'a precondition of method X is that the file must exist'. – Lawrence Wagerfield Mar 14 '12 at 21:22

How to define preconditions on extrinsic state using Code Contracts?

2 Answers2