what's the point of runtime code contracts behaviour?

Question

Hi,

If static code analysis proves that according to contracts, misuse of types cannot happen. So I don't have to spend processor cycles over and over again on defensive coding with if... then throw....

So what does runtime behaviour gives me? Or rather how is it an advancement on if... then throw...? And what's the relation of static analysis and runtime checking? Are they mutually exclusive?

Thanks

---

something for spammers to harvest

Answer 1

Hi,

Ideally, static checking would be perfect and we wouldn't need runtime checking; however, in reality, static checking isn't perfect.

1. It sometimes generates false positives and unproven assertions, which you can avoid by placing explicit assumptions in your code with the Contract.Assume method.  Runtime checking is the only way to verify assumptions.
2. Sometimes assertions aren't even checked at all due to the possible infinite complexity of programs.
3. There are some things that the static checker won't even attempt to check; e.g., the contents of strings and delegates.  Lambdas passed to LINQ operators and async callbacks aren't statically checked at all.  I'm not sure whether iterator blocks are checked 100% either.

> And what's the relation of static analysis and runtime checking? Are they mutually exclusive?

No.  I often use both for the reasons given above.

In some projects, I'll just use runtime checking due to the performance of the static checker.

I never use the static checker without runtime checking, though sometimes I'll only enable runtime checking of preconditions in production deployments, if performance happens to be of great concern.  For staging deployments, I'll always enable runtime checking of everything.

- Dave

---

http://davesexton.com/blog

Answer 2

Thanks Dave,

Is it fair to say that for runtime checking only preconditions are relevant, postconditions and invariants are useful for static checker only?

I mean if you are sure about your input, then you should be sure about side effects and output? I'm trying to understand what would failed postcondition actually mean in production code. Doesn't it mean that that code shouldn't be in production yet?

Thanks

 

---

something for spammers to harvest

Answer 3

Hi,

> Is it fair to say that for runtime checking only preconditions are relevant [snip]?

No, I think all 3 points still apply.

1. It sometimes generates false positives and unproven assertions [snip]

Sometimes post-conditions and invariants, which are basically just post-conditions, are proven by the static checker with the help of explicit assumptions that you specify with Contract.Assume.  As stated previously, Contract.Assume can only be verified at runtime.  Thus, bad assumptions may cause post-conditions to fail at runtime.  In practice, I've seen it happen.

2. Sometimes assertions aren't even checked at all due to the possible infinite complexity of programs.

This includes post-conditions and invariants.  Again, in practice, I've seen it happen.  I usually resort to suppressing specific unproven contracts or disabling contract verification for an entire method, or even an entire class.  If the static checker isn't helping, then it seems important to check post-conditions at runtime.

Also consider complex contracts.  The code itself may be fairly straightforward, yet contracts can still be too complex to check statically.

3. There are some things that the static checker won't even attempt to check [snip]

This includes post-conditions and invariants.  Perhaps a common example is a post-condition against the contents of a string.

Contract.Ensures(Contract.Result<string>().StartsWith("Hello "));

An explicit assumption or a suppression attribute must be specified to avoid static checker warnings.  Essentially, the post-condition is based on an assumption, and assumptions can only be verified at runtime; however, if assumptions weren't being checked at runtime then you'd still want the post-conditions to be checked.

> Doesn't [failed post-conditions] mean that that code shouldn't be in production yet?

Yes, I agree.  It probably indicates bugs in your code that callers cannot fix themselves.*  That's why I always enable full runtime checking in staging deployments and, if possible, in production deployments as well.

*Assuming of course that the failing post-conditions aren't the result of bad explicit assumptions that fail to properly validate arguments, in which case workarounds may exist for callers if they can specify different arguments.

- Dave

---

http://davesexton.com/blog