Application of Implication

There is a very useful concept in linguistics and logic called entailment. One says that a implies b or a entails b meaning that if a is true, then b must also be true, or the whole expression is false. If however a is false, then the statement as a whole is true. One example could be: (p < q) entails (q > p); or that (a = b and b = c) entails (a = c).

The new Code Contracts for .Net formalism provides a way to inject Design by Contract into the .Net Framework. Code Contracts deal with boolean expressions; preconditions, postconditions and invariants are all about boolean properties that must be satisfied. It occurred to me that a simple extension method could help out here.

[Pure]
public static bool Implies(this bool iff, bool then)
{
	return iff ? then : true;
}

The ternary/conditional operator is used here. Another way to formulate implies would be as !iff || then. It may look strange but it is very useful in logic and in Code Contracts. Indeed this operator is also used in Eiffel, the mother of Design by Contract and the inspiration for Code Contracts. Let’s see a concrete code example of the application of implication: of implies in action:

[Pure]
public static bool LessThanOrEqual<X>(this X a, X b) where X : IOrder<X>
{
	Contract.Requires(a != null);
	Contract.Requires(b != null);
	Contract.Ensures(Contract.Result().Implies(a.Symmetric(b)));

	return a.Compare(b) <= Sign.Same;
}

The first two preconditions (Contract.Requires) are trivial, they merely safeguard against a possible null value for a and b, were X be be a reference type (class) and thus nullable.

The first postcondition (and third condition) is the interesting one. It states that if the result of the method is true then that implies that a must be symmetric to b. What that means is that if a ≤ b then it must also be the case that b ≥ a. This is in a way a specification of how the Compare method must work but in this case we specify it here as well.

It’s a simple example but without Implies the code would be slightly shorter but much less readable.

Enhanced by Zemanta
Advertisements

About xosfaere

Software Developer
This entry was posted in Computer Science, Declarative, Paradigm, Software, Technical and tagged , , , , , , , , , , , , . Bookmark the permalink.

2 Responses to Application of Implication

  1. David Ellis says:

    I found your post because I just ran into a place where the Code Contracts static checker is failing to deduce facts based on an implication in a Contract.Ensures().

    Anyway, I like the way your Implies() extension method looks but it does seem to have one drawback in that it is strict in its “then” parameter. If I write an implication out literally in a Contract statement I’ll get short-circuiting, but with the extension method both clauses in the implication are always evaluated. This could introduce unexpected run-time overhead. I which C# had a way to do this cleanly!

  2. xosfaere says:

    True. It does have a potential run-time overhead. This is mitigated by the fact that it is targeted at Code Contracts first and foremost and for these it shouldn’t matter too much with a little extra overhead. They can be switched off in production builds.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s