Si consideri la seguente specifica del tipo astratto Officina
(dove Mezzo è una classe già definita):
- TipoAstratto Officina
-
- Domini
-
- Officina
- : dominio di interesse del tipo
- Mezzo
- : dominio degli oggetti presenti nell'officina
- Funzioni
-
- crea(Stringa pi) Officina
-
pre: nessuna
post: RESULT è un'officina avente pi
come partita IVA e con nessun mezzo
- partitaIva(Officina o) String
-
pre: nessuna
post: RESULT è la partita IVA dell'officina
o
- arrivaMezzo(Officina o, Mezzo a) Officina
-
pre: a non è presente nell'officina
post: RESULT è l'officina ottenuta da o
aggiungendo il mezzo a e attribuendo a tale mezzo lo status di
inRiparazione
- approntaMezzo(Officina o, Mezzo a) Officina
-
pre: a è presente nell'officina ed ha con status
inRiparazione
post: RESULT è l'officina ottenuta da o
cambiando lo status del mezzo a in pronta
- parteMezzo(Officina o, Mezzo a) Officina
-
pre: a è presente nell'officina ed ha con status
pronta
post: RESULT è l'officina ottenuta da o
eliminando il mezzo a
- estInRiparazione(Officina o, Mezzo a) Boolean
-
pre: nessuna
post: RESULT è true se se a è presente
nell'officina o ed ha lo status inRiparazione;
false altrimenti
- estPronta(Officina o, Mezzo a) Boolean
-
pre: nessuna
post: RESULT è true se a è presente
nell'officina o ed ha lo status pronta;
false altrimenti
- FineTipoAstratto
-
Si noti che Officina è un tipo astrazione di entità che è in
relazione con molti oggetti di tipo Mezzo.