  $\{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.
