Asserting Implications

A short one today!

When using assertions heavily, a common pattern is asserting an implication:

assert(a implies b);

Most programming languages don’t have special syntax for implication, as you don’t often branch based on implications. But in my experience, you want to assert implications all the time!

Recall that and, or, and not logical operators form a basis, so an implication can be expressed in terms of disjunction and negation:

A \Rightarrow B \Leftrightarrow \neg A \lor B

This tautology is how asserting that a implies b gets expressed by default:

assert(!a or b);

I find this form hard to read, and suggest using the if instead:

if (a) assert(b);

From a recent code change:

// Before:
assert(header_b != null or replica.commit_min == replica.op_checkpoint);

// After:
if (header_b == null) assert(replica.commit_min == replica.op_checkpoint);