Notation for API features, reasoning about consistency

[bvssvni]

This notation can be used to reason about consistency for APIs that may vary across platforms. Syntax is based on Prolog, but extended with consistency for what-usually-happens semantics. It can also be used in pragmatic domains where there is uncertainty but not enough information to use probability.

The basic idea is that features are either coupled with other features (X, Y) or decoupled X, Y, and the implementation has 4 variations !X (not supported), ?!X (usually not supported), ?X (usually supported) and X (supported).

Rules

• ?X means usually true (more often true than false, but both might happen).
• !X or absence of X means X is false
• , means logical "and".
• Logical "or" makes usually not sense, but when it does ; can be used.
• Ends with .. A single . means everything is false.
• !?X = ?!X - something that is not usually true is usually false.
• !?(X, Y) = ?(!X, !Y) - coupled features follow different inversion rules than Boolean algebra.

Examples

Features: X, Y.

• . - X and Y are not supported.
• ?!X. - X is usually not supported, Y is not supported.
• X, Y. - Both X and Y are true.
• X, ?Y. - X is true and Y is usually true.
• ?(X, Y). - X and Y are usually true, but sometimes both are false.
• ?(X, !Y). - Usually, X is true and Y is false, but sometimes X is false and Y is true.

Why does logical "or" ?!Sense

The reason logical "or" does not usually make sense is because when two coupled observations are usually true, they are false together too but never decoupled, such when inverted !?(X, Y) = ?(!X, !Y). In Boolean algebra this would be !?(X, Y) = ?(!X; !Y) which makes little sense.

Adding consistency semantics means that logical "or" can be express in other ways, but not precisely. For example ?X, ?Y. means it is possible that neither X or Y is supported (which is impossible for logical "or"), but this is rare, so it almost means the same thing.

Motivation

When writing back-end agnostic APIs we would like to make it as consistent as possible for library users, but we are sometimes dealing with back-ends with an underlying API that has inconsistent behavior across platforms. These cases can be tricky to reason about, and this notation allows us to formally verify that inconsistent behavior is detected and dealt with properly.

Another reason is that defining consistent behavior is hard when platforms are so different that a reference implementation does not make sense. It is easier to describe the specific characteristics of a platform through this notation about consistency and then categorize the recommended solutions.