In 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]

A decision procedure for restricted intensional sets

ROSSI, Gianfranco
2017-01-01

Abstract

In 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.
2017
9783319630458
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]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2832956
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 9
social impact