We propose a theory of the semantic analysis of programs, providing a unified framework to carry out some analyses, from the most precise ones, like the ones that are performed to justify the total correctness of programs, to the coarsest, like the ones that are used in compilation. In our opinion, there is no lack of continuity between these two extremes, and the theory we propose allows the construction of a continuous range of applications, from exact analysis to the most approximate analyses. Since we care about practical applications, we have devoted part of our efforts to build up a model leading to automatized solutions, (some automatizations having effectively been realized), to economically relevant problems.
Generally, the development of a theory for the semantic analysis of programs leading to automatized applications, is justified by the technical resolution of the software reliability and software efficiency problems. It is, in our opinion, complementary to the efforts, which are currently made to turn the art of programming into the status of a science.
Let us now give a very short summary of the content of this thesis:
We will reduce the problem of the determination of semantic properties of a program, to the problem of building up the extreme fixed points of monotone operators on a complete lattice. After this introduction, the second chapter is then dedicated to the mathematical study of fixed-point theorems in complete lattices. We provide a constructive demonstration of Tarski's theorem, showing that the set of fixed points of a monotone operator F on a complete lattice L is the image of L by the pre-closures defined by means of transfinite iteration limits. It is a matter of showing how classic iterative methods can be adapted to converge starting from any starting point and also, to reach fixed points other than the least and the greatest one. This also allows us to define the union and the intersection in the lattice of the fixed points of F in a constructive way, that is by recurrences using F. We then obtain, as a particular case, the theorem of construction of the least fixed point of a continuous operator. We will then consider some systems of monotone fixed point equations in a complete lattice. After remembering the formal resolution method by elimination of variables, we will demonstrate a convergence result of chaotic iterative methods, asynchronous and asynchronous with memory. This opens the way to the resolution of systems of monotone equations on a lattice, using different processors, calculating in parallel, without the necessity of any synchronization.
In the third chapter, the problem of semantic analysis of programs is studied independently on the problems of language definition, within the very general framework of studying the behavioral of a discrete dynamic system. A program is a discrete dynamic system as long as it defines a transition relation (or a transition function, if it is deterministic), between the states of memory preceding or following the execution of any elementary instruction. To study the behavior of a dynamic discrete system, it is necessary to characterize the set of reachable states satisfying a given entry specification, or else, to characterize the set of ascendants satisfying a given exit specification. In other words, it is necessary to determine the weakest pre-condition, regarding the entry states, so that the system may evolve towards a state satisfying a given postcondition, or the strongest post-condition characterizing the states towards which the system evolves, starting from any entry state, satisfying a given pre-condition. We will show that these conditions are obtained as solutions of fixed-points equations or of equation systems, when the set of states of the dynamic discrete system is partitioned. We will then formalize the operational semantics of a simple programming language, corresponding to sequential iterative programs, and we will show how a program defines a discrete dynamic system. We will then apply the results obtained by the analysis of discrete dynamic systems behavior to the semantic analysis of programs. This leads us to define forward and backward deductive semantics of programs, generalizing the classic forward program verification method of Floyd-Naur, and the backward method of Hoare-Dijkstra, to techniques for formalizing the semantics of programming languages. In fact, the forward and backwards deductive semantics define the conditions in which a program is correctly carried out, is not carried out at all, or leads to an error as a solution of semantic equation systems, associated to the program. Both semantics can be used to characterize, in each point of the program, the set of descendants of the entry states and the set of ascendants of the exit states. As a consequence, they are equivalent, as both allow to make an exact semantic analysis of programs.
After having shown that the exact semantic analysis of programs consists in solving equation systems, keeping in mind that the solutions to these equations are not automatically computable, and wishing, at the same time, to find some automatic techniques of semantic analysis of programs, we are forced to limit ourselves to approximate automatic analyses of programs. So in chapter four we will study some calculation methods for approximating fixed points of monotone operators on a lattice. To effectively calculate lower and upper approximations of the solutions of an equation system, we essentially propose two complementary methods. They consist, on one end, in simplifying the equations to solve and, on the other end, in accelerating the convergence of iterative methods of fixed-point construction. To accelerate the convergence of an iteration which does not stabilize itself naturally in a fixed number of steps, we propose to extrapolate, while calculating the terms of the sequence of iterates to obtain an approximation of its limit in a finite number of steps. As in iterative methods with convergence acceleration, the simplification of equations is widely used in numerical analysis but, for what our problems need, we have to study them in a purely algebraic framework. To simplify the semantic equation systems associated to the programs, for each particular problem of semantic analysis of programs, we propose to ignore a priori certain properties and only keep the program properties which are meaningful for this specific application. From an algebraic viewpoint, this approximation is formalized by a closure in the domain of the equations to solve, a closure that we will define, in an equivalent way, by a Moore family, as relations of congruence, or pairs of adjoint functions. Different approximate analyses can be combined by combining the corresponding closures, and in particular the lattice of closures formalizes the creation of a hierarchy of approximations, depending on their precision.
In chapter five we will develop automatic semantic programs analysis methods, therefore necessarily approximate. In order to perform an approximate semantic analysis of programs, we propose to compute an approximation of the forward and backward systems of semantic equations associated to this program. Having chosen a particular class of program properties providing useful answers to a given problem, we will show how the results of chapter four allows us to design an algorithm which can automatically carry out the analysis of any program for this class of properties. The design of this algorithm is based on the choice of a closure allowing to define a space of approximate properties, as well as the rules of construction of systems of simplified equation systems associated to a program. To solve these equations, we will use an iterative method. Extrapolation operations will also have to be designed when conver gence must be accelerated. We will illustrate our approach by giving some examples of the conception of an approximate semantic analysis of programs. After having briefly examined many different classic examples within program optimization, we will deal with some applications to the discovery of pointers properties, the determination of the types of variables in high level languages without declarations, the analysis of the interval of values of numeric variables, and also to the discovery of linear relations of equality or inequality between the variables of a program.
Chapter six deals with recursive procedures, whose analysis is more complex than the one of sequential iterative programs, given that it is necessary to consider functional equations of the form f(x) = F(f)(x), and not equations of the type x = f(x), any more. We will use the same approach as for iterative sequential programs, by defining a deductive semantics, then, by introducing some approximation methods which, in fact, generalize the study of chapter four in the case of functional equation systems.
\bibitem{Cousot78-1-TheseEtat}
P. Cousot.
\newblock M{\'e}\-tho\-des it{\'e}\-ra\-ti\-ves de cons\-truc\-tion et
d'ap\-pro\-xi\-ma\-tion de points fi\-xes d'op{\'e}\-ra\-teurs
mo\-no\-to\-nes sur un treil\-lis, ana\-ly\-se s{\'e}\-man\-ti\-que
de pro\-gram\-mes (in {F}rench).
\newblock Th{\`e}\-se d'{{\'E}}tat {\`e}s sci\-en\-ces ma\-th{\'e}\-ma\-ti\-ques,
Uni\-ver\-si\-t{\'e} Jo\-seph Fou\-r\-ier, Gre\-no\-ble,
Fran\-ce, 21 March 1978.
@phdThesis{Cousot78-1-TheseEtat,
author = {Cousot, P{.}},
title = {M{\'e}\-tho\-des it{\'e}\-ra\-ti\-ves de cons\-truc\-tion et
d'ap\-pro\-xi\-ma\-tion de points fi\-xes d'op{\'e}\-ra\-teurs
mo\-no\-to\-nes sur un treil\-lis, ana\-ly\-se s{\'e}\-man\-ti\-que
de pro\-gram\-mes (in {F}rench)},
type = {Th{\`e}\-se d'{{\'E}}tat {\`e}s sci\-en\-ces
ma\-th{\'e}\-ma\-ti\-ques},
school = {Uni\-ver\-si\-t{\'e} Jo\-seph Fou\-r\-ier},
address = {Gre\-no\-ble, Fran\-ce},
month = {21 March},
year = 1978,
}