Formal Method for the Retrospective Specification of the Functionality of Existing Software Systems

The dissertation proposes an unusual but reasonable alternative for the interpretation of programs. Pursuant to this the text of a program denotes a finite set of disjoint relations called the ‘functionality of that program. The relations so associated with the program perfectly represent the different ways in which the program can participate in the realization of the functional specification of the incorporating software system. The accurate definition of the functionality of a program amounts to the functional specification which the program complies with in reality. The pursuance of this subject resulted in a new formal semantics called functional semantics for programming languages. The work on a functional semantics adopted those techniques which have been applied in the formalization of programming language semantics. Yet the functional approach differs qualitatively from the classical ones Since it involves a necessary concern for the pragmatics of the target language. As demonstrated in the dissertation, the operational part of the text of a program is ambiguous in view of the functionality of that program since the externally observable behaviour of two programs of identical operational part may differ considerably. The formal treatment of ambiguity has required a necessary departure from the classical semantic ideas. Within the functional approach, the declaration part of the text of a program has a peculiar significance. The declarations are interpreted as giving positive indication of a situation which is set up by the other programs of the incorporating software system. The meaning of the operational part of the program is resolved in this situation, and it is identical with the functionality of the complete program. The program-functionalities are expressed formally in a constructive sublanguage of classical first order logic in the form of a finite set of inductive definitions. Given that the applied sublanguage of first order logic is universal in view of computability, the meaning function of functional semantics translates, indeed, a program into a_ functionally equivalent logic program The work has a number of practical implications. These include the reasoning about the inherent structure of a sequence of program statements or the maximal parallel implementation of a program. The techniques resulted from the work seem to have some significance beyond programming languages.