Discovering Empirical Theories of Modular Software Systems. An Algebraic Approach

This paper is concerned with the construction of theories of software
systems yielding adequate predictions of their target systems’ computations. It
is first argued that mathematical theories of programs are not able to provide
predictions that are consistent with observed executions. Empirical theories of
software systems are here introduced semantically, in terms of a hierarchy of
computational models that are supplied by formal methods and testing techniques
in computer science. Both deductive top-down and inductive bottom-up approaches
in the discovery of semantic software theories are refused to argue in favour
of the abductive process of hypothesising and refining models at each level in
the hierarchy, until they become satisfactorily predictive. Empirical theories of
computational systems are required to be modular, as modular are most software
verification and testing activities. We argue that logic relations must be thereby
defined among models representing different modules in a semantic theory of a
modular software system. We exclude that scientific structuralism is able to define
module relations needed in software modular theories. The algebraic Theory of
Institutions is finally introduced to specify the logic structure of modular semantic
theories of computational systems.