Executable Computational Logics: Combining Formal Methods and Programming Language Based System Design
José Meseguer · 2008
An executable computational logic can provide the desired bridge between formal system properties and formal methods to verify them on the one hand, and executable models of system designs based on programming languages on the other. However, not all such logics are equally well suited for the task. This paper gives some requirements that seem important for a computational logic to be suitable in practice, and discusses the experience with rewriting logic, its Maude language implementation, and its formal tool environment, concluding that they seem to meet well those requirements. 1. The General Idea The present conference explores a convergence of formal methods and programming language based approaches to system design in both hardware and embedded hardwaresoftware systems. There are many practical benefits to be gained from such a convergence and, furthermore, there are important research issues involved. I wish to put forward a simple general idea that in my view provides a conceptual key to exploring a convergence of this kind. As suggested in the title, the idea is that an executable computational logic can provide the desired bridge between formal system properties and formal methods to verify them on the one hand, and executable models of system designs based on programming languages on the other. The general idea as such is hardly new: it has already been demonstrated very successfully by different researchers using different computational logics. There are