Le implementazioni dei metodi soddisfano la specifica

• si ragiona usando la funzione di astrazione

  • un metodo alla volta

• ciò è possibile solo perché abbiamo già dimostrato che il rep invariant è soddisfatto da tutte le operazioni

  • il rep invariant cattura le assunzioni comuni fra le varie operazioni
  • permette di trattarle separatamente

Previous slide

Next slide

Back to first slide

View graphic version