A Formal Specification of a Programming Language: Design of Pit

Formal specifications and supporting tools have shown to be very effective to improve the quality and correctness of a software system. A compiler is large and complex software; it takes as input a program written in some language and generates as output a program in another language. One of the main characteristics of any compiler is to preserve the semantics of the program being compiled. Therefore, developing correct compilers that can generate faithful target code without introducing any errors is critically important. In this paper, we show how to use Z notation to formally specify part of the Pit, which is a general-purpose programming language that we are currently developing. The main idea behind Pit is to create a language where the programmer can choose between allocating memory manually by using static ally-typed "primitive" variables or allowing the compiler to insert memory management code automatically by using dynamically-typed "auto" variables. This feature, in turn, allows a programmer to choose between automatically ensuring that there are no buffer overrun or integer overflow vulnerabilities in the code.