Tipo astratto Officina

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) $ \mapsto$  Officina
 
pre: nessuna
post: RESULT è un'officina avente pi come partita IVA e con nessun mezzo
partitaIva(Officina o) $ \mapsto$  String
 
pre: nessuna
post: RESULT è la partita IVA dell'officina o
arrivaMezzo(Officina o, Mezzo a) $ \mapsto$  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) $ \mapsto$  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) $ \mapsto$  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) $ \mapsto$  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) $ \mapsto$  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.