ABSTRACT
Semantic analysis of programs is essential in optimizing compilers and program verification systems. It encompasses data flow analysis, data type determination, generation of approximate invariant assertions, etc.
Several recent papers (among others Cousot & Cousot[77a], Graham & Wegman[76], Kam & Ullman[76], Kildall[73], Rosen[78], Tarjan[76], Wegbreit[75]) have introduced abstract approaches to program analysis which are tantamount to the use of a program analysis framework (A,t,ã) where A is a lattice of (approximate) assertions, t is an (approximate) predicate transformer and ã is an often implicit function specifying the meaning of the elements of A. This paper is devoted to the systematic and correct design of program analysis frameworks with respect to a formal semantics.
Preliminary definitions are given in Section 2 concerning the merge over all paths and (least) fixpoint program-wide analysis methods. In Section 3 we briefly define the (forward and backward) deductive semantics of programs which is later used as a formal basis in order to prove the correctness of the approximate program analysis frameworks. Section 4 very shortly recall the main elements of the lattice theoretic approach to approximate semantic analysis of programs.
The design of a space of approximate assertions A is studied in Section 5. We first justify the very reasonable assumption that A must be chosen such that the exact invariant assertions of any program must have an upper approximation in A and that the approximate analysis of any program must be performed using a deterministic process. These assumptions are shown to imply that A is a Moore family, that the approximation operator (wich defines the least upper approximation of any assertion) is an upper closure operator and that A is necessarily a complete lattice. We next show that the connection between a space of approximate assertions and a computer representation is naturally made using a pair of isotone adjoined functions. This type of connection between two complete lattices is related to Galois connections thus making available classical mathematical results. Additional results are proved, they hold when no two approximate assertions have the same meaning.
In Section 6 we study and examplify various methods which can be used in order to define a space of approximate assertions or equivalently an approximation function. They include the characterization of the least Moore family containing an arbitrary set of assertions, the construction of the least closure operator greater than or equal to an arbitrary approximation function, the definition of closure operators by composition, the definition of a space of approximate assertions by means of a complete join congruence relation or by means of a family of principal ideals.
Section 7 is dedicated to the design of the approximate predicate transformer induced by a space of approximate assertions. First we look for a reasonable definition of the correctness of approximate predicate transformers and show that a local correctness condition can be given which has to be verified for every type of elementary statement. This local correctness condition ensures that the (merge over all paths or fixpoint) global analysis of any program is correct. Since isotony is not required for approximate predicate transformers to be correct it is shown that non-isotone program analysis frameworks are manageable although it is later argued that the isotony hypothesis is natural. We next show that among all possible approximate predicate transformers which can be used with a given space of approximate assertions there exists a best one which provides the maximum information relative to a program-wide analysis method. The best approximate predicate transformer induced by a space of approximate assertions turns out to be isotone. Some interesting consequences of the existence of a best predicate transformer are examined. One is that we have in hand a formal specification of the programs which have to be written in order to implement a program analysis framework once a representation of the space of approximate assertions has been chosen. Examples are given, including ones where the semantics of programs is formalized using Hoare[78]'s sets of traces.
In Section 8 we show that a hierarchy of approximate analyses can be defined according to the fineness of the approximations specified by a program analysis framework. Some elements of the hierarchy are shortly exhibited and related to the relevant literature.
In Section 9 we consider global program analysis methods. The distinction between "distributive" and "non-distributive" program analysis frameworks is studied. It is shown that when the best approximate predicate transformer is considered the coincidence or not of the merge over all paths and least fixpoint global analyses of programs is a consequence of the choice of the space of approximate assertions. It is shown that the space of approximate assertions can always be refined so that the merge over all paths analysis of a program can be defined by means of a least fixpoint of isotone equations.
Section 10 is devoted to the combination of program analysis frameworks. We study and examplify how to perform the "sum", "product" and "power" of program analysis frameworks. It is shown that combined analyses lead to more accurate information than the conjunction of the corresponding separate analyses but this can only be achieved by a new design of the approximate predicate transformer induced by the combined program analysis frameworks.
- Aho A. V. & Ullman J. D. {1977}, Principles of compiler design, Addison Wesley Pub. Co., (1977). Google ScholarDigital Library
- Birkhoff G. {1967}, Lattice theory, AMS Colloquium Pub., XXV, Third ed., Providence, R.I., (1967).Google Scholar
- Cousot P. {1977}, Asynchronous iterative methods for solving a fixed point system of motone equations in a complete lattice, Rapport de Recherche no88, Laboratoire IMAG, Grenoble, (Sept. 1977).Google Scholar
- Cousot P. & Cousot R. {1977a}, Abstract interpretation : a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conf. Rec. of the 4th ACM Symp. on Principles of Programming Languages, Los Angeles, Calif., (Jan. 1977), 238-252. Google ScholarDigital Library
- Cousot P. & Cousot R. {1977b}, Static determination of dynamic properties of recursive procedures, IFIP WG.2.2 Working Conf. on Formal Description of Programming Concepts, St-Andrews, Canada, North-Holland Pub. Co., (Aug. 1977).Google Scholar
- Cousot P. & Halbwachs N. {1978}, Automatic discovery of linear restraints among variables of a program, Conf. Rec. of the 5th ACM Symp. on Principles of Programming Languages, Tucson, Ariz., (Jan. 1978), 84-97. Google ScholarDigital Library
- Dijkstra E. W. {1976}, A discipline of programming, Prentice Hall, Englewood Cliffs, N.J., (1976). Google ScholarDigital Library
- Floyd R. W. {1967}, Assigning meaning to programs, Proc. Symp. in Applied Math., vol.19, AMS, Providence, R.I., (1967), 19-32.Google ScholarCross Ref
- Graham S. L. & Wegman M. {1976}, A fast and usually linear algorithm for global flow analysis, JACM 23, 1(1976), 172-202. Google ScholarDigital Library
- Grätzer G. {1971}, Lattice theory, first concepts and distributive lattices, W.H. Freeman and Co., San Francisco, Calif., (1971).Google Scholar
- Grätzer G. & Schmidt E. T. {1958}, Ideals and congruence relations in lattices, Acta Math. Acad. Sci. Hungar., 9(1958), 137-175.Google ScholarCross Ref
- Hoare C. A. R. {1969}, An axiomatic approach to computer programming, CACM 12, 10(Oct. 1969), 576-580,583. Google ScholarDigital Library
- Hoare C. A. R. {1978}, Some properties of predicate transformers, JACM 25, 3(July 1978), 461-480. Google ScholarDigital Library
- Jones N. D. & Muchnick S. S. {1976}, Binding time optimization in programming languages : some thoughts toward the design of an ideal language, Conf. Rec. of the 3rd ACM Symp. on Principles of Programming Languages, Atlanta, GA., (Jan. 1976), 77-91. Google ScholarDigital Library
- Kaplan M. A. & Ullman J. D. {1978}, A general scheme for the automatic inference of variable types, Conf. Rec. of the 5th ACM Symp. on Principles of Programming Languages, Tucson, Ariz., (Jan. 1978), 60-75. Google ScholarDigital Library
- Kam J. B. & Ullman J. D. {1977}, Monotone data flow analysis frameworks, Acta Informatica, 7 (1977), 305-317.Google ScholarDigital Library
- Kildall G. A. {1973}, A unified approach to global program optimization, Conf. Rec. of the ACM Symp. on Principles of Programming Languages, Boston, Mass., (Oct. 1973), 194-206. Google ScholarDigital Library
- Manna Z. {1974}, Mathematical theory of computation, Mc-Graw Hill Book Co., (1974). Google ScholarDigital Library
- Monteiro A. & Ribeiro H. {1942}, L'opéération de fermeture et ses invariants dans les systèmes partiellement ordonnés, Portugal. Math. 3, 171-184.Google Scholar
- Ore O. {1943}, Combination of closure relations, Ann. of Math., 44(1943), 514-533.Google ScholarCross Ref
- Ore O. {1944}, Galois connections, Trans. AMS, 55 (1944), 493-513.Google ScholarCross Ref
- Pickert G. {1952}, Bemerkungen über Galois-verbindungen, Archv. Math. J. 3(1952), 285-289.Google ScholarCross Ref
- Rosen B. {1978}, Monoids for rapid data flow analysis Conf. Rec. of the 5th ACM Symp. on Principles of Programming Languages, Tucson, Ariz.,47-59. Google ScholarDigital Library
- Scott D. {1972}, Continuous lattices, Lect. Notes in Math. 274, Springer Verlag, 97-136.Google Scholar
- Scott D. {1976}, Data types as lattices, SIAM Comp. 5, 3(Sept. 1976), 522-587.Google Scholar
- Shamir A. & Wadge W. W. {1977}, Data types as objects, Lect. Notes in Comp. Sci. 52, Springer Verlag, (1977), 465-479. Google ScholarDigital Library
- Tarjan R. E. {1976}, Iterative algorithms for global analysis, in Algorithms and complexity, new directions and recent results, (J. F. Traub ed.), Acad. Press Inc., (1976), 71-101.Google Scholar
- Tenenbaum A. M. {1974}, Type determination for very high level languages, Rep. NSO-3, Comp. Sci. Dept., N.Y. Univ., (Oct. 1974).Google Scholar
- Ward M. {1942}, The closure operators of a lattice, Annals Math., 43(1942), 191-196.Google ScholarCross Ref
- Wegbreit B. {1975}, Property extraction in well-founded property sets, IEEE Trans. on Soft. Eng., SE-1, 3(Sept. 1975), 270-285.Google Scholar
- Systematic design of program analysis frameworks
Recommendations
Completing Herbelin's programme
TLCA'07: Proceedings of the 8th international conference on Typed lambda calculi and applicationsIn 1994 Herbelin started and partially achieved the programme of showing that, for intuitionistic implicational logic, there is a Curry-Howard interpretation of sequent calculus into a variant of the λ-calculus, specifically a variant which manipulates ...
Conditions Nécessaires d’Optimalité pour un Programme Stochastique avec Recours
Necessary conditions are derived for stochastic programs with locally Lipschitz objective and locally Lipschitz constraints. The problem consists in choosing $x \in X$ so as to satisfy the constraints $x \in F_1 $, $f_{1,i} (x) \leqq 0$, $i \in \langle {1,...
Hypersequential Argumentation Frameworks: An Instantiation in the Modal Logic S5
AAMAS '18: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent SystemsIn this paper we introduce hypersequent-based frameworks for the modeling of defeasible reasoning by means of logic-based argumentation. These frameworks are an extension of sequent-based argumentation frameworks, in which arguments are represented not ...
Comments