Options
{log}: Set formulas as programs
Cristiá, Massimiliano
Rossi, Gianfranco
2021
Loading...
e-ISSN
2464-8728
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.
Publisher
EUT Edizioni Università di Trieste
Source
Massimiliano Cristiá, Gianfranco Rossi, "{log}: Set formulas as programs" in: "Rendiconti dell’Istituto di Matematica dell’Università di Trieste: an International Journal of Mathematics vol.53 (2021)", EUT Edizioni Università di Trieste, Trieste, 2021. pp.
Languages
en
Rights
Attribution-NonCommercial-NoDerivatives 4.0 Internazionale
File(s)