Tipo astratto Officina

Si consideri la seguente specifica del tipo astratto Officina (dove Auto è un tipo astratto già definito):

TipoAstratto Officina

Domini

  

Officina

: dominio di interesse del tipo

Auto

: 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 nessuna auto

partitaIva(Officina o) $\mapsto$  String

 
pre: nessuna
post: RESULT è la partita IVA dell'officina o

arrivaAuto(Officina o, Auto a) $\mapsto$  Officina

 
pre: a non è presente nell'officina
post: RESULT è l'officina ottenuta da o aggiungendo l'auto a e attribuendo a tale auto lo status di inRiparazione

approntaAuto(Officina o, Auto a) $\mapsto$  Officina

 
pre: a è presente nell'officina ed ha con status inRiparazione
post: RESULT è l'officina ottenuta da o cambiando lo status dell'auto a in pronta

parteAuto(Officina o, Auto a) $\mapsto$  Officina

 
pre: a è presente nell'officina ed ha con status pronta
post: RESULT è l'officina ottenuta da o eliminando l'auto a

estInRiparazione(Officina o, Auto 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, Auto 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 (has-many) di tipo Auto (cfr. Unità 13).