Thetransformationofconstraintlogicprograms(CLPprograms)hasbeenshowntobean effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program T , and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2017). Program verification using constraint handling rules and array constraint generalizations. FUNDAMENTA INFORMATICAE, 150(1), 73-117 [10.3233/FI-2017-1461].

Program verification using constraint handling rules and array constraint generalizations

PETTOROSSI, ALBERTO;
2017

Abstract

Thetransformationofconstraintlogicprograms(CLPprograms)hasbeenshowntobean effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program T , and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.
Pubblicato
Rilevanza internazionale
Articolo
Esperti anonimi
Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni
English
constraint handling rules; constraint logic programming; program transformation; program verification
De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2017). Program verification using constraint handling rules and array constraint generalizations. FUNDAMENTA INFORMATICAE, 150(1), 73-117 [10.3233/FI-2017-1461].
De Angelis, E; Fioravanti, F; Pettorossi, A; Proietti, M
Articolo su rivista
File in questo prodotto:
File Dimensione Formato  
2015_DFPP_IASI-08 (1).pdf

accesso aperto

Descrizione: Articolo principale
Licenza: Non specificato
Dimensione 1.09 MB
Formato Adobe PDF
1.09 MB Adobe PDF Visualizza/Apri

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: http://hdl.handle.net/2108/184691
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 1
social impact