Lezione 15 – Complementi sul
linguaggio Z (1)
Ingegneria del software
Modulo 1 - Introduzione al processo software
Unità didattica 3 - Modelli di fase d’analisi
Ernesto Damiani
Università degli Studi di Milano
Specificazione di modello astratto
• Descrive esplicitamente il comportamento di un
sistema nei termini di un modello, usando tipi
ben definiti (sequenze, relazioni, funzioni), e
definisce le operazioni mostrando gli effetti sul
modello
• La specificazione include:
– tipo: natura dell’oggetto specificato
– modello: struttura sottostante
– invariante: proprietà dell’oggetto modellato
– pre/post condizioni: semantica delle operazioni
Notazione
• Viene usata per testare i risultati
• È indipendente dal codice di programma
• Si basa su un modello matematico
• Rappresenta aspetti sia statici sia dinamici di un
sistema
Caratteristiche (notazione Z)
• Scomporre la specificazione in piccole parti
(schemi)
• Gli schemi vengono usati per descrivere gli
aspetti sia statici sia dinamici del sistema
• Si possono ignorare i dettagli per focalizzarsi
sugli aspetti del problema che interessano
Schema (1)
Aspetti statici
• Lo stato in cui si trova il sistema
• I predicati invarianti che vengono mantenuti
mentre il sistema si muove da stato a stato
Schema (2)
Aspetti dinamici
• Le operazioni che sono possibili
• Il rapporto tra input e output
• Il cambiamento di stato che si verifica in seguito
a una transizione
Esempio di notazione
Esempio (1)
Esempio (2)
Race condition
• Non abbiamo gestito la condizione quando l’utente
cerca di aggiungere un compleanno, che è già
noto al sistema o cerca di trovare il compleanno di
qualcuno che è sconosciuto
• Si gestisca ciò aggiungendo un risultato extra! A
ogni operazione
• Risultato := of| already_known | not_known
FINE