CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishIn this paper we present a decision procedure for Restricted Intensional Sets (RIS), i.e. sets given by a property rather than by enumerating their elements, similar to set comprehensions available in specification languages such as B and Z. The proposed procedure is parametric with respect to a first-order language and theory X, providing at least equality and a decision procedure to check for satisfiability of X -formulas. We show how this framework can be applied when X is the theory of hereditarily finite sets as is supported by the language CLP(SET). We also present a working implementation of RIS as part of the log tool and we show how it compares with a mainstream solver and how it helps in the automatic verification of code fragments.
A decision procedure for restricted intensional sets / Cristià, Maximiliano; Rossi, Gianfranco. - STAMPA. - 10395(2017), pp. 186-201. [10.1007/978-3-319-63046-5_12]
| Titolo: | A decision procedure for restricted intensional sets | |
| Autori: | ||
| Data di pubblicazione: | 2017 | |
| Serie: | ||
| Citazione: | A decision procedure for restricted intensional sets / Cristià, Maximiliano; Rossi, Gianfranco. - STAMPA. - 10395(2017), pp. 186-201. [10.1007/978-3-319-63046-5_12] | |
| Handle: | http://hdl.handle.net/11381/2832956 | |
| ISBN: | 9783319630458 | |
| Appare nelle tipologie: | 2.1 Contributo in volume (Capitolo di libro) |
File in questo prodotto:
http://hdl.handle.net/11381/2832956
Copyright © 2022