$\{log\}$: Set Formulas as Programs
This work addresses the problem of program correctness and verification for developers in constraint logic and declarative programming, though it is incremental in combining existing paradigms.
The paper introduces $\{log\}$, a programming language and satisfiability solver for finite sets and binary relations, enabling programmers to write abstract programs close to specifications and automatically prove non-trivial properties, as demonstrated through several examples.
$\{log\}$ is a programming language at the intersection of Constraint Logic Programming, set programming and declarative programming. But $\{log\}$ is also a satisfiability solver for a theory of finite sets and finite binary relations. With $\{log\}$ programmers can write abstract programs using all the power of set theory and binary relations. These programs are not very efficient but they are very close to specifications. Then, their correctness is more evident. Furthermore, $\{log\}$ programs are also set formulas. Hence, programmers can use $\{log\}$ again to automatically prove their programs verify non trivial properties. In this paper we show this development methodology by means of several examples.