%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Relazione scientifica sulla ricerca svolta
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Il lavoro svolto dall'Unità di Parma può articolarsi
nei seguenti due punti:
(1) Analisi di linguaggi logici (con vincoli).
(2) Definizione di linguaggi con vincoli insiemistici e loro impiego
nell'analisi di programmi basata su insiemi.
Per quanto riguarda il punto (1), ci si è concentrati sulla
definizione e dimostrazione di correttezza di domini di analisi atti a
caratterizzare alcune proprietà di sicurezza dei programmi logici,
come la finitezza dei termini elaborati (occur-check reduction e
finite-tree analysis). Questa proprietà è un prerequisito
essenziale quando si vogliono integrare analisi statiche progettate
per domini di alberi finiti all'interno di implementazioni di sistemi
logici che di fatto calcolano su domini di alberi razionali
potenzialmente infiniti, pervenendo quindi ad una vera e propria
certificazione del programma (oppure identificando i punti in cui si
ha un potenziale problema di correttezza e/o sicurezza). Questo
problema è particolarmente sentito nel caso di agenti mobili scritti
in un linguaggio logico (fase 1 del progetto). La progettazione di
una estensione dell'analizzatore China in grado di operare in modo
incrementale e modulare (fase 2 del progetto) è tuttora in corso.
Molta attenzione è stata posta al miglioramento ed alla valutazione
sperimentale della precisione dell'analisi (fasi 1 e 3 del progetto).
- Finite-tree analysis.
L'analisi di finitezza dei termini, introdotta in [C4,RT5], è un
nuovo tipo di analisi statica che ha l'obiettivo di determinare a
tempo di compilazione se un dato termine razionale è sicuramente
finito. Questa analisi rappresenta una generalizzazione dell'analisi
di occur-check ed è applicabile in tutti i casi in cui il programma
considerato effettua, intenzionalmente ed in modo controllato,
computazioni su alberi razionali potenzialmente infiniti. Come per il
caso dell'occur-check reduction, la correttezza, la precisione e
l'efficienza della finite-tree analysis dipendono essenzialmente dalle
corrispondenti proprietà dell'analisi di sharing, che ne è una delle
componenti principali.
- Analisi di sharing.
Uno degli obiettivi dell'analisi di sharing per i programmi logici è
quello di determinare quali coppie di variabili possono condividere
una terza variabile. Il dominio Sharing (Jacobs e Langen, 1989) è
una scelta pressoché standard per questo tipo di analisi e per
ulteriori studi teorici. A dispetto di ciò si è riscontrato che non
esistevano dimostrazioni soddisfacenti delle proprietà chiave,
commutatività ed idempotenza, che rendono Sharing ben
definito. Inoltre, le prove o congetture pubblicate circa la
correttezza dell'analisi basata su questo dominio presumono che il
linguaggio analizzato implementi l'unificazione con l'occur-check,
cosa che è falsa nella quasi totalità dei casi. Il lavoro [R4]
chiude queste falle, rimaste aperte per quasi un decennio. La
complementazione, e cioè l'operazione inversa del prodotto ridotto,
rappresenta una tecnica relativamente nuova per la determinazione
automatica di decomposizioni minimali dei domini astratti. In [R5]
mostriamo la decomposizione per complementazione della versione non
ridondante di Sharing, denotata PSD, dando sostanza all'affermazione
che la complementazione, da sola, non è sufficiente per ottenere
decomposizioni veramente minimali: la giusta soluzione a questo
problema consiste prima nella rimozione delle ridondanze attraverso il
calcolo del quoziente del dominio rispetto al comportamento
osservabile, e poi nella decomposizione per complementazione.
- Miglioramenti della precisione delle analisi.
Relativamente alla precisione delle analisi basate su combinazioni di
domini che includono il dominio Sharing, esiste un piccolo nucleo di
tecniche, quali la combinazione standard con informazioni di
linearità e di freeness, che sono oramai ampiamente accettate ed
utilizzate. Esistono però diverse altre proposte che sono circolate
nella comunità scientifica per anni, accomunate dal fatto che nessuna
di esse sembra essere stata sottoposta ad una adeguata validazione
sperimentale. Per questa ragione, come parte del nostro sforzo per
spingere la precisione dell'analisi oltre i limiti attuali, in [C1,S1]
ci siamo posti il problema di verificare se e quanto dette proposte
possono contribuire ad un effettivo miglioramento della precisione. In
particolare abbiamo discusso e/o valutato sperimentalmente utilizzando
l'analizzatore China le seguenti possibilità: l'effetto della
propagazione su Sharing delle variabili ground identificate da Pos;
l'incorporazione di informazione strutturale esplicita nel dominio di
analisi; tecniche più sofisticate per integrare Sharing e Pos; la
questione del riordinamento dei binding nel calcolo dell'mgu astratto;
una proposta originale concernente l'aggiunta di informazioni
sull'insieme di variabili che sono ground o free; tecniche più
precise per l'integrazione delle informazioni di linearità e di
freeness; la possibilità di migliorare la precisione dell'analisi
mantenendo informazioni sulla compoundness delle variabili.
In [C2,RT3] abbiamo presentato la costruzione razionale di un dominio
generico con informazione strutturale per l'analisi di programmi CLP.
Il dominio proposto, Pattern(D), ha come parametro un qualsiasi
dominio astratto D, che deve soddisfare alcuni requisiti assolutamente
ragionevoli. La nostra definizione del dominio suddetto prende
ispirazione da un analogo dominio parametrico per l'analisi di
programmi logici introdotto da A. Cortesi e colleghi. D'altra parte,
la nostra formalizzazione, oltre ad applicarsi all'analisi di un
qualunque linguaggio CLP, è indipendente dalla tecnica di
implementazione: il dominio di Cortesi, opportunamente esteso per
trattare correttamente i linguaggi CLP che omettono l'occur-check
nella procedura di unificazione, è una delle possibili
implementazioni. Ragionando ad un più alto livello di astrazione
siamo in grado di riferirci a nozioni classiche della teoria
dell'unificazione e di consentire all'implementatore una notevole
libertà d'azione. Infatti, come dimostriamo in [C2,RT3], un
analizzatore che incorpori informazione strutturale basandosi sul
nostro approccio può essere estremamente competitivo, sia dal punto
di vista della precisione (cosa largamente scontata) sia dal punto di
vista dell'efficienza (cosa non scontata ed in contrasto con alcune
considerazioni, non supportate da sperimentazioni, recentemente
apparse in letteratura).
Allo scopo di aumentare la precisione della finite-tree analysis, in
[C5,RT6] abbiamo studiato l'integrazione del dominio proposto in
[C4,RT5] con il dominio Bfun delle le funzioni booleane definite sulle
variabili del programma. In questo modo è possibile catturare le
dipendenze di finitezza tra le variabili stesse, in particolare
rendendo possibile una più accurata approssimazione dei built-in. La
novità di questa analisi, rispetto all'analoga analisi delle
dipendenze di groundness basata sui domini Pos e Def, consiste nella
possibilità di sfruttare adeguatamente anche l'informazione fornita
dalle funzioni booleane negative. In [C5,RT6] sono anche mostrate le
interconnessioni esistenti tra le dipendenze di groundness (Pos), le
dipendenze di finitezza (BFun) e la proprietà di finitezza
caratterizzata in [C4,RT5], dimostrando come ed in che misura i tre
tipi di informazione possono interagire durante l'analisi. Da una
prima valutazione sperimentale con China è possibile notare come i risultati
della finite-tree analysis, sebbene già caratterizzati da un buon
livello di precisione, sono sensibilmente migliorati grazie al dominio
delle dipendenze di finitezza.
Sempre mirando ad un aumento della precisione delle varie analisi, si
è provveduto a sviluppare una libreria per la manipolazione di
poliedri convessi [A3]. Il dominio dei poliedri convessi è utilizzato
in moltissime applicazioni dell'analisi statica (non solo per i
linguaggi logici, ma anzi principalmente per i linguaggi imperativi),
tra le quali spiccano le analisi per identificare eventuali problemi
di sicurezza causati dai buffer-overflow delle applicazioni di rete:
è stato calcolato che essi costituiscono più del 50% di tutti gli
attacchi informatici via rete. La libreria è già utilizzata
all'interno dell'analizzatore China.
Per quanto riguarda il punto (2) del lavoro svolto dall'Unità di
Parma ci si è in particolare concentrati sugli obiettivi: (a) di
migliorare ed estendere la definizione e l'implementazione del
linguaggio logico a vincoli con insiemi CLP(SET) (fasi 1 e 2); (b) di
analizzare come le possibilità specifiche presenti in questo
linguaggio possano essere vantaggiosamente impiegate nell'analisi di
programmi basata su insiemi (fasi 2 e 3).
(a) Le precedenti versioni di CLP(SET) sono state opportunamente
estese con l'aggiunta di nuovi vincoli insiemistici (operazioni di
unione e di non-intersezione) ed il conseguente ampliamento delle
procedure per il controllo di soddisfacibilità dei vincoli. La
disponibilità di queste operazioni come vincoli primitivi del
linguaggio è indispensabile per l'utilizzo del linguaggio di vincoli
insiemistici per l'analisi di programmi basata su insiemi. Di
fondamentale importanza, in particolare, è l'operazione di
unificazione insiemistica, studiata approfonditamente in [S2]. La
nuova versione del linguaggio CLP(SET) è descritta per esteso in [R1].
Un altro aspetto che si è ritenuto importante analizzare -- anche se
non esplicitamente previsto nella proposta originaria -- riguarda il
trattamento della negazione nel linguaggio CLP(SET) e la stretta
connessione tra questa e la possibilità di fornire definizioni
intensionali (e cioè per proprietà) degli insiemi. La disponibilità
di queste forme di astrazione insiemistica si dimostra infatti di
fondamentale importanza per permettere un uso più ampio del
linguaggio di vincoli insiemistici nell'analisi di programmi basata su
insiemi. In [R2] viene fornita un'analisi approfondita delle
problematiche relative all'aggiunta della negazione (ed in particolare
della Negazione Costruttiva) al linguaggio CLP(SET), e quindi viene
presentata una possibile soluzione per il trattamento di insiemi
intensionali. In [R3] viene evidenziato però un risultato negativo in
cui si mostra come la Negazione Costruttiva non sia in grado di
funzionare correttamente con qualsiasi programma CLP(SET) e, più in
generale, con qualsiasi linguaggio CLP basato su una struttura non
decidibile. Un altro importante arricchimento del linguaggio di
vincoli insiemistici che si è analizzato (vedi [RT1][RT4][S3])
riguarda l'introduzione di altre forme di aggregato, quali i
multi-insiemi e le liste. A differenza degli insiemi, queste
astrazioni permettono di tener conto dell'ordine e della molteplicità
degli elementi nell'aggregato. Considerazioni e proposte sull'utilizzo
dei multi-insiemi nel contesto di un linguaggio CLP sono presentate in
[R6] e [C3].
(b) Parallelamente alla realizzazione ed ampliamento di CLP(SET) si è
approfondito lo studio relativo all'utilizzo del linguaggio di vincoli
insiemistici fornito da CLP(SET) per l'analisi di programmi basata su
insiemi ("set-based analysis"), senza tuttavia arrivare ad una
completa pubblicazione dei risultati ottenuti. In particolare si è
potuto verificare come il nostro linguaggio di vincoli insiemistici
costituisca una valida alternativa ai linguaggi di set-constraints
considerati in letteratura e tuttora frequentemente impiegati nel
campo dell'analisi di programmi (si veda a proposito, ad esempio,
l'articolo di A. Aiken "Introduction to Set Constraint-Based Program
Analysis"). Se, da una parte, CLP(SET) non è in grado di trattare
adeguatamente i vincoli su insiemi infiniti gestibili invece con i
set-constraints, dall'altra, la possibilità di annidamento di
insiemi, la presenza di un'operazione di appartenenza insiemistica, la
possibilità di trattare insiemi intensionali, nonché quella di
estendere il dominio del discorso ad altre forme di aggregati, quali i
multi-insiemi, rende il linguaggio a vincoli insiemistici di CLP(SET)
un interessante strumento per la realizzazione di forme di "set-based
analysis" possibilmente più generali e flessibili di quelle
attualmente descritte in letteratura. A scopo d'esempio si è
verificato l'utilizzo di una tecnica di analisi di programmi basata su
CLP(SET) sul problema dell'analisi di groundness di programmi logici,
concludendo che la maggior flessibilità e potenza espressiva di
CLP(SET) rispetto ai linguaggi di set-constraints solitamente usati in
letteratura permettono di risolvere facilmente problemi non risolti
con quest'ultimi (in particolare l'interdipendenza tra le variabili).
I risultati preliminari ottenuti su queste specifiche tematiche sono
documentati dai lavori [A1] e [A2]. Esempi di analisi di semplici
programmi Prolog con i relativi vincoli insiemistici CLP(SET) prodotti
e le definizioni CLP(SET) aggiuntive atte alle loro verifica sono
disponibili qui.
Questi programmi CLP(SET) possono vedersi come un primo prototipo
degli strumenti di analisi di programmi basata sulle tecniche da noi
sviluppate e che costituivano uno degli obiettivi del progetto.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Pubblicazioni
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
In riviste internazionali
[R1] A. Dovier, C. Piazza, E. Pontelli, and G. Rossi.
Sets and Constraint Logic Programming.
ACM Transaction on Programming Language and Systems,
Vol. 22 (5), Sept. 2000, 861-931.
[R2] A. Dovier, E. Pontelli, and G. Rossi.
Constructive negation and constraint logic programming with sets.
New Generation Computing, Springer Verlag and Ohmsha Ltd,
19(3)209--255, May 2001.
[R3] A. Dovier, E. Pontelli, and G. Rossi.
A Necessary Condition for Constructive Negation in Constraint Logic
Programming. Information Processing Letters, Vol. 74 (3-4) (2000),
Elsevier, North Holland, 147-156.
[R4] P. M. Hill, R. Bagnara, E. Zaffanella.
Soundness, idempotence and commutativity of set-sharing.
To appear in Theory and Practice of Logic Programming.
[R5] E. Zaffanella, P. M. Hill, R. Bagnara.
Decomposing non-redundant sharing by complementation.
To appear in Theory and Practice of Logic Programming.
[R6] A. Dovier, C. Piazza, and G. Rossi.
Multiset rewriting by multiset constraint solving
Romanian Journal of Information Science and Technology,
Vol. 4(1--2):59--76, 2001.
In atti di Conferenze internazionali
[C1] R. Bagnara, E. Zaffanella, P. M. Hill.
Enhanced sharing analysis techniques: A comprehensive evaluation.
In Proc. 2nd Int. ACM SIGPLAN Conf. on Principles and Practice of
Declarative Programming (PPDP 2000) (Montreal, Canada, 2000),
M. Gabbrielli and F. Pfenning, Eds., ACM, 103-114.
[C2] R. Bagnara, P. M. Hill, E. Zaffanella.
Efficient structural information analysis for real CLP languages.
In Proc. 7th Int. Conf. on Logic for Programming and Automated Reasoning
(LPAR 2000) (Reunion Island, France, 2000), M. Parigot and A. Voronkov, Eds.,
vol. 1955 of LNCS, Springer-Verlag, Berlin, 189-206.
[C3] A. Dovier, C. Piazza, and G. Rossi. Multiset Constraints and P Systems.
To appear in: Multisets Processing (C.S. Calude, Gh. Paun,
G. Rozenberg, A. Salomaa, eds.), Lecture Notes in Computer Science,
Springer Verlag.
[C4] R. Bagnara, R. Gori, P. M. Hill ed E. Zaffanella.
Finite-Tree Analysis for Constraint Logic-Based Languages.
In Proc. of the 8th Int. Symp. on Static Analysis
(SAS 2001) (Paris, France, July 2001), vol. 2126 of LNCS,
P. Cousot, Ed., pp. 165-184.
[C5] R. Bagnara, E. Zaffanella, R. Gori e P. M. Hill.
Boolean Functions for Finite-Tree Dependencies.
In Proc. of the 8th Int. Conf. on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR 2001) (Havana, Cuba, December 2001),
vol. 2250 of LNCS, R. Nieuwenhuis and A. Voronkov, Eds., pp. 575-589
Rapporti Tecnici
[RT1] A. Dovier, C. Piazza, and G. Rossi.
A uniform approach to constraint-solving for lists, multisets,
compact lists, and sets.
Rapporto di Ricerca, Dipartimento di Matematica, Università di Parma, n.235,
September 2000.
[RT2] G. Rossi.
{log} User's Manual - Version 3.3.
Rapporto di Ricerca, Dipartimento di Matematica, Università di Parma, n.233,
September 2000.
[RT3] R. Bagnara, P. M. Hill, E. Zaffanella.
Efficient structural information analysis for real CLP languages.
Quaderno 229, Dipartimento di Matematica, Università di Parma, 2000.
[RT4] A. Dovier, C. Piazza, and G. Rossi.
A uniform approach to constraint-solving for
lists, multisets, compact lists, and sets
In Pre-Proceedings of the Workshop on Multiset
Processing WMP2000 (C.S.Calude, M.J.Dinnen, Gh.Paun, eds),
Curtea de Arges (Romania), Research Report CDMTCS-140, Centre
for Discrete Mathematics and Theoretical Computer Science,
University of Auckland, New Zealand, Agosto 2000.
[RT5] R. Bagnara, R. Gori, P. M. Hill ed E. Zaffanella.
Finite-Tree Analysis for Constraint Logic-Based Languages.
Quaderno 251, Dipartimento di Matematica, Università di Parma, 2001.
[RT6] R. Bagnara, E. Zaffanella, R. Gori e P. M. Hill.
Boolean Functions for Finite-Tree Dependencies.
Quaderno 252, Dipartimento di Matematica, Università di Parma, 2001.
Sottomessi
[S1] R. Bagnara, E. Zaffanella, P. M. Hill.
Enhanced Sharing Analysis Techniques: a Comprehensive Evaluation.
Submitted to Theory and Practice of Logic Programming.
[S2] A. Dovier, E. Pontelli, and G. Rossi.
Set Unification. versione sottomessa.
[S3] A. Dovier, C. Piazza, and G. Rossi.
A uniform approach to constraint-solving for lists, multisets,
compact lists, and sets. versione sottomessa.
Altre
[A1] A. Dovier, C. Piazza, and G. Rossi. Set-based constraints
In preparazione.
Versione preliminare ("draft")
[A2] A. Morini.
Una proposta per l'analisi di "groundness" di programmi logici basata su insiemi (in Italian),
Tesi di Laurea, Dipartimento di Matematica, Università di Parma, Ottobre 2000.
[A3] R. Bagnara, S. Bonini, P. M. Hill, A. Pescetti, E. Ricci,
A. Stazzone, E. Zaffanella, T. Zolo.
The Parma Polyhedra Library User's Manual
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Prodotti software sviluppati
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
L'attività svolta ha portato alle seguenti realizzazioni:
1) Ampliamento e miglioramento di China, un analizzatore per linguaggi
logici con vincoli scritto in C++ da R. Bagnara e E. Zaffanella. Tutti
i domini di analisi studiati sono stati implementati ed integrati in
China. Per la valutazione sperimentale dell'analizzatore si è
provveduto alla ricerca e raccolta sistematica dei programmi logici
disponibili sulla rete Internet. In questo modo è stata costituita
una estesa "benchmark suite" che garantisce la significatività
della sperimentazione stessa.
2) Parma Polyhedra Library: libreria C++ per la
manipolazione di poliedri convessi (vedere Appendice A).
3) Ampliamento e miglioramento di CLP(SET), un linguaggio logico con
vincoli insiemistici [R1]. L'interprete del linguaggio, scritto in
SICStus Prolog, è disponibile qui (vedere Appendice B).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Altre attività
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Partecipazione a conferenze/workshop/scuole
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Workshop on Multiset Processing (WMP), Curtea de Arges, Romania
Agosto 2000 (G. Rossi).
- 2nd Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative
Programming, Montreal (Canada), Settembre 2000 (R. Bagnara e E. Zaffanella).
- 7th Int. Conf. on Logic for Programming and Automated Reasoning (LPAR
2000), Reunion Island (Francia), Novembre 2000 (R. Bagnara).
- POPL01 - Principles of Programming Languages, Londra, Gennaio 2001 (G. Rossi).
- European Joint Conferences on Theory and Practice of Software (ETAPS 2001),
Genova, Italia, Aprile 2001 (E. Zaffanella).
- 8th International Static Analysis Symposium (SAS 2001), Paris, France,
Luglio 2001 (R. Bagnara e E. Zaffanella).
- 2001 Joint Conference on Declarative Programming (APPIA-GULP-PRODE 2001),
Evora, Portugal, Settembre 2001 (R. Bagnara).
Seminari
^^^^^^^^
- Seminario su "Efficient Structural Information Analysis
for Real CLP Languages", tenuto da R. Bagnara presso la
Facultad de Informatica, Universidad Politecnica di Madrid,
gennaio 2001.
- Seminario su "Widening Sharing", tenuto da R. Bagnara presso la
Facultad de Informatica, Universidad Politecnica di Madrid,
gennaio 2001.
- Seminario su "Correctness, Precision and Efficiency in the Sharing
Analysis of Real Logic Languages", tenuto da E. Zaffanella
presso il Dipartimento di Informatica dell'Università di Pisa,
novembre 2001.
Materiale inventariabile acquisito nell'ambito del progetto
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 2 PC HIBIT Biostar M7MKA con processore AMD K7 Athlon 700MHz,
memoria RAM da 256 MByte, HD da 20 GByte e Monitor 17''
- 1 Modem V.90 K56Flex
- 1 Masterizzatore WAITEC "TITAN"
- 1 Masterizzatore SONY CRX1611-82E
- 3 Banchi DIMM PC133 da 512MB
- Libri.
Personale a contratto
^^^^^^^^^^^^^^^^^^^^^
È stato stipulato un contratto per prestazione occasionale della durata di
3 mesi con la Dott.ssa Angela Stazzone (vedere Allegato C).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Appendici
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Appendice A - Parma Polyhedra Library
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
La "Parma Polyhedra Library" (PPL) è una libreria C++ per la
manipolazione di poliedri convessi. Più precisamente, PPL tratta
poliedri convessi che possono essere definiti come intersezione di un
numero finito di iperspazi chiusi, ognuno descritto da un uguaglianza
o disuguaglianza a coefficienti razionali.
La libreria PPL usa la rappresentazione della doppia descrizione
introdotta da T. S. Motzkin e colleghi: la descrizione basata
sull'intersezione di iperspazi è accompagnata da una descrizione
basata sull'enumerazione dei vertici e dei raggi estremali del
poliedro. In altre parole, nella prima descrizione il poliedro è
descritto da un insieme finito di vincoli; nella seconda descrizione,
il poliedro è descritto da un insieme finito di generatori. Alcune
operazioni sui poliedri si possono eseguire più convenientemente sulla
prima rappresentazione. Ad esempio, l'intersezione di due poliedri
può essere caratterizzata dall'unione dei rispettivi insiemi di
vincoli. Il calcolo dell'inviluppo convesso di due poliedri, invece,
può essere facilmente visto come l'unione dei rispettivi insiemi di
generatori.
La libreria PPL esegue, automaticamente ed in modo totalmente trasparente
all'utilizzatore, le conversioni da una rappresentazione all'altra.
Le conversioni vengono posposte quanto più possibile; quando queste
non possono essere ulteriormente dilazionate, le conversioni vengono
effettuate in modo da massimizzarne il beneficio (ad esempio, alcuni
risultati intermedi vengono salvati in modo da poter essere riutilizzati
nelle computazioni successive).
Per eseguire le conversioni, la libreria usa un algoritmo originariamente
proposto da T. S. Motzkin e colleghi, poi riscoperto e migliorato da
N. V. Chernikova, H. Le Verge, D. K. Wilde, K. Fukuda, A. Prodon,
N. Halbwachs, Y.-E. Proy, P. Roumanoff e B. Jeannet.
La libreria include anche algoritmi di widening derivati da quelli
di N. Halbwachs e P. Cousot.
Alcune caratteristiche peculiari della Parma Polyhedra Library sono:
- facilità d'uso: sfruttando i meccanismi di overloading degli operatori
del C++ un vincolo può essere scritto, ad esempio, `x + 2*y + 5*z <= 7';
- totale dinamicità: la disponibilità di memoria virtuale è l'unica
limitazione alla dimensione di ogni oggetto;
- scritta in C++ standard, e dunque portabile, ma interfacciabile
con altri linguaggi (un'interfaccia per Prolog è già disponibile);
- sicura rispetto alle eccezioni: anche nel caso in cui venga superato
il limite di memoria virtuale disponibile, non vengono sprecate risorse
né si lasciano in esistenza oggetti invalidi (questo supporta tecniche
di analisi miste: si tenta l'analisi poliedrale e si ripiega su un'analisi
basata su intervalli nel caso di risorse insufficienti);
- piuttosto efficiente: grazie a tecniche implementative (alcune esposte sopra)
particolarmente sofisticate;
- interamente documentata: nello stile noto come "literate programming"
(ad esempio, tutta la matematica necessaria a giustificare il funzionamento
della libreria è parte della documentazione);
- software libero: distribuito nei termini della "GNU General Public License"
(e dunque liberamente disponibile, in perpetuo, a chiunque voglia usarla,
studiarla e modificarla).
Appendice B - Interprete per il linguaggio CLP(SET)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
CLP(SET) è un linguaggio logico a vincoli che fornisce varie forme
generali e flessibili di costrutti insiemistici con le relative
operazioni di base per la loro manipolazione. Gli insiemi in CLP(SET)
sono visti come oggetti primitivi del linguaggio, precisamente termini
della logica del prim'ordine, mentre tutti i predicati predefiniti che
hanno a che fare con insiemi sono visti come vincoli ("constraint")
primitivi del linguaggio. Il linguaggio CLP(SET) descritto in [R1]
rappresenta un'evoluzione e revisione in termini di una visione CLP
("Constraint Logic Programming") del linguaggio logico esteso {log}
descritto in A.Dovier, E.Omodeo, E.Pontelli, G.Rossi. "{log}: A
Language for Programming in Logic with Finite Sets", Journal of Logic
Programming, Vol.28(1).
Nell'ambito di questo progetto è stato portata a termine
l'implementazione di un interprete per l'intero linguaggio descritto
in [R1], comprensivo dei constraint di unione e di
disgiunzione. L'interprete è implementato in SICStus Prolog ed è
disponibile al sito WEB www.math.unipr.it/~gianfr/setlog.Home.html.
A questa stessa pagina è anche disponibile altro materiale di ausilio
all'utilizzo del linguaggio CLP(SET), e precisamente:
- il manuale utente del linguaggio (disponibile anche come [RT2]);
- un file contenente la definizione CLP(SET) di varie operazioni
insiemistiche di base non fornite come constraint primitivi dal
linguaggio, ma facilmente definibili in termini di questi;
- vari file contenenti esempi di programmi CLP(SET) funzionanti.
L'interprete di CLP(SET) è scritto in SICStus Prolog e quindi per
poterlo eseguire è richiesta la disponibilità di interprete SICStus
Prolog. In realtà l'interprete di CLP(SET) utilizza pochissime
possibilità specifiche del SICStus Prolog e quindi può essere fatto
funzionare con poco sforzo su qualsiasi altro sistema Prolog.
Appendice C - Contratto Dott.ssa Angela Stazzone
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Lavoro svolto (in breve):
1) studio del formato rpm (Red Hat Package Manager) e
realizzazione di una distribuzione, in tale formato,
dell'analizzatore statico China;
2) raffinamento dell'implementazione (in C++) di un occurs-check
reducer accoppiato al suddetto analizzatore;
3) raffinamento, auditing e documentazione di alcune parti
della Parma Polyhedra Library.
Lavoro svolto (per esteso):
1) Red Hat Package Manager
Red Hat Package Manager (RPM) è un sistema per la gestione di
pacchetti software che ne facilita enormemente la distribuzione e
l'installazione. Questo sistema gestisce un data-base di tutti i
pacchetti installati e dei rispettivi file, in modo da poter
automatizzare l'installazione, la disinstallazione e la verifica di
integrità di ogni pacchetto.
China è un analizzatore data-flow/control-flow per programmi logici
con vincoli su domini simbolici e numerici. Utilizzando Red Hat
Package Manager, è stata creata una versione RPM dell'analizzatore
China che può quindi essere distribuito ed installato anche da persone
non esperte.
2) Occurs-Check Reducer
È stato raffinato un "occurs-check reducer" (OCR), in grado di
eseguire, in modo automatico, un numero minimale di modifiche su un
programma logico sufficienti ad assicurarne la correttezza. L'OCR,
interagendo con l'analizzatore statico China, controlla tutte le
unificazioni (implicite ed esplicite) presenti in un programma ed
eventualmente le trasforma in unificazioni con occurs-check. La regola
generale prevede di lasciare inalterate le unificazioni non soggette
al problema dell'occurs-check e di trasformare quelle potenzialmente
pericolose in unificazioni con occurs-check. Questo tipo di controllo
riguarda anche alcuni built-in che, implicitamente o esplicitamente,
effettuano unificazioni.
3) Parma Polyhedra Library
La documentazione della PPL è stata estesa e migliorata; le principali
funzionalità della libreria sono state illustrate nel modo più chiaro
possibile, facendo riferimento ai risultati utilizzati durante
l'implementazione ed eventualmente fornendone la dimostrazione.