AA 2006/2007Analisi dei Ruoli1 ANALISI DEI RUOLI Visentini Diego mat.814702 De Martin Andrea mat....

AA 2006/2007 Analisi dei Ruoli 1

ANALISI DEI RUOLIANALISI DEI RUOLI

Visentini Diego Visentini Diego mat.814702mat.814702

De Martin Andrea De Martin Andrea mat. 810091mat. 810091

Laurea Specialistica in Laurea Specialistica in InformaticaInformatica

Analisi e Verifica dei Analisi e Verifica dei ProgrammiProgrammi

docente: prof. Cortesi Agostinodocente: prof. Cortesi Agostino


OBIETTIVIOBIETTIVI Nuovo “sistema di Ruoli”Nuovo “sistema di Ruoli”

Funzionalità dei ruoliFunzionalità dei ruoli

Algoritmi che implementano varie analisi dei ruoliAlgoritmi che implementano varie analisi dei ruoli


EXCURSUSEXCURSUS Introduzione generaleIntroduzione generale

Definizione e Proprietà dei ruoliDefinizione e Proprietà dei ruoli

Modello di programmazioneModello di programmazione

Analisi intraproceduraleAnalisi intraprocedurale

Analisi interproceduraleAnalisi interprocedurale

Estensioni del sistema di ruoliEstensioni del sistema di ruoli

Lavoro correlatoLavoro correlato

ConclusioniConclusioni


TIPO vs RUOLOTIPO vs RUOLO Tipo di una variabile: int, bool, float, ecc…Tipo di una variabile: int, bool, float, ecc…

Ruolo: estensione del concetto di tipo inteso come relazione Ruolo: estensione del concetto di tipo inteso come relazione di referenza tra oggetti; incrementa sia sicurezza che di referenza tra oggetti; incrementa sia sicurezza che leggibilità del programmaleggibilità del programma

Esempio ideologico, non basato su codice, che chiarisce la Esempio ideologico, non basato su codice, che chiarisce la distinzione tra ruolo e tipo: distinzione tra ruolo e tipo:

Carta PostepayCarta Postepay Il Il tipotipo dell’oggetto è “carta ricaricabile” dell’oggetto è “carta ricaricabile” Il Il ruoloruolo dipende dall’ambito in cui viene usata: dipende dall’ambito in cui viene usata:

carta di creditocarta di credito in operazioni di acquisto su internet con in operazioni di acquisto su internet con Paypal Paypal

BancomatBancomat allo sportello delle poste allo sportello delle poste


INTRODUZIONE (1) INTRODUZIONE (1)

Sistemi di ruoli tradizionali mantengono proprietà Sistemi di ruoli tradizionali mantengono proprietà “invarianti”, finchè l’oggetto esiste“invarianti”, finchè l’oggetto esiste

Ruoli di un oggetto cambiano a seconda di come Ruoli di un oggetto cambiano a seconda di come cambiano i valori memorizzati nei propri campi cambiano i valori memorizzati nei propri campi oppure mentre i programmi invocano operazioni oppure mentre i programmi invocano operazioni su tale oggettosu tale oggetto

Soluzione: integrazione tra cambiamento di stati Soluzione: integrazione tra cambiamento di stati e sistema di ruolie sistema di ruoli


INTRODUZIONE (2)INTRODUZIONE (2) Role ConceptRole Concept: lo stato di un oggetto dipende dalle : lo stato di un oggetto dipende dalle

sue relazioni di referenza con gli altri oggettisue relazioni di referenza con gli altri oggetti

Linguaggio per definire un ruoloLinguaggio per definire un ruolo: per esprimere : per esprimere invarianti e strutture datiinvarianti e strutture dati

Modello di ProgrammazioneModello di Programmazione: set di regole che : set di regole che permettono o meno la violazione dei vincolipermettono o meno la violazione dei vincoli

Linguaggio delle specifiche per l’interfaccia Linguaggio delle specifiche per l’interfaccia proceduraleprocedurale: contesto iniziale ed effetti su : contesto iniziale ed effetti su procedureprocedure

Algoritmi di analisi dei ruoliAlgoritmi di analisi dei ruoli: controllano se i vincoli : controllano se i vincoli vengono violati e in questo caso controllano se la vengono violati e in questo caso controllano se la regola applicata ne consentiva la violazioneregola applicata ne consentiva la violazione


ESEMPIO ESEMPIO Diagramma delle referenze dei ruoli per un Diagramma delle referenze dei ruoli per un process schedulerprocess scheduler


DEFINIZIONE DEI RUOLIDEFINIZIONE DEI RUOLI (1) (1) Esempio di definizione dei ruoli del grafo precedente scritto in Esempio di definizione dei ruoli del grafo precedente scritto in

pseudocodicepseudocodice

Ruolo dei processi in esecuzione: notare il vincolo identities

Ruolo dei processi in esecuzione: notare il

vincolo acyclic


DEFINIZIONE DEI RUOLI (2)DEFINIZIONE DEI RUOLI (2) Vincoli di identitàVincoli di identità

Vincoli di aciclicitàVincoli di aciclicità

Nell’esempio: il vincolo di identità Nell’esempio: il vincolo di identità next.prevnext.prev nel nel ruolo ruolo RunningProcRunningProc specifica il vincolo della lista specifica il vincolo della lista ciclica doppiamente linkata che segue il ciclica doppiamente linkata che segue il nextnext, poi , poi il campo il campo prevprev riconduce sempre all’oggetto riconduce sempre all’oggetto iniziale. Il vincolo aciclico iniziale. Il vincolo aciclico leftleft e il e il rightright nel ruolo nel ruolo SleepingProcSleepingProc specifica che non ci sono cicli specifica che non ci sono cicli nello heap inglobando solo gli archi nello heap inglobando solo gli archi leftleft e e rightright. . Dall’altro lato, la lista dei processi attivi deve Dall’altro lato, la lista dei processi attivi deve essere ciclica, perché i suoi nodi non possono mai essere ciclica, perché i suoi nodi non possono mai puntare a puntare a nullnull


PROPRIETA’ DEI RUOLIPROPRIETA’ DEI RUOLI

Proprietà di consistenza:Proprietà di consistenza: i ruoli sono in grado di i ruoli sono in grado di assicurare che il programma rispetti le proprietà di assicurare che il programma rispetti le proprietà di consistenza della struttura dati a livello applicazione. I ruoli consistenza della struttura dati a livello applicazione. I ruoli nel nostro nel nostro process schedulerprocess scheduler, per esempio, assicurano che , per esempio, assicurano che un processo non può essere contemporaneamente attivo e un processo non può essere contemporaneamente attivo e

sleepingsleeping Modifiche dell’ interfaccia:Modifiche dell’ interfaccia: l’interfaccia cambia l’interfaccia cambia

mentre cambiano le sue relazioni di referenzamentre cambiano le sue relazioni di referenza Relazioni correlate:Relazioni correlate: gruppi di oggetti cooperano per gruppi di oggetti cooperano per

implementare una parte di una funzionalità implementare una parte di una funzionalità


SINTASSI E SEMANTICA DEI RUOLI SINTASSI E SEMANTICA DEI RUOLI (1)(1)

Rappresentazione di uno Heap: Rappresentazione di uno Heap:

grafo grafo HHCC

oggetti oggetti nodesnodes((HHCC) )

archi archi (O(O11, ƒ,O, ƒ,O22) ) єє H HCC



RR set usati nelle definizioni di ruoli set usati nelle definizioni di ruoli

nullnullRR, , nullnullc, c, RR00=R =R U{nullU{nullRR}}

Ogni ruolo è rappresentato come la congiunzione Ogni ruolo è rappresentato come la congiunzione di 4 vincoli:di 4 vincoli: CampiCampi:per ogni campo :per ogni campo cc è associata una funzione è associata una funzione fieldfieldƒƒ(): R(): R 2 2RR00

SlotsSlots: slotno(: slotno(rr): un oggetto di ruolo ): un oggetto di ruolo rr può avere un può avere un numero di alias pari a slot(r) numero di alias pari a slot(r)

IdentitàIdentità: identities(: identities(rr) ) CC ƒƒ є є FF. Le identità sono coppie di . Le identità sono coppie di campi (campi (ƒ,gƒ,g) dove ogni referenza ) dove ogni referenza ƒ ƒ su un oggetto su un oggetto o o poi poi ritorna su referenze ritorna su referenze gg che portano nuovamente ad che portano nuovamente ad oo

AciclicitàAciclicità:setAcyclic(r) :setAcyclic(r) CC ƒƒ di campi lungo la quale i cicli di campi lungo la quale i cicli

sono proibitisono proibiti



REFERENCE ROLE DIAGRAMREFERENCE ROLE DIAGRAM

DEFINIZIONE FORMALE:DEFINIZIONE FORMALE:

RRD={RRD={(r,ƒ, r’) (r,ƒ, r’) | | r’ r’ єє field fieldƒ ƒ (r) e э(r) e эii (r,ƒ) (r,ƒ) є slotє sloti i ((r’ r’ )} U {)} U {(r,ƒ,(r,ƒ, null nullRR)\ )\ nullnullR R єє field fieldƒ ƒ

(r) }(r) }

Come si può notare, cattura alcuni ma non tutti i tipi Come si può notare, cattura alcuni ma non tutti i tipi di vincoli definiti in precedenzadi vincoli definiti in precedenza


MODELLO DI PROGRAMMAZIONE (1)MODELLO DI PROGRAMMAZIONE (1)

Scopo di questa tecnica: violare temporaneamente i Scopo di questa tecnica: violare temporaneamente i vincoli durante la modifica di strutture dativincoli durante la modifica di strutture dati

Linguaggio imperativo (ogni programma è un insieme di Linguaggio imperativo (ogni programma è un insieme di procedure procedure procproc) con allocazione di oggetti dinamica) con allocazione di oggetti dinamica

Oggetti onstage e offstage nello heapOggetti onstage e offstage nello heap

1.1. onstage(Hc)onstage(Hc) : referenziato da una variabile locale o da : referenziato da una variabile locale o da un parametro di qualche attivazione di recordun parametro di qualche attivazione di record

2.2. offstage(Hc)offstage(Hc) : mai referenziati da variabili locali o : mai referenziati da variabili locali o

parametriparametri


MODELLO DI PROGRAMMAZIONE (2)MODELLO DI PROGRAMMAZIONE (2)

Consistenza localeConsistenza locale

Consistenza dei nodi offstage e onstageConsistenza dei nodi offstage e onstage

Consistenza rimozione referenzeConsistenza rimozione referenze

Consistenza chiamate a proceduraConsistenza chiamate a procedura


ANALISI INTRAPROCEDURALE DEI RUOLIANALISI INTRAPROCEDURALE DEI RUOLI Rappresentazione grafica (Heap,nodi, archi)Rappresentazione grafica (Heap,nodi, archi)

Algoritmo: generare casualmente più nodi offstageAlgoritmo: generare casualmente più nodi offstage

Scopo: Verificare che oggetti che hanno lo stesso Scopo: Verificare che oggetti che hanno lo stesso ruolo ma sono rappresentati da nodi offstage ruolo ma sono rappresentati da nodi offstage diversi, hanno diversa raggiungibilitàdiversi, hanno diversa raggiungibilità

Verifica globale tramite verifica progressiva di nodi Verifica globale tramite verifica progressiva di nodi che passano a offstageche passano a offstage


ANALISI INTERPROCEDURALE DEI RUOLIANALISI INTERPROCEDURALE DEI RUOLI

Approssimiamo la funzione di trasferimento nelle semantiche Approssimiamo la funzione di trasferimento nelle semantiche concrete con interfacce procedurali consistenti in:concrete con interfacce procedurali consistenti in:

1.1. un contesto inizialeun contesto iniziale

2.2. un insieme di effettiun insieme di effetti

Assumiamo che queste interfacce procedurali siano concepite:Assumiamo che queste interfacce procedurali siano concepite:

1.1. verificando che approssimino in modo sommario il verificando che approssimino in modo sommario il comportamento della proceduracomportamento della procedura

2.2. istanziando le interfacce di procedura ai call sitesistanziando le interfacce di procedura ai call sites


INTERFACCE DI PROCEDURA (1)INTERFACCE DI PROCEDURA (1)

CONTESTO INIZIALECONTESTO INIZIALE

Il grafo di tipo iniziale assegna:Il grafo di tipo iniziale assegna: un insieme di heaps concreti ai campi della un insieme di heaps concreti ai campi della

proceduraprocedura i nomi per gli insiemi di oggetti in questi heapsi nomi per gli insiemi di oggetti in questi heaps

Denotiamo il grafo di ruolo iniziale come <HDenotiamo il grafo di ruolo iniziale come <HICIC, , ρρICIC, , KKICIC>>

Il grafo di tipo iniziale potrebbe contenere due tipi Il grafo di tipo iniziale potrebbe contenere due tipi di archi:di archi:

arco di parametroarco di parametro p p pn pn è interpretato come è interpretato come <proc, p, pn><proc, p, pn> HHICIC

arco di albero n - f arco di albero n - f m m denota un arco denota un arco <n,f,m> <n,f,m> HHICIC

Chiamiamo i nodi dell’RRD (contenuto nel grafo di Chiamiamo i nodi dell’RRD (contenuto nel grafo di ruolo iniziale)ruolo iniziale) nodi anoniminodi anonimi

ARCHI DI PARAMETRO

ARCHI DI ALBERO

NODO DICHIARATO

NODO ANONIMO


INTERFACCE DI PROCEDURA(2)INTERFACCE DI PROCEDURA(2)EFFETTI DI PROCEDURAEFFETTI DI PROCEDURA

Gli effetti di procedura:Gli effetti di procedura: approssimano conservativamente la zona dell’heap dove accede la approssimano conservativamente la zona dell’heap dove accede la

proceduraprocedura indicano cambiamenti alle relazioni di riferimento all’interno di indicano cambiamenti alle relazioni di riferimento all’interno di

questa zonaquesta zona

Ci sono due tipi di effetti:Ci sono due tipi di effetti: quelli di letturaquelli di lettura: specificano un set : specificano un set readread((procproc) di nodi del grafo di ) di nodi del grafo di

ruolo iniziale a cui ha accesso la procedura; sono usati per ruolo iniziale a cui ha accesso la procedura; sono usati per assicurare che la condizione di accessibilità sia soddisfattaassicurare che la condizione di accessibilità sia soddisfatta

quelli di scritturaquelli di scrittura: nella forma : nella forma ee11.f=e2.f=e2 raccoglie l’effetto di raccoglie l’effetto di operazioni operazioni storestore all’interno della chiamata; all’interno della chiamata; e1e1 denota gli oggetti denota gli oggetti scritti, scritti, ff il campo scritto e il campo scritto e e2e2 gli oggetti i cui riferimenti sono scritti gli oggetti i cui riferimenti sono scritti nel camponel campo


VERIFICA DELLE INTERFACCE VERIFICA DELLE INTERFACCE DI PROCEDURA(1)DI PROCEDURA(1)

Per verificare gli effetti ampliamo la rappresentazione dell’analisi Per verificare gli effetti ampliamo la rappresentazione dell’analisi <H,<H,ρρ,K>,K>..

H H è l’heap astratto che rappresenta gli oggettiè l’heap astratto che rappresenta gli oggetti ρρ è un assegnamento di ruolo astratto è un assegnamento di ruolo astratto K indica il tipo di ogni nodoK indica il tipo di ogni nodo

Un grafo di tipo non-error e’ ora una tupla <H,ρ,K,Un grafo di tipo non-error e’ ora una tupla <H,ρ,K,,E> dove:,E> dove:

:: nodes nodes(H)(H)nodesnodes00((HHICIC) e’ una trasformazione di contesto ) e’ una trasformazione di contesto iniziale che assegna un grafo di tipo iniziale iniziale che assegna un grafo di tipo iniziale (n) (n) nodesnodes(H(HICIC) ) per ogni nodo n rappresentante un oggetto che esiste a priori per ogni nodo n rappresentante un oggetto che esiste a priori verso la chiamata di procedura. Esso assegna anche NEW ad verso la chiamata di procedura. Esso assegna anche NEW ad ogni nodo rappresentante un oggetto creato durante ogni nodo rappresentante un oggetto creato durante l’esecuzione della procedural’esecuzione della procedura

E E UUiimustWrmustWrii((procproc) e’ una lista di effetti must write che la ) e’ una lista di effetti must write che la procedura ha performato finoraprocedura ha performato finora



GRAFI DI RUOLO ALLE ENTRY DI PROCEDURAGRAFI DI RUOLO ALLE ENTRY DI PROCEDURA

La nostra analisi dei ruoli:La nostra analisi dei ruoli: crea l’insieme dei grafi di ruolo alle entry di procedura dal crea l’insieme dei grafi di ruolo alle entry di procedura dal

grafo di ruolo iniziale grafo di ruolo iniziale contextcontext((procproc).). istanzia quindi i nodi nel grafo di ruolo iniziale per creare un istanzia quindi i nodi nel grafo di ruolo iniziale per creare un

set di grafici di ruolo ( La figura qui sotto descrive questo set di grafici di ruolo ( La figura qui sotto descrive questo processo )processo )

L’analisi:L’analisi:

• prima seleziona un parametro prima seleziona un parametro arco per ogni parametroarco per ogni parametro

• poi usa il parametro di poi usa il parametro di espansione di relazione espansione di relazione per per istanziare e dividere il nodo istanziare e dividere il nodo referenziatoreferenziato



VERIFICA DELLE ASSERZIONI BASEVERIFICA DELLE ASSERZIONI BASE

Per assicurare che una procedura sia conforme alla sua interfaccia, Per assicurare che una procedura sia conforme alla sua interfaccia, l’analisi usa la mappa l’analisi usa la mappa per assegnare ogni asserzione di per assegnare ogni asserzione di Load Load e e StoreStore ad un effetto dichiarato ad un effetto dichiarato

L’esecuzione simbolica di una clausola di L’esecuzione simbolica di una clausola di LoadLoad x=y.f x=y.f rende certo che il Load e’ registrato in qualche effetto lettorende certo che il Load e’ registrato in qualche effetto letto se il caso non e’ questo, viene riportato un errorese il caso non e’ questo, viene riportato un errore

L’esecuzione simbolica della clausola di L’esecuzione simbolica della clausola di StoreStore x.f=y x.f=y prima reperisce i nodi prima reperisce i nodi (nx) e (nx) e (ny) del grafo di ruolo iniziale che (ny) del grafo di ruolo iniziale che

corrispondono ai nodi nx e ny nel grafo di ruolo correntecorrispondono ai nodi nx e ny nel grafo di ruolo corrente se l’effetto < se l’effetto < (nx),f, (nx),f, (ny) > e’ dichiarato come un effetto di (ny) > e’ dichiarato come un effetto di

possibile scrittura, l’esecuzione procede come al solitopossibile scrittura, l’esecuzione procede come al solito altrimenti, l’effetto e’ usato per aggiornare la lista E degli effetti altrimenti, l’effetto e’ usato per aggiornare la lista E degli effetti

must-writemust-write



VERIFICA DELLE POSTCONDIZIONI DI PROCEDURAVERIFICA DELLE POSTCONDIZIONI DI PROCEDURA

Alla fine della procedura, l’analisi:Alla fine della procedura, l’analisi:

attua una verifica di nodo su tutti i nodi in stato usando il attua una verifica di nodo su tutti i nodi in stato usando il predicato predicato nodeChecknodeCheck(n,<H, ρ, K>, (n,<H, ρ, K>, nodesnodes(H)) per tutti i nodi (H)) per tutti i nodi nnonstageonstage(H).(H).

verifica anche che ogni effetto apportato in E può essere attribuito verifica anche che ogni effetto apportato in E può essere attribuito ad un esatto must-effect dichiarato.ad un esatto must-effect dichiarato.


ANALISI DEI CALL SITES(1)ANALISI DEI CALL SITES(1)

L’analisi aggiorna l’insieme dei grafi di ruolo dei siti alla chiamata di L’analisi aggiorna l’insieme dei grafi di ruolo dei siti alla chiamata di procedura basati sulle interfacce del chiamato e considera una procedura basati sulle interfacce del chiamato e considera una procedura procedura procproc come un call site nella forma come un call site nella forma proc’proc’(x(x11,……,x,……,xpp))

La computazione della funzione di trasferimento per un call sites ha La computazione della funzione di trasferimento per un call sites ha le seguenti fasi:le seguenti fasi:

Parameter checkParameter check Context Matching ( matchContext )Context Matching ( matchContext ) Effect Instantiation (FXEffect Instantiation (FX)) Role Reconstruction(RRRole Reconstruction(RR))



PARAMETER CHECKPARAMETER CHECK

assicura che i ruoli dei parametri siano conformi ai ruoli attesi dalla assicura che i ruoli dei parametri siano conformi ai ruoli attesi dalla chiamata chiamata proc’proc’ richiedendo richiedendo nodeChecknodeCheck(n(nii, G, , G, offstageoffstage(H(H{n{njj}}jj) ) per ogni nodo di parametro nper ogni nodo di parametro nii

CONTEXT MATCHINGCONTEXT MATCHING

assicura che i grafi di ruolo chiamati rappresentino un sottoinsieme assicura che i grafi di ruolo chiamati rappresentino un sottoinsieme dell’albero concreto rappresentato da <Hdell’albero concreto rappresentato da <HICIC, , ρρICIC, K, KICIC> derivando > derivando un mapping un mapping dal grafo di ruolo chiamato ai nodi (H dal grafo di ruolo chiamato ai nodi (H ICIC).).



EFFECT INSTANTIATIONEFFECT INSTANTIATION

usa usa mayWrmayWr((proc’proc’) e ) e mustWrmustWrii((proc’proc’) per approssimare tutti i ) per approssimare tutti i cambiamenti al grafo di ruolo che proc’ può effettuarecambiamenti al grafo di ruolo che proc’ può effettuare

ROLE RECONSTRUCTIONROLE RECONSTRUCTION

usa ruoli finali per i nodi di parametro, usa ruoli finali per i nodi di parametro, postRpostRii((proc’proc’), combinata con ), combinata con le definizioni di ruolo globali, per ricostruire i ruoli di ogni nodo le definizioni di ruolo globali, per ricostruire i ruoli di ogni nodo nella parte del grafo di ruolo che rappresenta la regione modifica nella parte del grafo di ruolo che rappresenta la regione modifica dell’heapdell’heap


ESTENSIONI DEL SISTEMA DI ESTENSIONI DEL SISTEMA DI RUOLO BASE(1)RUOLO BASE(1)

CAMBIAMENTI DI RUOLO A CASCATACAMBIAMENTI DI RUOLO A CASCATA

Noi usiamo la clausola Noi usiamo la clausola setRoleCascadesetRoleCascade(x(x11:r:r11,……..,x,……..,xnn:r:rnn) per ) per effettuare un cambiamento di ruolo a cascata su di un insieme di effettuare un cambiamento di ruolo a cascata su di un insieme di oggettioggetti

Dato un grafo di ruolo <H,ρ,K,E>, un cambio di ruolo a cascata:Dato un grafo di ruolo <H,ρ,K,E>, un cambio di ruolo a cascata: trova un nuovo valido assegnamento di ruolo ρ‘ nel quale trova un nuovo valido assegnamento di ruolo ρ‘ nel quale

l’oggetto in stato ha i ruoli desideratil’oggetto in stato ha i ruoli desiderati i ruoli degli oggetti fuori stato sono aggiustati in modo appropriatoi ruoli degli oggetti fuori stato sono aggiustati in modo appropriato

Ogni soluzione che soddisfa le costrizioni deve rispettare la Ogni soluzione che soddisfa le costrizioni deve rispettare la

semantica originalesemantica originale



RUOLI SIMULTANEIRUOLI SIMULTANEI

Questa definizione di albero Questa definizione di albero specifica che una struttura dati specifica che una struttura dati è un albero con costrizioni sui è un albero con costrizioni sui campi campi left left e e rightright

Similarmente, la definizione di Similarmente, la definizione di una lista linkata specifica una lista linkata specifica costrizioni solo per il campo costrizioni solo per il campo nextnext



Possiamo combinare l’albero ed i tipi di lista per ottenere un tipo ad Possiamo combinare l’albero ed i tipi di lista per ottenere un tipo ad albero threaded:albero threaded:

• Definizioni di ruolo per ruoli simultanei possono usare Definizioni di ruolo per ruoli simultanei possono usare precedenti definizioni di ruolo tramite la parola chiave precedenti definizioni di ruolo tramite la parola chiave extendsextends

• Le relazioni Le relazioni extendsextends sono date dall’insieme di ruoli sono date dall’insieme di ruoli subrolessubroles(r) per ogni ruolo r(r) per ogni ruolo r


LAVORO CORRELATOLAVORO CORRELATO

Approcci typestate proposti recentemente usano ruoli lineari per Approcci typestate proposti recentemente usano ruoli lineari per collegamenti ad heap per supportare i cambi di stato degli oggetti collegamenti ad heap per supportare i cambi di stato degli oggetti allocati dinamicamente.allocati dinamicamente.

I ricercatori hanno:I ricercatori hanno:

sviluppato approcci typestate per verificare le proprietà di sviluppato approcci typestate per verificare le proprietà di salvaguardia di programmi di linguaggio assemblysalvaguardia di programmi di linguaggio assembly

sviluppato sistemi che usano estensioni di ruoli lineari che evitino sviluppato sistemi che usano estensioni di ruoli lineari che evitino la pseudonimia generale e conti sul design del linguaggio per la pseudonimia generale e conti sul design del linguaggio per evitare l’inferenza di tipo non localeevitare l’inferenza di tipo non locale

adottato un approccio constraint-based che caratterizza le adottato un approccio constraint-based che caratterizza le strutture dati in termini delle costrizioni che devono essere strutture dati in termini delle costrizioni che devono essere soddisfattesoddisfatte


CONFRONTOCONFRONTO

La nostra analisi:La nostra analisi:

ha un approccio constraint-based che caratterizza le strutture ha un approccio constraint-based che caratterizza le strutture dati in termini delle costrizioni che devono essere soddisfattedati in termini delle costrizioni che devono essere soddisfatte

è incentrata sull’aspetto globale come ad esempio la è incentrata sull’aspetto globale come ad esempio la partecipazione di oggetti in strutture dati multiplipartecipazione di oggetti in strutture dati multipli

usa un meno preciso ma più scalabile trattamento di usa un meno preciso ma più scalabile trattamento di procedureprocedure

usa un approccio composizionale che analizza ogni procedura usa un approccio composizionale che analizza ogni procedura da sola per verificare che sia conforme alla sua interfacciada sola per verificare che sia conforme alla sua interfaccia

traccia molte più informazioni dettagliate riguardo l’heaptraccia molte più informazioni dettagliate riguardo l’heap


CONCLUSIONICONCLUSIONIQuesta analisi dei ruoli propone 2 idee chiave:Questa analisi dei ruoli propone 2 idee chiave: le relazioni di aliasing potrebbero determinare, in parte, il ruolo di le relazioni di aliasing potrebbero determinare, in parte, il ruolo di

ogni oggettoogni oggetto il sistema di ruolo dovrebbe usare l’oggetto risultante come sua il sistema di ruolo dovrebbe usare l’oggetto risultante come sua

astrazione fondamentale per descrivere le interfacce di procedura e astrazione fondamentale per descrivere le interfacce di procedura e le relazioni di riferimento degli oggettile relazioni di riferimento degli oggetti

ed un algoritmo di analisi che può verificare che il programma rispetti ed un algoritmo di analisi che può verificare che il programma rispetti correttamente i vincoli di ruolocorrettamente i vincoli di ruolo

I programmatori possono usare i ruoli per una varietà di utilizzi:I programmatori possono usare i ruoli per una varietà di utilizzi: per assicurare la correttezza dell’interfaccia di procedura estesa che per assicurare la correttezza dell’interfaccia di procedura estesa che

prende i ruoli dei parametri negli accountprende i ruoli dei parametri negli account per verificare importanti proprietà della consistenza delle strutture per verificare importanti proprietà della consistenza delle strutture

datidati per esprimere come le procedure muovono oggetti tra strutture datiper esprimere come le procedure muovono oggetti tra strutture dati per controllare che il programma implementi correttamente le per controllare che il programma implementi correttamente le

relazioni correlate tra gli stati di oggetti multiplirelazioni correlate tra gli stati di oggetti multipli

Ci aspettiamo perciò che i ruoli migliorino l'affidabilità del programma e Ci aspettiamo perciò che i ruoli migliorino l'affidabilità del programma e la sua trasparenza a sviluppatori e manutentori.la sua trasparenza a sviluppatori e manutentori.


RIFERIMENTI(1)RIFERIMENTI(1)[1] A. Albano, R. Bergamini, G. Ghelli and R. Orsini. An introduction to [1] A. Albano, R. Bergamini, G. Ghelli and R. Orsini. An introduction to

database programming language Fibonacci. The VLDB journal, 4(3), database programming language Fibonacci. The VLDB journal, 4(3), 19951995

[2] Craig Chambers. Predicate Classes. In proceedings of the 7° European [2] Craig Chambers. Predicate Classes. In proceedings of the 7° European Conference on Object-Oriented Programming, pages 268-296, 1993Conference on Object-Oriented Programming, pages 268-296, 1993

[3] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. [3] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. Fickle: Dynamic objet re-classification. In proceedings of the 15° Fickle: Dynamic objet re-classification. In proceedings of the 15° European Conference on Object-Oriented Programming, LNCS 2072, European Conference on Object-Oriented Programming, LNCS 2072, pages 130-149. Springer, 2001.pages 130-149. Springer, 2001.

[4] Rakesh Ghiya and Laurie J. Hendren. Connection analysis: A practical [4] Rakesh Ghiya and Laurie J. Hendren. Connection analysis: A practical interprocedural heap analysis for C. In Proceedings of the 8° Workshop interprocedural heap analysis for C. In Proceedings of the 8° Workshop on Languages and Compilers for Parallel Computing, 1995.on Languages and Compilers for Parallel Computing, 1995.

[5] Laurie J. Hendren, Josep Hummel, and Alexsandru Nicolau. A general [5] Laurie J. Hendren, Josep Hummel, and Alexsandru Nicolau. A general data dependence test for dynamic, pointer-based data structures. In data dependence test for dynamic, pointer-based data structures. In Proceedings of the SIGPLAN’94 Conference on Programming Language Proceedings of the SIGPLAN’94 Conference on Programming Language Design and Implementation, 1994.Design and Implementation, 1994.


RIFERIMENTI(2)RIFERIMENTI(2)[[6] Jacob J. Jensen, Michael E. Joergensen, Nils Klarlund, and Michael I. 6] Jacob J. Jensen, Michael E. Joergensen, Nils Klarlund, and Michael I.

Schwartzbach. Automatic verification of pointer programs using Schwartzbach. Automatic verification of pointer programs using monadic second order logic. In Proceedings of the SIGPLAN’94 monadic second order logic. In Proceedings of the SIGPLAN’94 Conference on Programming Language Design and Implementation, Conference on Programming Language Design and Implementation, Las Vegas, NV, 1997.Las Vegas, NV, 1997.

[7] Victor Kunkak. Designing an algorithm for role analysis. Master’s [7] Victor Kunkak. Designing an algorithm for role analysis. Master’s thesis, Massachusetts Institute of Tecnology, 2001.thesis, Massachusetts Institute of Tecnology, 2001.

[8] Trygve Reenskaug. Working with Objects. Prentice Hall, 1996.[8] Trygve Reenskaug. Working with Objects. Prentice Hall, 1996.

[9] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric Shape [9] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric Shape Analysis via 3-valued logic. In Proceeding of the 26° Annual ACM Analysis via 3-valued logic. In Proceeding of the 26° Annual ACM Symposium on the Principles of Programming Languages, 1999.Symposium on the Principles of Programming Languages, 1999.

[10] Wolfgang Thomas. Languages, automata, and logic. In Handbook of [10] Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages Vol.3: Beyond Words. Springer-Verlag, 1997.Formal Languages Vol.3: Beyond Words. Springer-Verlag, 1997.

AA 2006/2007Analisi dei Ruoli1 ANALISI DEI RUOLI Visentini Diego mat.814702 De Martin Andrea mat....

Documents

Transcript of AA 2006/2007Analisi dei Ruoli1 ANALISI DEI RUOLI Visentini Diego mat.814702 De Martin Andrea mat....