Generating the Parser-Pretty-Printer Isomorphism (Correct-by-Construction Proofs of Properties of Domain-Specific Language)

A Domain-Specific Language (DSL) is a small, usually declarative, language expressive over the distinguishing characteristics of a set of programs in a particular problem domain. Often they are used as input to application generators that create program instances possessing the distinguishing characteristics described in input specifications. When reasoning about the correctness of a generated application with respect to some criteria, it quite useful to be able to utilize the logic of the generator (the semantics) to prove that any generated application must satisfy the correctness criteria. This paper describes how classical techniques in language design and formal methods can be utilized in the development of a DSL that meets certain correctness criteria. Specifically, we take a small but real DSL, give it a semantics, and use the logic of the DSL semantics to prove that certain properties are true for any application produced by the generator. Keywords: Application Generators, Dom..