Reliable software construction: a logic programming based methodology

摘要

In this position paper we investigate how logic programming technology can aid software development. The overall goal is to provide a framework for specification and verification that is "computational" in nature rather than being based on traditional, more complex formalisms such as theorem proving and term rewriting. Two approaches are discussed. In the first approach, given a program written in a traditional language (e.g., C), an equivalent logic program is automatically obtained. This equivalent logic program serves as a high level abstraction of the original program and can be put to a number of uses including verification, structured debugging and generation of provably correct target code. The second approach is centered around domain specific languages. Given a task for which a software system is to be developed, a high-level domain specific language (DSL) is first designed. Domain experts can use this DSL for writing programs at their level of abstraction. Logic programming provides a framework in which programs written in this DSL can be interpreted, compiled, debugged, verified, and profiled.