Natural semantics as a static program analysis framework

Natural semantics specifications have become mainstream in the formal specification of programming language semantics during the last ten years. In this paper, we set up sorted natural semantics as a specification framework which is able to express static semantic information of programming languages declaratively in a uniform way and allows at the same time to generate corresponding analyses. Such static semantic information comprises context-sensitive properties which are checked in the semantic analysis phase of compilers as well as further static program analyses such as e.g. classical data and control flow analyses or type and effect systems. The latter require fixed point analyses to determine their solutions. We show that, given a sorted natural semantics specification, we can generate the corresponding analysis. Therefore, we classify the solution of such an analysis by the notion of a proof tree. We show that a proof tree can be computed by solving an equivalent residuation problem. In case of the semantic analysis, this solution can be found by a basic algorithm. We show that its efficiency can be enhanced using solution strategies. We also demonstrate our prototype implementation of the basic algorithm which proves its applicability in practical situations. With the results of this paper, we have established natural semantics as a framework which closes the gap between declarative an