Come descrivere cosa Andrea Polini -...
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