Come descrivere cosa Andrea Polini -...

53
5. Modellare la specifica Come descrivere cosa Andrea Polini Ingegneria del Software Corso di Laurea in Informatica (Ingegneria del Software) 5. Modelli 1 / 49

Transcript of Come descrivere cosa Andrea Polini -...

5. Modellare la specificaCome descrivere cosa

Andrea Polini

Ingegneria del SoftwareCorso di Laurea in Informatica

(Ingegneria del Software) 5. Modelli 1 / 49

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 2 / 49

Materiale di studio

Carlo Ghezzi, Mehdi Jazayeri, Dino MandrioliFondamenti di Ingegneria del Software, 2a Ed. ItalianaPrentice Hall, 2004(Capitolo 5)

(Ingegneria del Software) 5. Modelli 3 / 49

Specifiche - generalità

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 4 / 49

Specifiche - generalità

Generalità

Una specifica termine piuttosto generale utilizzato in differenti fasi dellaproduzione del software.

In generale una specifica fornisce una precisa definizione dellecaratteristiche del “manufatto” che deve essere realizzato nelle fasisuccessive, fino a giungere all’implementazione.

Specifica dei requisiti contiene dunque una definizione dellecaratteristiche e delle funzionalità attese dal cliente.

(Ingegneria del Software) 5. Modelli 5 / 49

Specifiche - generalità

Il problema della specifica

Specifica dei requisiti in linguaggio naturale presenta diverseproblematiche e difficoltà di verifica.

linguaggio tecnicoambiguitàsinonimicompletezzainconsistenzacomprensibilità...

Il problema del significato

Pensate alle differenze con specifiche matematiche (e.g. addizione)

(Ingegneria del Software) 5. Modelli 6 / 49

Specifiche - generalità

Formalismi

Formalismo: notazione con precisa sintassi e sematica

Specifiche formali vengono definite attraverso l’uso di notazioni formali

Vantaggi principalicomprensione ?ambiguità ?completezza ?inconsistenza ?

Verifica formale: dato un formalismo ed una specifica formale èpossibile verificare esattamente se alcune proprietà valgono oppure nodirettamente “ragionando” sul modello.

(Ingegneria del Software) 5. Modelli 7 / 49

Specifiche - generalità

Specificheformali, informali, semiformali

Specifiche formali sono tipicamente costose da definire. In alcuni casipuò comunque essere utile poter avere specifiche più semplici ecomprensibili ad un più ampio “pubblico”

Si distingue dunque tra:Formalisemiformaliinformali

(Ingegneria del Software) 5. Modelli 8 / 49

Specifiche - generalità

SpecificheOperazionali vs. Descrittive

Le specifiche si distinguono in due grandi categorie:operazionali: descrivono un sistema attraverso il comportamentonecessario a raggiungere gli obiettividescrittive: descrivono proprietà del sistema che devono esserevere

Un esempio dal mondo matematico.

Un esempio nel mondo “informatico”

Come al solito le distinzioni non sono sempre nette!

(Ingegneria del Software) 5. Modelli 9 / 49

Specifiche - generalità

SpecificheOperazionali vs. Descrittive

Le specifiche si distinguono in due grandi categorie:operazionali: descrivono un sistema attraverso il comportamentonecessario a raggiungere gli obiettividescrittive: descrivono proprietà del sistema che devono esserevere

Un esempio dal mondo matematico.

Un esempio nel mondo “informatico”

Come al solito le distinzioni non sono sempre nette!

(Ingegneria del Software) 5. Modelli 9 / 49

Specifiche - generalità

SpecificheOperazionali vs. Descrittive

Le specifiche si distinguono in due grandi categorie:operazionali: descrivono un sistema attraverso il comportamentonecessario a raggiungere gli obiettividescrittive: descrivono proprietà del sistema che devono esserevere

Un esempio dal mondo matematico.

Un esempio nel mondo “informatico”

Come al solito le distinzioni non sono sempre nette!

(Ingegneria del Software) 5. Modelli 9 / 49

Specifiche - generalità

SpecificheOperazionali vs. Descrittive

Le specifiche si distinguono in due grandi categorie:operazionali: descrivono un sistema attraverso il comportamentonecessario a raggiungere gli obiettividescrittive: descrivono proprietà del sistema che devono esserevere

Un esempio dal mondo matematico.

Un esempio nel mondo “informatico”

Come al solito le distinzioni non sono sempre nette!

(Ingegneria del Software) 5. Modelli 9 / 49

Modelli Operazionali

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 10 / 49

Modelli Operazionali Data Flow Diagram (DFD)

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 11 / 49

Modelli Operazionali Data Flow Diagram (DFD)

Caratteristiche

DFD sono una notazione molto utilizzata per descrivere le funzioni diun sistema informativo e su come i dati fluiscono all’interno delsistema. Il sistema è in effetti visto come un insieme di funzioni chemanipolano dati.

Come possono essere manipolati i dati:I dati possono essere immagazzinati in repositoryI dati possono fluire all’interno del sistemaI dati possono entrare o uscire dal sistema

(Ingegneria del Software) 5. Modelli 12 / 49

Modelli Operazionali Data Flow Diagram (DFD)

Sintassi

Regole per combinare i simboli...

(Ingegneria del Software) 5. Modelli 13 / 49

Modelli Operazionali Data Flow Diagram (DFD)

Qualche esempio

dal mondo matematico (a + b) ∗ (c + a ∗ d)

Il distributore del caffèLa biblioteca

(Ingegneria del Software) 5. Modelli 14 / 49

Modelli Operazionali Data Flow Diagram (DFD)

Distributore del caffè

(Ingegneria del Software) 5. Modelli 15 / 49

Modelli Operazionali Data Flow Diagram (DFD)

Biblioteca

(Ingegneria del Software) 5. Modelli 16 / 49

Modelli Operazionali Data Flow Diagram (DFD)

Carenze dei DFD

Carenza nella definizione del controllo

Semantica ed arrichimento delle informazioni in un DFD

Abbiamo visto molti esempi di ambiguità

Formali? Semiformali? Informali?

(Ingegneria del Software) 5. Modelli 17 / 49

Modelli Operazionali Finite State Machines (FSM)

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 18 / 49

Modelli Operazionali Finite State Machines (FSM)

Caratteristiche

Una macchina a stati finiti è formalmente definita da una tupla<Q, I, δ,q0> dove:Q è un insieme di statiI è un insieme finito di inputδ è la funzione di transizione ( Q× I � Q )q0 ∈ Q è lo stato iniziale

Notazione grafica . . .

FSM sono particolarmente utili a modellare il controllo di un sistemasoftware.

(Ingegneria del Software) 5. Modelli 19 / 49

Modelli Operazionali Finite State Machines (FSM)

Qualche esempio

interruttorebuffer di lettura scrittura - un processo lettore, un processoscrittore ed un buffer di due posizioniil distributore di bevande calde - il distributore accetta monete da5, 10, 20, 50 cc ed 1c. La macchinetta eroga caffè al prezzo di40cc, tè al prezzo di 30cc, cioccolato 45cc. La macchinetta nonè capace di memorizzare un credito superiore ai 3c. Lamacchinetta da resto. Utilizzare un I/O FSM per modellare ildistributore.

(Ingegneria del Software) 5. Modelli 20 / 49

Modelli Operazionali Finite State Machines (FSM)

Questioni

Formali? semiformali? informali?

FSM sono molto usate per verificare formalmente proprietà dei sistemi

Una FSM si trova sempre in un solo stato e permette di specificaresoltanto uno stato successivo per una stessa azione. Allo stessotempo il sistema è un sistema sincrono che non ha attività concorrenti.

Esplosione degli stati (e.g. somma di due interi) ed estensione delformalismo di base. Memoria limitata dal numero degli stati.

Possibili estensioni. I/O FSM. Transizioni con guardia ed azioni.

(Ingegneria del Software) 5. Modelli 21 / 49

Modelli Operazionali Petri Nets (PN)

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 22 / 49

Modelli Operazionali Petri Nets (PN)

Reti di Petri

Le reti di Petri sono un formalismo ideato negli anni 60 per modellare sistemiconcorrenti, asincroni, distribuiti, paralleli, non deterministici, e/o stocastici.Formalmente sono definite da una tupla <P, T ,F ,W,M0>:

P è un insieme finito di piazze

T è un insieme finito di transizioni

F ⊆ {P × T } ∪ {T × P} è detta relazione di flusso della rete di Petri

W : F � N+ è la funzione peso che associa valore non nullo agli elementi di FM0 : P � N è la marcatura iniziale ed indica lo stato iniziale della rete di Petri

Deve poi valere che: P ∪ T 6= � e P ∩ T = �

In ogni momento lo stato di una rete di petri è indicato dalla funzione di marcatura cheassocia ad ogni piazza un numero naturale indicante il numero di “token” (gettoni)presenti nella piazza:M : P � N

(Ingegneria del Software) 5. Modelli 23 / 49

Modelli Operazionali Petri Nets (PN)

Reti di Petrinotazione grafica

Evoluzione di una rete di Petri:Data una transizione chiamiamo piazza di input (o di output), una piazzacollegata ad un flusso entrante (uscente) dalla transizione stessa.Una transizione è abilitata, e può dunque “sparare”, se e solo se TUTTE lepiazze collegate ad un qualsiasi flusso di input alla transizione, contengono unnumero di token maggiore o uguale al peso dell’elemento flusso che collegaognuna di loro alla transizione.Quando una transizione “spara” ogni piazza collegata ad un flusso uscente dallatransizione riceverà un numero di token pari al peso del corrispondente flusso.Le transizioni con nessun flusso entrante sono sempre abilitate.

(Ingegneria del Software) 5. Modelli 24 / 49

Modelli Operazionali Petri Nets (PN)

Petri Net

Tipicamente le piazze possono rappresentare una risorsa e l’accessoalla risorsa può essere modellato dalla presenza di Token. Allo stessomodo piazze e transizioni possono essere utilizzate per rappresentarestati di un processo e l’evoluzione dello stesso

Politiche di risoluzione dei conflitti non sono intrinseche nel formalismoma devono invece essere implementate. Ad esempio il formalismo nonè fair. Esempio....

Una rete di Petri si dice in deadlock se non ci sono transizioni abilitate.Nel caso in cui la rete di Petri si trovi in deadlock la sua marcaturarappresenterà lo stato finale delle rete. Esempio...

(Ingegneria del Software) 5. Modelli 25 / 49

Modelli Operazionali Petri Nets (PN)

Esempi

Buffer di due posizioniLettori/Scrittorifilosofi a cenaSemaforoCatena di montaggio

(Ingegneria del Software) 5. Modelli 26 / 49

Modelli Operazionali Petri Nets (PN)

Problemi e possibili estensioni al modelloFormalismo che si focalizza sul controllo. Comunque presenta alcune lacunein particolare per la gestione dei dati.

In particolare non è possibile modificare il flusso in dipendenza dei dati.

Non è possibile selezionare una transizione tra più transizioni attive.

Possibilità di specificare tempo e deadline.

Le reti di Petri sono state estese per poter modellare sistemi più complessi:

Token con associati valori. Token tipati e dunque gestione del contenuto.(Coloured Petri Nets - CPN)

Politiche di priorità. pri:T � N.

Reti di Petri temporizzate. Alle transizioni sono associati valori di tempominimo e massimo entro i quali la transizione, se abilitata, potrà sparare.

Reti temporizzate con associate funzioni di distribuzione (StochasticPetri Nets - SPN)

(Ingegneria del Software) 5. Modelli 27 / 49

Modelli Descrittivi

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 28 / 49

Modelli Descrittivi

Modelli Descrittivi

Questo tipo di modelli forniscono una formalizzazione del sistema intermini delle proprietà che questo soddisfa. Non viene descrittodirettamente il suo comportamento.

Diagrammi Entità Relazione (ER)Specifiche LogicheSpecifiche Algebriche

(Ingegneria del Software) 5. Modelli 29 / 49

Modelli Descrittivi Diagrammi Entità-Relazione

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 30 / 49

Modelli Descrittivi Diagrammi Entità-Relazione

Diagrammi Entità-Relazione

Descrizione concettuale della struttura dei dati e delle loro relazioni. Inrelazione a DFD:

Diversamente DFD si focalizzavano sul flusso del dato ma nonspecificavano la loro strutturaPossono essere utilizzati insieme per modellare diversi aspetti

Vengono modellati tre concetti fondamentali:EntitàAttributiRelazioni

(Ingegneria del Software) 5. Modelli 31 / 49

Modelli Descrittivi Diagrammi Entità-Relazione

Diagrammi Entità-Relazionenotazione grafica

ER non sono stati standardizzati, dunque molte varianti

In alcune varianti è permesso definire relazioni parziali

(Ingegneria del Software) 5. Modelli 32 / 49

Modelli Descrittivi Diagrammi Entità-Relazione

Limitazioni

Potere espressivo è piuttosto limitato. Concetti complessi di relazionenon possono essere rappresentati (anche se alcune variantipermettoni di rappresentare relazioni di ereditarietà tramite relazioni“is-a”)

Alcune varianti permettono di definire relazioni n-arie che comunquerisultano concettualmente e tecnicamente complesse da interpretareed implementare

Non è possibile specificare che un’entità esiste solo se il numero diistanze in una relazione sarà maggiore di un certo numero.

Come al solito poi per i problemi più “spinosi” sono proposteestensioni. In generale il diagramma viene complementato coninformazioni aggiuntive. Formali e non.

Diagramma delle classi ed ER

(Ingegneria del Software) 5. Modelli 33 / 49

Modelli Descrittivi Specifiche logiche

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 34 / 49

Modelli Descrittivi Specifiche logiche

Specifiche logichegeneralità

Utilizzo di formule FOT (First Order Theory) per descrivere proprietà diun programma

Una proprietà sarà soddisfatta se il corrispondente predicatoassumerà valore positivo.

FOT è un espressione che può comprendere:variabili (a, b, . . . )costanti numeriche (1, 3.4, 4.233e10, . . . )funzioni f (x , y , . . .), . . .predicati p(), . . .parentesi ( ), [ ], { }, . . .connettivi logici (∧, ∨, ¬,⇒, . . . )quantificatori (∀, ∃)

(Ingegneria del Software) 5. Modelli 35 / 49

Modelli Descrittivi Specifiche logiche

Specifiche logiche

Variabili libere e legate e dipendenza del valore di verità

Valore di verità dipende dal dominio scelto per le variabili della formula

Nel corso ci limiteremo a considerare specifiche di sistemi che terminano

Dato un programma P con input <i1, i2, . . . , in> ed output <o1, o2, . . . , om>una specifica logica per P è definita come:{Pre(i1, i2, . . . , in)}P{Post(o1, o2, . . . , om, i1, i2, . . . , in)}

Esercizi:

1 programma che calcola somma dei primi n numeri2 programma che genera permutazione di un vettore di ingresso3 programma che verifica che il primo elemento di un vettore sia duplicato

all’interno dello stesso4 . . .

(Ingegneria del Software) 5. Modelli 36 / 49

Modelli Descrittivi Specifiche logiche

Specifiche di parti

Specifiche logiche possono essere utilizzate anche per specificareparti di programma utilizzando le variabili stesse del programmaall’interno della specifica logica

Il caso di una classe nei linguaggi OO e le invarianti.Stato di un oggettoEsecuzione dei metodi e pre e post condizioni

{INV ∧ Pre(i1, i2, . . . , in)}m(i1, i2, . . . , in){INV ∧ Post(o1, o2, . . . , om, i1, i2, . . . , in)}

Esempio: vettore estendibile di elementi ordinati

(Ingegneria del Software) 5. Modelli 37 / 49

Modelli Descrittivi Specifiche logiche

Specifiche logicheconsiderazioni

Anche semplici programmi generano specifiche piuttosto complesse.

Definizione e riuso di formule permettono di semplificare la specifica

Spesso associate ad altri formalismi per aumentarne la potenzaespressiva.

(Ingegneria del Software) 5. Modelli 38 / 49

Modelli Descrittivi Specifiche logiche

Specifiche logiche e verifica

Utilizzando FOT viene specificato che per qualsiasi implementazionedi un programma o di un frammento di programma i predicati devonoessere valutati a vero

Espressioni logiche possono essere utilizzate nella fase di analisiapplicando deduzione logica. La proprietà espressa in forma FOTdeve poter essere derivata dalla specifica. Questo fornisce una prova!

Questo non era possibile per le specifiche operazionali con le quali èpossibile scoprire comportamento (simulazioni) ma non fornire prove.Ma . . . theorem proving è indecidibile in FOT

(Ingegneria del Software) 5. Modelli 39 / 49

Modelli Descrittivi Specifiche logiche

Specifiche logiche e verifica

Utilizzando FOT viene specificato che per qualsiasi implementazionedi un programma o di un frammento di programma i predicati devonoessere valutati a vero

Espressioni logiche possono essere utilizzate nella fase di analisiapplicando deduzione logica. La proprietà espressa in forma FOTdeve poter essere derivata dalla specifica. Questo fornisce una prova!

Questo non era possibile per le specifiche operazionali con le quali èpossibile scoprire comportamento (simulazioni) ma non fornire prove.Ma . . . theorem proving è indecidibile in FOT

(Ingegneria del Software) 5. Modelli 39 / 49

Modelli Descrittivi Specifiche logiche

Si supponga di voler specificare tramite formalismo logico la funzione (findInVect) che dato un vettore di interi di dimensionenon nulla non contenente duplicati, e dato un intero positivo, restituisce un dato astratto di tipo Result contenente due campipublici, found di tipo booleano e index di tipo intero. Tali campi assumeranno rispettivamente il valore true e l’indicecorrispondente alla posizione nel vettore nel caso in cui l’elemento cercato sia presente. Altrimenti i due campi assumerannorispettivamente valore false e−1 nel caso in cui l’elemento non sia presente nel vettore.Si definiscano dunque la Pre-condizione e la Post-condizione relativa alla seguente definizione della funzione:

findInVect(in:int VI[], in:int val, out:Result res)

dove il tipo Result risulta essere così definito:abstract data Result boolean found; int index;Nella definzione della specifica è possibile utilizzare l’operatore di . per accedere ai campi del tipo di dato astratto Result.Inoltre il meccanismo di accesso agli elementi del vettore VI[i] permette di indicare l’elemento i-esimo del vettore. È infinepossibile utilizzare la funzione length(in:int V[], out:int l) che dato un vettore in ingresso ne restituisce ladimensione.

Si utilizzi la funzione findInVect(...) sopra definita nella specifica della Pre- e Post-Condizione della funzionecheckAllValue così definita:

checkAllValue(in:int VI[], in:int upper, in:int lower, out:boolean check)

Tale funzione prende in ingresso un vettore di interi positivi e due interi positivi di cui il primo (upper) maggiore o uguale delsecondo (lower). Come risultato la funzione restituisce il valore true nel caso in cui tutti i valori compresi tra il primo ed ilsecondo valore siano presenti nel vettore. In caso negativo la funzione restituirà false.Nella definizione della funzione si utilizzi la funzione

removeDuplicate(in:int vi[], out:int vo[])

tale funzione dato un vettore che può contenere duplicati ne restituisce uno in cui i duplicati sono stati rimossi.

(Ingegneria del Software) 5. Modelli 40 / 49

Modelli Descrittivi Specifiche logiche

Uso di specifiche logiche

Modellare la macchinetta del caffèInsiemi: c:coins, d:drinks, t:time, n:intFunzioni: prices(d):c,Eventi: insertCoins(c,t), giveChange(t), selectDrink(d,t),readyDrink(d,t) . . .Stati: servingDrink(d,t1,t2), credit(c,t1,t2), availDrink(d,t1,n)

Descrivere relazioni e proprietàfunzionamentocredito costante finchè non c’è inserimento moneteselezione non disponibile durante servizio. . .

(Ingegneria del Software) 5. Modelli 41 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Sommario

1 Specifiche - generalità

2 Modelli OperazionaliData Flow Diagram (DFD)Finite State Machines (FSM)Petri Nets (PN)

3 Modelli DescrittiviDiagrammi Entità-RelazioneSpecifiche logicheSpecifiche algebriche (Cenni)

(Ingegneria del Software) 5. Modelli 42 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Specifiche algebriche (cenni)generalità

Formalismo descrittivo basato su definizione ed uso di algebre

algebre omogeneealgebre eterogenee

Molti sistemi software possono essere specificati “facilmente”utilizzando algebre eterogenee

(Ingegneria del Software) 5. Modelli 43 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Specifiche algebriche (cenni)esempio

Si vuole specificare un sistema che gestisce le stringhe. Con leseguenti operazioni:

creazione di una stringa vuotaconcatenazione di stringheaggiunta di un carattere ad una stringalunghezza di una stringaverifica se una stringa è vuota o menoverifica di uguaglianza di stringhe

Insiemi?

(Ingegneria del Software) 5. Modelli 44 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Specifiche algebriche (cenni)esempio

Definizione di algebra (sorts, segnatura, operazioni, vincoli)

La semantica delle operazioni viene data tramite equazioni chedefiniscono le proprietà fondamentali che devono valere quando leoperazioni sono applicate (assiomi)

Descrivere algebra con il linguaggio Larch:

algebra [name]imports [algebra list]introducessorts [sort list]operations

...constraints [operations list] so that

[name] generated by [ operations list ][constraints list]

(Ingegneria del Software) 5. Modelli 45 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Specifiche algebriche (cenni)vincoli

constraints isEmpty, append, new, add, equal, length so thatfor all [s,s1,s2:String;c:Char]

isEmpty(new()) = ?isEmpty(add(s,c)) = ?length(new()) = ?length(add(s,c)) = ?append(s,new()) = ?append(s1,add(s2,c)) = ?equal(new(),new()) = ?equal(new(),add(s,c)) = ?equal(add(s,c),new()) = ?equal(add(s1,c),add(s2,c)) = ?

(Ingegneria del Software) 5. Modelli 46 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Specifiche algebriche (cenni)derivazione di proprietà

Una proprietà è vera se può essere derivata dagli assiomi:

append(new(),add(new(),c) = add(new(),c)

append(new(),s) = s

(Ingegneria del Software) 5. Modelli 47 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Specifiche algebriche (cenni)proprietà non derivabili dagli assiomi

Capita spesso di poter incontrare proprietà che non possono esserederivate degli assiomi. Si consideri ad esempio la proprietà:equal(add(s,’a’),add(s,’b’)) = false

La specifica è incompleta e possono essere attuati tentativi di renderela specifica “più” completa aggiungendo altri assiomi.

(Ingegneria del Software) 5. Modelli 48 / 49

Modelli Descrittivi Specifiche algebriche (Cenni)

Specifiche algebriche (cenni)specifiche modulari

Sistemi complessi possono richiedere di definire molte algebre allostesso tempo.

Sono previsti operatori di “import” che permettono di includereun’algebra nella definizione di un’altra

(Ingegneria del Software) 5. Modelli 49 / 49