{log}: From a Constraint Logic Programming Language to a Formal Verification Tool
This provides a tool for formal verification in software engineering, offering an integrated approach to programming and proof, but it is incremental as it builds on existing CLP and set theory foundations.
The paper presents {log}, a Constraint Logic Programming language extended into a formal verification environment for state machines, enabling automated verification and test case generation with the same code serving as both program and specification.
{log} (read 'setlog') was born as a Constraint Logic Programming (CLP) language where sets and binary relations are first-class citizens, thus fostering set programming. Internally, {log} is a constraint satisfiability solver implementing decision procedures for several fragments of set theory. Hence, {log} can be used as a declarative, set, logic programming language and as an automated theorem prover for set theory. Over time {log} has been extended with some components integrated to the satisfiability solver thus providing a formal verification environment. In this paper we make a comprehensive presentation of this environment which includes a language for the description of state machines based on set theory, an interactive environment for the execution of functional scenarios over state machines, a generator of verification conditions for state machines, automated verification of state machines, and test case generation. State machines are both, programs and specifications; exactly the same code works as a program and as its specification. In this way, with a few additions, a CLP language turned into a seamlessly integrated programming and automated proof system.