10/5/2010 UNICAM - p. 1/38

Ingegneria del software

Alloy, per esempio

Rosario Culmonerosario.culmone@unicam.it

10/5/2010 UNICAM - p. 2/38

Contesto

Gli attuali software sono costituiti da milioni di righe di codice (Microsoft Word).I sistemi operativi da decine di milioni di righe di codice (Linux, Windows). Segli errori di codifica possono essere inevitabili (programmatori indianisottopagati), gli errori di progettazione possono essere evitati.

In termini di stati, un programma si può trovare in decine di miliardi di possibilistati. Ad esempio se un programma gestisce una memoria dati di 1 KByte, ilnumero di possibili stati è teoricamente 2

8192, un sistema operativo ...

10/5/2010 UNICAM - p. 3/38

Sistemi critici

Vi sono diversi contesti in cui bisogna in tutti i modi evitare di produrre softwaremalfunzionante. Ad esempio:▲ Dispositivi medicali: pacemaker, defibrillatori, raggi X, TAC▲ Produzione dell’energia: centrali nucleari, centrali termoelettriche, centrali

idroelettriche▲ Trasporto: controllo del traffico aereo, controllo di navigazione aerea, sistemi

di controllo della stabilità▲ Finanza: gestione dei flussi finanziari, gestione dei bilanci▲ Difesa: siatemi di puntamento, sistemi di difesa, sistemi di guida di missili▲ Produzione industriale: apparecchi di precisione, sistemi elettroniciIn questi contesti l’errore di progettazione può avere gravissime conseguenze!

10/5/2010 UNICAM - p. 4/38

Conseguenze

La cattiva progettazione può avere diverse conseguenze:▲ Perdite economiche: il blocco del sistema di gestione di borsa di pochi minuti

può avere costi di svariate decine di milioni di perdite. Il blocco delfunzionamento di Google per un ora produce una perdita di mancati introitipubblicitari di decine di milioni di dollari.

▲ Perdite di vite umane: il blocco del sistema di navigazione di un aereo dilinea può causare la morte dei passeggeri. Il malfunzionamento del sistemadi controllo di una centrale nucleare può produrre decine di migliaia di morti.La cattiva progettazione del Therac-25 ha prodotto 8 morti.

▲ Fallimento di progetti: un errore di progettazione del sistema di gestione dibasi di dati dBase dell’Ashton-Tate lo ha portato al fallimento. Ilmalfunzionamento del sistema di controllo del missile Arianne-5 ha causatola perdita di due satelliti.

10/5/2010 UNICAM - p. 5/38

Soluzione

Questo è un estratto della licenza d’uso di Windows XP

ATTIVITÀ AD ALTO RISCHIOIl SOFTWARE non è fault-tolerant (ossia non funziona in casodi guasti) e non è stato progettato, costruito o concepitoper essere utilizzato o rivenduto come strumento di control loon-line in ambienti a rischio che richiedono un utilizzo aprova di guasti - come nella gestione di apparecchi nucleari ,sistemi di navigazione e di comunicazione aerea, controllodel traffico aereo, apparecchiature medicali di supportovitale o armamenti - in cui il malfunzionamento del SOFTWAREpotrebbe causare morte, danni personali o gravi danni fisic i oambientali ("Attività ad Alto Rischio"). MICROSOFT ed i suo ifornitori dichiarano espressamente di non concedere alcun agaranzia, espressa o implicita, di idoneità per Attività adAlto Rischio.

10/5/2010 UNICAM - p. 6/38

Soluzione alternativa

Progettare e produrre software di qualità.

Per produrre software di qualità è necessario:▲ seguire in modo rigoroso un processo di produzione,▲ adottare metodologie di provata affidabilità,▲ usare strumenti per la verifica dei prodotti della progettazione e▲ adottare strumenti per la produzione automatizzata del codice

Pur adottando quando detto sopra non potremmo mai essere certi che ilprodotto software sia esente da errori di progettazione o di codifica mapotremmo ridurli notevolmente.

10/5/2010 UNICAM - p. 7/38

Strumenti

In questo corso si utilizzerà:▲ UML/OCL: nella fase di analisi e progettazione sia degli aspetti statici che

dinamici▲ Reti di Petri: nella fase di specifica formale degli aspetti dinamici del sistema▲ Alloy: nella fase di progettazione per la specifica formale dei requisiti e

verifica di correttezza▲ JML: nella fase di codifica permette di annotare pre/post e invarianze oltre

che vincoli sui dati

10/5/2010 UNICAM - p. 8/38

Introduzione

Introduciamo Alloy con un semplice esempio di modello statico.▲ In particolare impareremo nel definire il modello:

● come definire domini, sottoinsiemi, relazioni con vincoli sulla molteplicità● come usare quantificatori e predicati per definire correttamente il modello

▲ Come utilizzare il framework Alloy per:● Eseguire il codice Alloy● impostare parametri e visualizzare le istanze del modello

10/5/2010 UNICAM - p. 9/38

Famiglia

Vogliamo modellare le relazioni familiari come:▲ i genitori e i figli sono relazioni primitive▲ la moglie/marito è una relazione primitiva▲ i fratelli è una relazione derivata▲ i vincoli biologici e sociali sono predicati

10/5/2010 UNICAM - p. 10/38

Dominio

Compongono il dominio gli insiemi che sono disgiunti e che possono avere unarelazione diretta con la realtà. Tipicamente in Alloy si segue la stessa strategiache si segue in UML. Esempio di dichiarazione sono:sig Persona {}sig Auto {}

La stringa sig è l’abbreviazione di signature. L’identificatore di un insieme ègeneralmente un sostantivo in maiuscolo e singolare. Le parentesi graffe cheseguono indicano la tipica rappresentazione matematica dell’insieme

10/5/2010 UNICAM - p. 11/38

Sottoinsiemi

Possono essere definiti sottoinsiemi da insiemi:▲ definire un sottoinsieme direttamente da un insieme

Utilitaria : Auto // Utilitaria è un sottoinsieme di Auto

▲ definire un sottoinsieme indirettamente da un sottoinsiemeElettrica : Utilitaria / * Elettrica è un sottoinsieme

di Utilitaria * /

▲ è possibile definire sottoinsiemi da un insiemeSpider, Utilitaria, SUV : Auto / * Spider, Utilitaria e SUV

sono tutti sottoinsiemidi Auto * /

10/5/2010 UNICAM - p. 12/38

Vincoli sugli insiemi

E’ possibile descrivere ulteriori vincoli sugli insiemi:▲ extends è usata con lo stesso significato nei class diagram UML o classi

Java.Utilitaria, Spider extends AutoOvvero Utilitaria e Spider sono sottoinsiemi di Auto ma possono esservi autoche no sono ne Spider ne Utilitarie che appartengono a Auto. Tale vincologarantisce solo che Spider e Utilitaria sono disgiunti

▲ abstract è usata con lo stesso significato nei class diagram UML o classiJava.Utilitaria, Spider extends abstract AutoOltre a quanto detto prima la stringa abstract applicata ad Auto specifica cheUtilitaria e Spider sono copertura di Auto ovvero la somma degli elementi diin Spider e Utilitaria sono pari agli elementi in Auto. Non esistono istanze inAuto

10/5/2010 UNICAM - p. 13/38

Altre operazioni su insiemi

Se si volesse avere un insieme con due diversi partizionamenti sempre sullostesso insieme si devono utilizzare ulteriori vincolisig X { }sig A, B, C, D in X { } {A+B=X and C+D=X and no A&B and no C&D}

Un insieme X ha 4 sottoinsiemi A, B, C e D. Per far si che A e B copranocompletamente X si usa l’unione + e l’uguaglianza =. Per imporre che A e Bsiano disgiunti si impone che l’intersezione & sia vuota no

10/5/2010 UNICAM - p. 14/38

Il modello Famiglia

Sposato

Persona

Uomo Donna

module Famigliaabstract sig Persona {}sig Uomo, Donna extends Persona {}sig Sposato {p : Persona}

Naturalmente questo è un possibile modello ma ne possono essere definiti altriper lo stesso problema

10/5/2010 UNICAM - p. 15/38

Istanze

In Alloy è possibile generare automaticamente le istanze descritte con ilmodello. Ad esempio per il modello precedente si possono avere:

Dominio Persona Uomo Donna Sposato OK

A {P0,P1,P2 } {P1, P2} {P0} {} ∨

B {P0,P1,P2 } {P1, P2} {P0, P1} {} ×

C {P0,P1,P2,P4 } {P1, P2, P3, P4} {} {P2, P3} ∨

D {P0, P1} {P0} {} {P1} ×

E {P0,P1} {P0} {P1} {P0,P1} ∨

. . . . . . . . . . . . . . . . . .

10/5/2010 UNICAM - p. 16/38

Relazioni

E’ possibile dichiarare una relazione tra due insiemi. La relazione è anch’essaun’insieme composto da coppie di elementi che appartengono a due insiemi.Ad esempio:possiede : Persona -> Auto

Sostanzialmente una relazione denota un sottoinsieme del prodotto cartesianotra Persona × Auto. La relazione non necessariamente denota una funzione(iniettiva, suriettiva, totale, pariziale, funzione, ...)

10/5/2010 UNICAM - p. 17/38

Famiglia con parenti

module Famigliaabstract sig Persona { fratelli : Persona -> Persona }sig Uomo, Donna extends Persona {}sig Sposato { moglie-marito : Persona }

Possibili istanze sono:Dominio Persona Uomo Donna Sposato fratello

A {P0,P1,P2, P3 } {P1, P2} {P0,P3} {} {(P0,P1),(P0,P2),(P1,P1)}. . . . . . . . . . . . . . . . . .

10/5/2010 UNICAM - p. 18/38

Operatori sulle relazioni

E’ possibile avere la trasposta di una relazione ovvero invertire dominio eimmagine.possiede : Persona -> Auto

haProprietario = ∼ possiede

10/5/2010 UNICAM - p. 19/38

Molteplicità

E’ possibile definire la molteplicità di un insieme.▲ some indica che l’insieme possiede uno o più elementi▲ lone indica che l’insieme possiede zero o più elementi▲ one indica che l’insieme possiede solo un elementoAd esempiosig Persona { figli : lone Persona, padre, madre : one Persona }

Una persona può avere figli ma sicuramente ha un padre e una madre

10/5/2010 UNICAM - p. 20/38

Molteplicità e relazioni: some -> one

Se la relazione è la seguente.f : A -> one B

Si vuole definire una relazione f che per ciascun elemento di A mappaesattamente un solo elemento di B. In matematica si dice che f è una funzionetotale

OK

a1

a2

a3

a4

b1

b2

b3

b4NO

a1

a2

a3

a4

b1

b2

b3

b4NO

a1

a2

a3

a4

b1

b2

b3

b4NO

a1

a2

a3

a4

b1

b2

b3

b4

10/5/2010 UNICAM - p. 21/38

Molteplicità e relazioni: one -> one

Se la relazione è la seguente.f : A one -> one B

Se per esattamente un elemento di A corrisponde esattamente un elemento diB bigettiva

NO

a1

a2

a3

a4

b1

b2

b3

b4OK

a1

a2

a3

a4

b1

b2

b3

b4NO

a1

a2

a3

a4

b1

b2

b3

b4NO

a1

a2

a3

a4

b1

b2

b3

b4

10/5/2010 UNICAM - p. 22/38

Molteplicità e relazioni: lone -> lone

Se la relazione è la seguente.f : A lone -> lone B

Se per almeno un elemento di A corrisponde almeno un elemento di Bparziale iniettiva

NO

a1

a2

a3

a4

b1

b2

b3

b4OK

a1

a2

a3

a4

b1

b2

b3

b4OK

a1

a2

a3

a4

b1

b2

b3

b4NO

a1

a2

a3

a4

b1

b2

b3

b4

10/5/2010 UNICAM - p. 23/38

Operatori su insiemi

Gli operatori usuali su insiemi sono:▲ + unione. Esempio Utilitarie+Spider

▲ & intersezione. Esempio Alti&Magri è l’nsieme delle persone che sonocontemporaneamente alti e magri

▲ - differenza. Esempio Persone-Magri è l’insieme delle persone escluse lemagre

10/5/2010 UNICAM - p. 24/38

Predicati

Sugli insiemi è possibile chiedersi:▲ some A è vero se in A vi è almeno un elemento (#A>0)▲ no A è vero se in A vi sono elmenti (#A=0)▲ sole A è vero se in A vi è al più un elemento (#A<=1)▲ one A è vero se in A vi è solo un elemento (#A=1)

10/5/2010 UNICAM - p. 25/38

Confronti tra insiemi

Sempre sugli insiemi possono essere effettuate operazioni di confronto▲ A=B è vero se A e B hanno gli stessi elementi▲ A in B è vero se A è un sottoinsieme di B

▲ A<>B è vero se A e B sono diversi▲ A not in B è vero se A non è un sottoinsieme di B

10/5/2010 UNICAM - p. 26/38

Proprietà su insiemi

I caratteri { e } definiscono come in matematica un insime. Se si vuole definireun insieme con proprietà è possibile farlo:{ x : A | P }

Ha il significato di voler definire un insieme i cui tutti gli elementi x presidall’insieme A soddisfano il predicato P

{ x : Int | x > 4 and x < 8}

L’insieme così definito contiene tre elementi ovvero 5, 6, 7

10/5/2010 UNICAM - p. 27/38

Operatori logici

Naturalmente vi sono gli usuali operatori logici:▲ a && b oppure a and b la congiunzione▲ a || b oppure a or b disgiunzione▲ !a oppure not a la negazione▲ a => b l’implicazione▲ a<=>b la doppia implicazione

10/5/2010 UNICAM - p. 28/38

Quantificatori

E’ possibile utilizzare i quantificatori nei predicati▲ all x : A | P indica che il quantificatore è vero se per tutti gli elementi x

appartenenti all’insieme A è vero il predicato P

▲ some x : A | P indica che il quantificatore è vero se per almeno unelemento x appartenente all’insieme A è vero il predicato P

▲ no x : A | P indica che il quantificatore è vero se per nessun elemento xappartenente all’insieme A è vero il predicato P

▲ sole x : A | P indica che il quantificatore è vero se per al più unelemento x appartenente all’insieme A è vero il predicato P

▲ all x : A | P indica che il quantificatore è vero se solo per un elementox appartenente all’insieme A è vero il predicato P

10/5/2010 UNICAM - p. 29/38

L’operatore punto

Se si definiscono due insiemisig B { }sig A { r : B }

Gli elementi di A "riferiscono" elementi di B mediante l’etichetta di sottoinsiemer . In pratica per ogni elemento di A è associato un sottoinsieme di B. Quindil’etichetta r realizza una relazione del tipo r : A -> B . Per semplificarel’utilizzo è definito l’operatore . (punto). L’operatore punto permette di"navigare" attraverso gli insiemi. Ad esempio{ e : A | sole e.r }

L’insieme definito è composto da tutti gli elementi di A che hanno associato alpiù un elemento in B

10/5/2010 UNICAM - p. 30/38

Navigazione

Se si definiscesig Persona { figli : Persona }

con all e : Persona | e not in e.figli si esprime il fatto che non èpossibile essere figli di se stesso.con disj no e1, e2 : Persona | no e1.figli&e2.figli esprime ilfatto che non esistono due persone che hanno un figlio in comune

10/5/2010 UNICAM - p. 31/38

Chiusura

Se si definiscesig Persona { figli : Persona }

Se la relazione è del tipo, come in questo caso, r:A->A ovvero dove dominio ecodominio coincidono allora è possibile applicare l’operatore di chiusuratransitiva ^ e chiusura transitiva riflessiva * . A esempio conall e : Persona | e not in e.^figli si vuole esprimere il fatto chenon esistono cicli ovvero che non esistono progenitori che possono essereantenati (cosa evidentemente assurda!).L’operatore di chiusura produce un insieme. La chiusura transitiva escludel’elemento a cui è applicata mentre la chiusura transitiva riflessivaincludel’elemento a cui è applicata.

10/5/2010 UNICAM - p. 32/38

Class diagram PersonaPersona

anni : integer

nascita : integer

Uomo Donnamoglie

0..1

marito

0..1

figlio

0..*

abstract sig Persona { nascita, anni : one Int,figli : set Persona }

sig Uomo { moglie : lone Donna }sig Donna { marito : lone Uomo }

10/5/2010 UNICAM - p. 33/38

Vincoli su Persona

La struttura su definita non garantisce la correttezza del modello. E’ facileosservare che vi sono diverse situazioni anomale ad esempio sposare unafiglia o far nascere figli prima della propria data di nascita.In questa fase bisogna definire dei vincoli, ad esempio:1. ogni persona ha un solo padre e una sola madre2. ogni persona può sposare una persona dell’altro sesso se ha un’età

superiore a 14 anni e se la differenza non è superiore a 303. ogni persona non può sposare antenati o figli4. nessuna persona non può avere come antenati progenie5. non è possibile il matrimoni tra fratelli6. la data di nascita di un genitore deve essere precedente di almeno 14 anni

la data di nascita dei figli7. una donna non può avere figli a distanza inferiore di 1 anno8. . . .

10/5/2010 UNICAM - p. 34/38

Fatti

I vincoli che sono strutturali con il modello sono fatti ovvero vincoli che nonpossono essere infranti e che sono parte integrante della semantica delmodello.

La frase "ogni persona ha un solo padre e una sola madre" è un vincolo chenon ammette eccezioni quindi diventa:fact FatherMother {

all p : Person | one f, m : Persona |p = f.figlio and p = m.figlio

}

Da notare che bisogna affermare che si abbia "un solo" padre e "una sola"madre. Sarebbe stato diverso per "almeno" o "al più".La frase "nessuna persona non può avere come antenati progenie" è unvincolo biologico quindi diventafact noCicle { no p : Persona | p in p.^figlio }

10/5/2010 UNICAM - p. 35/38

Predicati

Vi possono essere dei vincoli che possono essere fatti entrare e uscire dalmodello. In questo caso tali vincoli si chiamano predicati. I predicati possonodiventare fatti se valutati essenziali per la consistenza del modello. Spesso ipredicati servono per mettere a punto il modello.

La frase "la data di nascita di un genitore deve essere precedente di almeno 14anni la data di nascita dei figli" può essere tradotta inpred fertility { all p : Person | one f, m : Persona |

p = f.figlio and p = m.figlio andf.nascita + 14 < p.nascita and m.nascita + 14 < p.nascita

}

Da notare che non necessariamente una persona deve avere figli

10/5/2010 UNICAM - p. 36/38

Asserzioni

Se sospettiamo che il nostro modello contenga delle falle ovvero dei vincoli chenon sono direttamente espressi, possiamo esprimere questi vincoli addizionalicome assert e usare l’analizzatore per indagare.Se una asserzione non è verificata, l’analizzatore produrrà un contro esempio,ovvero tutte le istanze che non verificano l’asserzione.Se una proprietà desiderata, espressa con una asserzione non è contenuta nelmodello, in genere si spostare tale vincolo in proprietà strutturale del modello.Ad esempio vogliamo sapere "se esistono persone che possono hanno duemadri":assert twoMothers {no x : Persona | #(x.( ∼figlio)) > 1 } Sel’asserzione è corretta non vengono prodotte istanze del modello. Sel’asserzione è infranta sono prodotte le istanze che non verificano l’asserzione

10/5/2010 UNICAM - p. 37/38

Funzioni

Quando i fatti, i predicati o le asserzioni sono particolarmente complessi sipossono dichiarare delle funzioni che permettono di semplificare e renderemeglio leggibile i vincoli. Le funzioni con o senza parametri produconogeneralmente un valore che generalmente è un insieme.

Ad esempio se volessimo una funzione che produca tutti i figli di una personascriveremmo:fun sons [p : Person] : set Persona { p.figlio }

Mentre per produrre i fratelli:fun siblings [p : Persona] : set Persona { p.( ∼figlio).figlio }Da notare che l’ordine di valutazione degli operatori e da sinistra verso destra

10/5/2010 UNICAM - p. 38/38

Esercizi

▲ Lista. Realizzare una semplice lista con campi info di tipo intero e next.sig List { info : one Int, next one List} . Considerando lalista di tipo LIFO, definire il modello statico e successivamente leoperazioniinsert[List,Int] , erase[List]

▲ Pila. Realizzare una pila con un campo info di tipo intero.sig Pila { info : one Int, top one Pila} . Definire il modellostatico e successivamente le operazioni di push[Pila,Int] , pop[Pila] eempty[Pila]

▲ Albero binario. Realizzare un albero binario con un campo info di tipo intero.sig Tree {info : one Int, l,r : one Tree} . Considerandol’albero un albero binario di riecrca, definire il modello statico esuccessivamente le operazioni di insert[Tree,Int] , \find[Tree,Int]e erase[Tree,Int]