The search functionality is under construction.
The search functionality is under construction.

Keyword Search Result

[Keyword] abstract interpretation(3hit)

1-3hit
  • LR Formalisms as Abstract Interpretations of Grammar Semantics

    Seunghwan O  Kwang-Moo CHOE  

     
    PAPER-Automata and Formal Language Theory

      Vol:
    E89-D No:12
      Page(s):
    2924-2932

    The concept of LR(k) validity is represented as an abstract interpretation of a refinement of the derivation semantics of a given grammar. Also the algorithm of LR(k) parsing is represented as an abstract interpretation of the refined semantics. Such representations of LR formalisms provide us with more intuitive and easier means by which to understand LR parsing.

  • Differential Evaluation of Fixpoints of Non-distributive Functions

    Joonseon AHN  

     
    PAPER-Theory and Models of Software

      Vol:
    E86-D No:12
      Page(s):
    2710-2721

    We present a differential fixpoint computation method for program analyses based on abstract interpretation. An analysis of a program based on abstract interpretation can be expressed using a monotonic increasing function and a fixpoint of the function becomes an analysis result. To compute a fixpoint, the function is applied repeatedly until the results become stable. This brings redundant computation because new results always include the former results. Differential methods try to avoid such redundancy by computing only the increment of each function application. Compared with other differential fixpoint evaluation methods, our method can deal with non-distributive functions which often occur in practical program analyses. To compute increments for non-distributive functions, we adapt an indirect way of using a differential evaluation rule for expressions which form function bodies. We have designed a differential worklist algorithm and applied the algorithm to implement an alias and constant propagation analysis. Experiments show that our method can avoid much redundant computation.

  • An Abstraction of Fixpoint Semantics for Normal Logic Programs

    Susumu YAMASAKI  

     
    PAPER-Software Theory

      Vol:
    E79-D No:3
      Page(s):
    196-208

    We deal with a fixpoint semantics for normal logic programs by means of an algebraic manipulation of idempotent substitution sets. Because of the negation, the function associated with a given normal logic program, which captures the deductions caused by the program, is in general nonmonotonic, as long as we are concerned with 2-valued logic approach. The demerit of the nonmonotonic function is not to guarantee its fixpoint well, although the fixpoint is regarded as representing the whole behaviour. The stable model as in [6] is fixpoint of nonmonotonic functions, but it is referred to on the assumption of its existences. On the other hand, if we take 3-valued logic approach for normal logic programs as in [5], [9], [11], [14] we have the monotonic function to represent resolutions and negation as failure, and define its fixpoint well, if we permit the fixpoint not to be constructive because of discontinuity. Since the substituitions for variables in the program are essentially significant in the deductions for logic programming, we next focus on the representations by means of substitutions for the deductions, without usual expressions based on atomic formulas. We examine the semantics in terms of abstract interpretations among semantics as surveyed in [9], where an abstraction stands for the capability of representing another semantics. In this paper, in 3-valued logic approach and by means of the substitution manipulation, the semantics is defined to be an abstraction of the semantics in [5], [9]. To construct a semantics based on the idempotent substitution set, the algebraic manipulation of substitutions is significant, whereas the treatment in [10] for the case of definite clause sets is not available because of the restriction of substitutions to some variable domain as most general unifications.