Abstraction Classes in Software Design

Strategic design statements articulate design decisions that determine the primary behavioural and structural properties of a program (software system). Strategic decisions address global, system-wide concerns and carry the most consequential implications.

Tactical design statements articulate design decisions that are concerned with a specific module. Tactical decisions often describe a pattern of correlations between one collection of modules (objects, procedures, classes etc.) and another.

At the lowest level of abstraction are concrete statements that are concerned with specific implementation details. An Implementation statement is not only ‘local’ but also ‘extensional’: it directly correlates to specific part of a specific program.

Architecture is concerned with the selection of architectural elements, their interaction, and the constraints on those elements and their interactions...

Design is concerned with the modularization and detailed interfaces of the design elements, their algorithms and procedures, and the data types needed to support the architecture and to satisfy the requirements.

Intension/Locality
Criterion

The Intension/Locality Hypothesis

Strategic statements are in Non-local Intensional
Tactical statements are in Local Intensional
Implementation statements are in Local Extensional

Universal Base Class

There is a class from which all other classes inherit.

φ = ∀c • c∈Class ∧ c≠Object ⇒ Inherit(c, Object)

p =

			class Object { }
			class Foo extends Object {}

p ⊨ φ

p' =

			class Object { }
			class Foo extends Object {}
			class Bar {} // extends?

p' ⊭ φ

Universal Base Class

Preserved under expansion? NO

UBC is in Non-local Intensional

Compiler must check each and every class to make sure that all of them inherit from some other class.

Finite Structures &
Tarski's Truth Conditions

Finite Structures

Finite structure M is an ordered pair <U_M, R_M> such that U_M={a₁,...a_k} is a finite set of entities, and R_M={R₁,...R_k} is a finite set of relations over the entitites in U_M.

Finite Structure of UBC

Entities: Foo, Object

Relations:

Class = { Foo, Object }
Inherit = { (Foo, Object) }

Tarski's Truth Conditions

P is true if, and only if, P.

For all x, True(x) if and only if φ(x),

Locality Criterion

A statement φ is local if, and only if, it is preserved under expansion.

A statement φ is local if, and only if, a program that satisfies cannot be expanded into a program that violates it.

Intension Criterion

A statement φ is extensional if, and only if, it is preserved both under expansion and under reduction.

A statement φ is extensional if, and only if, a program that satisfies cannot be expanded or reduced into a program that violates it.

Expansion Formally

M = <U, R> — finite strucuture

M' = <U', R'> — is an expansion of M if it can result by:

adding a non-empty finite set of new entities to U, i.e. {b₁,...b_j}
adding to each n-ary relation r in R zero or more n-tuples, each of which contains at least one of b₁,...b_j

Valid Expansion

			class Object {}
			class Foo extends Object {}

			class Object {}
			class Foo extends Object {}
			class Bar {}

Invalid Expansion

			class Object {}
			class Foo extends Object {}

			class Object {}
			class Foo extends Object {
			  someMethod() {}
			}

Layered Architecture

A layered system is organized hierarchically, each layer providing service to the layer above it and serving as a client to the layer below

Layered Architecture (Formally)

Each element belongs to exactly one layer
Each element may depend (invoke, inherit, etc) only on elements of the same or lower layers

φ =

∀x ∃!k∈N • Layer(x) = k

∀x,y • Depend(x, y) ⇒ Layer(x) ≥ Layer(y)

Finite Structure

Entities: UserProfileView, UserStore

Relations:

Layer = { (UserProfileView, 2), (UserStore, 1) }
Depend = { (UserProfileView, UserStore) }

Finite Structure (Expansion)

Entities: UserProfileView, UserStore, FriendsStore

Relations:

Layer = { (UserProfileView, 2), (UserStore, 1), (FriendsStore, 1) }
Depend = { (UserProfileView, UserStore), (FriendsStore, UserProfileView) }

Conclusions

Depend(FriendsStore, UserProfileView) but Layer(FriendsStore) < Layer(UserProfileView)

φ is not preserved under expansion

Layered Architecture is non-local intensional statement

Architectural Mismatch

A program p assumes all data to be communicated is represented as ASCII strings.

φ — assumtion

p ⊨ φ

A program q includes program p, but it is not an app where p is "intended to operate".

q — App

q ⊭ φ

p and q mismatch on φ

φ is non-local intensional

Practical Implications

Make architectural (non-local) assumptions explicit
Minimize the number of non-local assumptions

Non-local design decisions must be taken (and made explicit) early
Each non-local decision may potentially violate every other design decision (architectural mismatch)
Local design decisions have limited consequences and are thus better postponed to the point following all non-local design decisions

When developing a new component, minimize the non-local assumptions it makes and make them explicit
When assembling an application from existing components, use only components whose non-local assumptions "match"
Tools that enforce non-local rules are inherently different from tools that verify local statements

Abstraction Classes in Software Design