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

翻译：$log ⁇ $是限制逻辑编程、设置编程和宣示编程交叉点的编程语言。 但$log ⁇ $还是有限组合和有限二进制关系理论的可讽刺性解析器。 $log ⁇ $程序员可以使用固定理论和二进制关系的所有力量撰写抽象程序。 这些方案效率不高, 但非常接近规格。 然后, 它们的正确性就更加明显了。 此外, $ ⁇ log ⁇ $ 程序也是设定公式的。 因此, 程序员可以再次使用$ ⁇ log ⁇ $来自动证明其程序的非次要属性。 在本文中, 我们通过几个例子来展示这种开发方法 。