## Reflections on Abstractions: Cases vs Models

Abstraction Awareness is about deeper understanding of abstraction, a concept so basic to human thinking. Subsequently abstraction is discussed by the means of basic Finite Model Theory.

All finite relational structures can uniquely be described in First Order Logic (FO) up to isomorphy. This is quite pleasant, since FO is a relatively nice and simple language (for expressing queries, doing proofs, etc). For example, a structure consisting of a 2-elementary alphabet and a binary relation R (see figure) can be characterised by conjunction of the following sentences:
I
(1) there are exactly 2 elements
(2) for x≠y: R(x,x), R(y,y) holds, R(x,y), R(y,x) doesn’t
where both sentences can be expressed in FO (see here for formalism).

However, another way to characterise R is:
II
(1) as above
(2′) R is reflexive and empty else ( x=y ⇔ R(x,y) )
what is also expressible in FO.

Between the two axiom systems (I) and (II) there is an essential difference: While (I) lists all existing cases in (2), (II) uses the property of reflexivity (2′) to characterise the structure. The latter has certain advantages: it, can be expanded easily for structures of more than 2 elements, and it states a principle that can be understood by humans.

This describes by simple means of basic Finite Model Theory a very important principle in software engineering: modelling properties is more expressive than just collecting cases. This is the reason why test cases can be derived from specifications but not vice versa. Another example is Intentional Programming, addressing that the big picture ‘gets lost’ on the source code level.

Like most things in life, expressing properties by models also comes with a downside: While cases as in (I) can always be expressed in FO, properties in general cannot. For example, for expressing that the alphabet of a structure is always of even size, FO is not expressive enough.

Thus, altogether cases vs models is always a trade-off.

So long
|=

PS for the ‘light’ version, see previous post