Please use this identifier to cite or link to this item: http://hdl.handle.net/10077/33309
Title: {log}: Set formulas as programs
Authors: Cristiá, Massimiliano
Rossi, Gianfranco
Keywords: set theorydeclarative programmingset programmingformal verification{log}
Issue Date: 2021
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.
Journal: Rendiconti dell’Istituto di Matematica dell’Università di Trieste: an International Journal of Mathematics 
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.
Type: Article
URI: http://hdl.handle.net/10077/33309
ISSN: 0049-4704
eISSN: 2464-8728
DOI: 10.13137/2464-8728/33309
Rights: Attribution-NonCommercial-NoDerivatives 4.0 Internazionale
Appears in Collections:Rendiconti dell’Istituto di Matematica dell’Università di Trieste: an International Journal of Mathematics vol.53 (2021)

Files in This Item:
File Description SizeFormat
23_CristiaRossi.pdf433.81 kBAdobe PDFThumbnail
View/Open
Show full item record


CORE Recommender

Page view(s)

55
checked on May 21, 2022

Download(s)

3
checked on May 21, 2022

Google ScholarTM

Check

Altmetric

Altmetric


This item is licensed under a Creative Commons License Creative Commons