$\{log\}$: Set Formulas as Programs

TL;DR

The paper introduces $ ext{log}$, a programming language combining set theory and logic, enabling the writing of high-level, verifiable programs that can also serve as formulas for automatic correctness proofs.

Contribution

It presents $ ext{log}$ as a novel language that unifies programming and formal verification using set formulas and logic, demonstrating its development methodology through examples.

Findings

$ ext{log}$ allows writing abstract, specification-like programs.

Programs in $ ext{log}$ can be automatically verified for correctness.

$ ext{log}$ integrates programming and proof within a unified framework.

Abstract

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