Il lavoro svolto dall'Unità di Parma può articolarsi nei seguenti due punti:
Per quanto riguarda il punto (1) ci si è in particolare concentrati sulla definizione e implementazione di un linguaggio logico, denominato CLP(SET), che permetta la definizione di insiemi e la loro manipolazione tramite le usuali operazioni insiemistiche di base.
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. La nuova versione del linguaggio CLP(SET) è descritta per esteso in [1].
Un altro aspetto che si è ritenuto importante analizzare per permettere un uso più ampio del linguaggio di vincoli insiemistici nell'analisi di programmi basata su insiemi è quello relativo alla presenza della negazione. Questo aspetto risulta, tra l'altro, strettamente connesso con la possibilita' di fornire definizioni intensionali (e cioè per proprietà) degli insiemi in CLP(SET), la cui disponibilità arricchisce notevolmente il potere espressivo del linguaggio. In [2] 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 il trattamento di insiemi intensionali. In [3} 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 [4]) 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.
Parallelamente alla realizzazione ed ampliamento di CLP(SET) si è iniziato ad indagare l'utilizzo del linguaggio di vincoli insiemistici fornito da CLP(SET) per l'analisi di programmi basata su insiemi ("set-based analysis"). Per il momento ci si è concentrati sul problema dell'analisi di groundness di programmi logici allo scopo di valutare l'adeguatezza della tecnica proposta. I risultati preliminari indicano che la maggior flessibilità e potenza espressiva di CLP(SET) rispetto ai linguaggi di vincoli insiemistici solitamente usati in letteratura permettono di risolvere problemi non risolti da quest'ultimi (quali l'interdipendenza tra le variabili).
Per quanto riguarda il punto (2) ci si è concentrati sulla definizione, dimostrazione di correttezza, implementazione e valutazione sperimentale di alcuni domini astratti per l'analisi statica.
L'obiettivo dell'analisi di sharing per programmi logici è quello di determinare quali coppie di variabili possono condividere una terza variabile. Tra le applicazioni di questa analisi è compresa la occur-check reduction, che garantisce l'assenza di una importante classe di errori a tempo di esecuzione. 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 [6] chiude queste falle, rimaste aperte per quasi un decennio. In particolare, viene data una generalizzazione della funzione di astrazione di Sharing che può essere applicata ad ogni linguaggio, con o senza l'occur-check. Oltre a questo, vengono dimostrati i risultati di correttezza, idempotenza e commutatività per l'operazione di unificazione astratta.
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. Filé e Ranzato hanno introdotto un metodo semplificato per il calcolo del complemento e, come applicazione, hanno considerato l'estrazione per complementazione del dominio di pair-sharing (PS) dal dominio di Sharing di Jacobs e Langen, basato sul set-sharing. Dal momento che il risultato di questa operazione è lo stesso Sharing, gli autori ne hanno concluso che PS è ``troppo astratto'' per lo scopo che si erano prefissi. In [7] mostriamo che la radice di queste difficoltà non sta in PS, ma in Sharing e, più precisamente, nell'informazione ridondante che Sharing contiene rispetto alle dipendenze ground ed al pair-sharing. Infatti, le difficoltà svaniscono se la versione non ridondante di Sharing, da noi identificata in un precedente lavoro e denotata PSD, viene utilizzata in luogo di Sharing. Per stabilire questo risultato su PSD abbiamo definito uno schema generale per sottodomini di Sharing che include come casi particolari sia PSD che Def (un altro dominio utilizzato nel campo dell'analisi di groundness). Questo getta nuova luce sulla struttura di PSD e svela una connessione naturale, sebbene inattesa, tra Def e PSD. In [7], inoltre, diamo 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.
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 [8] 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 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 [9,10] 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 riferici a nozioni classiche della teoria dell'unificazione e di consentire all'implementatore una notevole libertà d'azione. Infatti, come dimostriamo in [9,10], un analizzatore che incorpori informazione strutturale basandosi sul nostro approccio può essere estremamento 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).
E' stato stipulato un contratto per prestazione occasionale della durata di 3 mesi con la Dr. Adriana Morini finalizzato all'approfondimento e messa a punto delle tecniche di analisi di programmi basate su insiemi.