Linguaggi modulari e ad oggetti

Linguaggi modulari e ad oggetti - Risultati

La ricerca riguarda fondamenti, design ed implementazione di linguaggi modulari ed object-oriented. Il filone vede coinvolte le unità di Genova, Padova, Torino e Udine.

Vi sono collaborazioni/sovrapposizioni con le tematiche 2 (Linguaggi logici) e 5 (Modelli, linguaggi e tecniche di specifica algebrica).
La ricerca afferente a questa tematica si articola nei seguenti sottotemi:

Calcoli di oggetti (4.1)

Linguaggi di moduli (design e fondamenti) (4.2)

Linguaggi object-oriented riflessivi (design ed implementazione) (4.3)

Calcoli di oggetti

L'attività di ricerca in questo sottotema ha visto la partecipazione dei ricercatori dell'unità di Padova, Torino ed Udine.

Il contesto generale della ricerca è quello dei calcoli ad oggetti, cioè calcoli che costituiscono l'astrazione di linguaggi object-oriented, nello stesso modo in cui il lambda calcolo fornisce un modello per la programmazione funzionale: esempi ormai "classici" sono l'Object Calculus di Abadi e Cardelli ed il Lambda Calculus of Objects di Fisher, Honsell, Mitchell (LCO nel seguito).
Tra gli scopi dello sviluppo e studio di tali calcoli vi è la definizione di sistemi di tipo "safe" che consentano di prevenire a tempo di compilazione errori di "messaggio non compreso", e il fornire un modello matematico di vari concetti dell'object-oriented evidenziandone eventuali interazioni o ortogonalità.
Si tratta di una ricerca di tipo fondamentale ma con una ricaduta immediata sul design e l'implementazione di linguaggi reali.

L'attività di ricerca si è svolta in questo settore è stata relativa a svariati aspetti. Ne elenchiamo qui sotto quattro: l'estensione di calcoli di oggetti con oggetti incompleti, la definizione di sistemi di tipi e algoritmi di type-inference, la modellazione della nozione di classe e il trattamento di caratteristiche imperative; molti lavori sono tuttavia relativi a più aspetti contemporaneamente.

Calcoli object-based con oggetti incompleti L'attività relativa a tale filone di ricerca ha come base di partenza LCO. Tale calcolo integra il lambda calcolo con primitive object-based. Gli oggetti che si possono rappresentare in tale calcolo sono sia modificabili (tramite overriding), sia estensibili (tramite un'operazione di "method addition"). Il fatto che gli oggetti siano estensibili implica, a livello del sistema di tipi, che si modelli la cosidetta ereditarietà "MyType", ovvero che i metodi siano tipati in modo polimorfo.
Tale calcolo è stato sviluppato in direzioni diverse.
In [BonoEtAl00], si sono combinate due interessanti caratteristiche: la possibilità di lavorare con oggetti "incompleti", ovvero con oggetti che contengono solo parte della loro implementazione, permettendo di modellare un'interessante forma di "rapid prototyping", e una forma di sottotipaggio compatibile con l'operazione di method addition.
Sistemi di tipi e type-inference Un'altra direzione di ricerca relativa ad LCO ha riguardato la semplificazione del sistema di tipi originale, dove l'ereditarietà MyType viene modellata in modo elegante ma molto complesso. Questo risultato [BonoBugliesi99], anche se piuttosto tecnico, ha il pregio di permettere una comparazione più diretta di LCO con altri calcoli object-based (quali quelli di Abadi e Cardelli e di Bruce), nonchè di essere una base più semplice sia per uno studio dal punto di vista semantico degli oggetti estensibili via una codifica in un lambda calcolo higher-order [BonoBugliesi98], sia come punto di partenza per risolvere il problema di trovare un algoritmo di inferenza di tipo per un calcolo con MyType ("work-in-progress"). Relativo al problema della type inference è [Bugliesi Pericas00]. In questo lavoro viene definito un sistema di tipi per un calcolo ad oggetti senza estensione, ma con override, che ammette subtyping in depth; è dato un algoritmo di inferenza polinomiale per il sistema. In [Liquori99] si propone un'estensionde del calcolo di Abadi e Cardelli con "MyType", compatibilmente con estensione e subtyping, e variabili private e pubbliche.
Modellazione dell'entità classe Se il concetto di "oggetto" può essere ormai considerato chiarito da un punto di vista fondazionale, non altrettanto si può dire per il concetto di "classe".
L'attività di ricerca riguardo questo filone ha seguito due strade, essenzialmente ortogonali, proprio per poter esplorare più possibilità differenti.
In un approccio, le classi sono viste come combinazione di oggetti estensibili e tipi di dati astratti, secondo l'idea di Fisher e Mitchell. In [BonoFisher98] viene studiato un linguaggio object-based imperativo che modella, appunto, le classi come oggetti estensibili ed encapsulabili. Nell'altro approccio, le classi sono rappresentate come entità primitive, piuttosto che generabili a partire da altri costrutti. In [BonoEtAl98], [BonoEtAl99] viene presentato un calcolo class-based imperativo, che unisce in sè un'inizio di studio formale dell'entità classe e una serie di buoni requisiti di software engineering.
Calcoli imperativi Oltre ai lavori [BonoEtAl98], [BonoEtAl99] precedentemente menzionati, caratteristiche imperative sono considerate in [LangEtAl99], [DoughertyEtAl99]. Questi articoli fondano le basi per un framework ad oggetti dove le caratteristiche funzionali, imperative e ad oggetti si possono combinare in modo modulare. Il formalismo è basato sulle sostituzioni esplicite e la graph rewriting è alla base della semantica operazionale.

Infine, una ricerca confinante con la tematica 2 (Linguaggi logici) ha riguardato la codifica di diversi calcoli di oggetti in logica lineare [BugliesiEtAl00].

Articoli

[BonoBugliesi98] V. Bono, M. Bugliesi,"Interpretation of Extensible Objects and Types", FCT'99, 1999.

[BonoBugliesi99] V. Bono, M. Bugliesi, "Matching for the Lambda Calculus of Objects".

[BonoEtAl00] V. Bono, M. Bugliesi, M. Dezani-Ciancaglini, L. Liquori, "A Subtyping for Extensible, Incomplete Objects".

[BonoFisher98] V. Bono, K. Fisher, "An Imperative, First-Order Calculus with Object Extension".

[BonoEtAl98] V. Bono, A. Patel, V. Shmatikov, J.C. Mitchell, "A Core Calculus of Classes and Objects", MFPS'99, 1999.

[BonoEtAl99] V. Bono, V. Shmatikov, A. Patel, "A Core Calculus of Classes and Mixins", ECOOP'99, LNCS, Springer Verlag, 1999.

[BugliesiPericas00] M. Bugliesi, S. Pericas, "Depth subtyping and Type Inference for Object Calculi", FOOL'00.

[BugliesiEtAl00] M. Bugliesi, G. Delzanno, L. Liquori, M. Martelli, "Object Calculi in Linear Logic".

[DoughertyEtAl99] D. Dougherty, F. Lang, P. Lescanne, L. Liquori, K. Rose, "A Generic Object-Calculus Based on Addressed Term Rewriting Systems".

[LangEtAlAl99] F. Lang, P. Lescanne, L. Liquori, "A Framework for Defining Object Calculi".

[Liquori99] L. Liquori, "Bounded Polymorphism for Extensible Objects".

Linguaggi di moduli (design e fondamenti)

L'attività di ricerca in questo sottotema ha visto la partecipazione dei ricercatori dell'unità di Genova.

Questa ricerca è relativa al design ed allo studio dei fondamenti dei linguaggi di moduli. Negli ultimi anni infatti vi è stato un notevole sviluppo di linguaggi con caratteristiche di modularità molto avanzate: citiamo ad esempio il sistema di moduli di ML nelle diverse varianti proposte, i meccanismi caratteristici dell'approccio object-oriented (inheritance ed overriding), i mixin (classi o, in generale, moduli con componenti "deferred", cioè non definite), il crescente interesse per la fase di linking, dovuto allo sviluppo di linguaggi, come Java, in cui i moduli in codice intermedio (bytecode) conservano molte informazioni di tipo.
In parallelo, una rilevante attività di ricerca è stata dedicata all'analisi ed ai fondamenti formali di tali linguaggi. Un principio che è emerso come idea comune dai vari approcci proposti è quello di vedere un linguaggio come strutturato in due livelli: il linguaggio core (secondo la terminologia introdotta con ML) e il linguaggio dei moduli, un linguaggio autonomo con proprie regole di tipo ed il più possibile indipendente dal livello sottostante, anzi in principio istanziabile su diversi linguaggi core.

L'attività di ricerca svolta in questo settore può essere riassunta come segue.

Si è definito un nucleo per un linguaggio di moduli mixin basato su tre semplici operatori primitivi: somma, ridotto e freeze [AnconaZucca98a]. Il linguaggio è definito in maniera il più possibile indipendente dal linguaggio core sottostante; tale indipendenza è realizzata anche a livello semantico utilizzando un framework categoriale (si ottiene quindi una semantica denotazionale composizionale).
Si è studiata la possibilità di tradurre diversi operatori di overriding presenti nei linguaggi di programmazione in questo nucleo linguistico [AnconaZucca97].
Si è data una presentazione assiomatica del linguaggio di moduli mixin proposto [AnconaZucca98]; tale assiomatizzazione mostra anche come esprimere diversi altri operatori (merge, overriding, composizione funzionale, hiding, etc.) per mezzo dei tre operatori base, e permette di provare un teorema di forma normale.
Si è definito un calcolo di moduli parametrico sul livello core con semantica di riduzione confluente e sistema di tipi sound [AnconaZucca99,AnconaZucca99b].
Infine, si è definita ed implementata un'estensione (chiamata Jam) di Java con mixin, intesi qui come classi eredi parametriche [AnconaEtAl99a].

Inoltre, altre attività di ricerca sono confinanti con la tematica 5, sottotematica 1 (Metodi formali e semiformali nelle varie fasi dello sviluppo dei sistemi informatici).

In [Ancona99] si è affrontato il problema di definire un framework algebrico per la modularizzazione che supporti la compilazione separata.
In [AnconaEtAl99] si è proposta la definizione di un formalismo di specifica (institution) in cui è esprimibile la nozione di "tipo dinamico" (tipo a run-time di un'espressione) e quindi la risoluzione dell'overloading, cioè la scelta della funzione da invocare in corrispondenza di un certo nome di funzione, può essere fatta a run-time in base al tipo dinamico di uno o più argomenti. In [AnconaEtAl99b] si è studiato come applicare quest'idea nell'ambito di CASL, il linguaggio standard di specifica algebrica proposto nell'ambito dell'iniziativa COFI.

Articoli

[Ancona99] D. Ancona, "An Algebraic Framework for Separate Type-Checking.

[AnconaEtAl99] D. Ancona, M.Cerioli, E. Zucca, "A Formal Framework with Late Binding".

[AnconaEtAl99b] D. Ancona, M.Cerioli, E. Zucca, "Extending Casl with Late Binding".

[AnconaEtAl99a] D. Ancona, G. Lagorio, E. Zucca, "Jam: A Smooth Extension of Java with Mixins".

[AnconaZucca97] D. Ancona, E. Zucca, "Overriding Operators in a Mixin-Based Framework".

[AnconaZucca98] D. Ancona, E. Zucca, "An Algebra of Mixin Modules".

[AnconaZucca98a] D. Ancona, E. Zucca, "A Theory of Mixin Modules: Basic and Derived Operators".

[AnconaZucca99] D. Ancona, E. Zucca, "A Primitive Calculus for Module Systems".

[AnconaZucca99b] D. Ancona, E. Zucca, "A Calculus of Module Systems".

Linguaggi object-oriented riflessivi (design ed implementazione)

L'attività di ricerca in questo sottotema ha visto la partecipazione dei ricercatori dell'unità di Genova.

Il contesto della ricerca è quello dei sistemi riflessivi, ossia sistemi che contengono al loro interno una rappresentazione di se stessi per cui possono automodificarsi. Molti linguaggi object-oriented hanno caratteristiche riflessive, ad esempio Smalltalk ed in parte Java.
I risultati della ricerca sono relativi ai seguenti argomenti:

Modello a Materializzazione del Canale un nuovo modello riflessivo, orientato alla comunicazione ed alla distribuzione, di uso complementare al noto schema basato sul metaoggetto [AnconaEtAl97a, AnconaEtAl97b,AnconaEtAl98].
Sicurezza e Riflessione. Si studia come modellare con architetture riflessive gli schemi di protezione di un sistema software, evidenziandone benefici e svantaggi [AnconaEtAl98a].È una collaborazione internazionale con la FAU USA (E. Fernandez).
Studio comparato di vari modelli riflessivi[Cazzola98].
Studio di paradigmi per lo sviluppo di applicazioni fault tolerant[CazzolaEtAl98].

Articoli

[AnconaEtAl97a] M. Ancona, W. Cazzola, G. Dodero, V. Gianuzzi, "Channel reification: a reflective model for distributed computation".

[AnconaEtAl97b] M. Ancona, W. Cazzola, G. Dodero, V. Gianuzzi, "Communication modelling in channel reification".

[AnconaEtAl98] M. Ancona, W. Cazzola, G. Dodero, V. Gianuzzi, "Channel reification: a reflective model for distributed computation".

[AnconaEtAl98a] M. Ancona, W. Cazzola, E. Fernandez, "Reflective authorization systems".

[Cazzola98] W. Cazzola, "Evaluation of Object-Oriented reflective models".

[CazzolaEtAl98] W. Cazzola, A. Clematis, V. Gianuzzi, A. Romanosvky, A. Tyrrel, "Approaches to designing complex dependable systems".

Vai alla pagina principale del progetto.
Responsabile: Maurizio Martelli.

Commenti e suggerimenti a: zucca@disi.unige.it

Ultimo aggiornamento: 13 gennaio 2000