logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-06112020-111206


Tipo di tesi
Tesi di laurea vecchio ordinamento
Autore
PAPA, ANGELA
URN
etd-06112020-111206
Titolo
La correttezza dei programmi in Java: asserzioni e sistemi per il Design by Contract
Dipartimento
INFORMATICA
Corso di studi
SCIENZE DELL'INFORMAZIONE
Relatori
relatore Prof. Bellia, Marco
Parole chiave
  • asserzione
  • contratto
  • correttezza
  • design by contract
  • invariante
  • java
  • postcondizione
  • precondizione
  • principio di sostituzione
  • sottoclasse
Data inizio appello
26/06/2020
Consultabilità
Tesi non consultabile
Riassunto
Le asserzioni, come formule della logica dei predicati, possono esprimere requisiti funzionali dei programmi e proprietà all'interno del loro codice. Nella tesi sono descritte le metodologie per l'uso di asserzioni eseguibili nel linguaggio Java, attraverso l'istruzione assert, o con l'ausilio dei costrutti del Design by Contract (progettazione per contratto) per la specifica di classi e metodi e nella definizione di sottoclassi. Insieme ai vantaggi, sono discussi i problemi legati all'integrazione dei contratti nel linguaggio e alle loro applicazioni, anche in vista di possibili sviluppi ed evoluzioni. La natura di questi controlli, che è possibile abbinare al testing, favorisce lo sviluppo e il riuso di componenti software. In assenza di particolari criticità, pur non avendo l'efficacia dei metodi di verifica formale, i controlli dinamici possono essere applicati a svariati programmi, anche di grandi dimensioni, e contribuire alla loro correttezza, individuando la presenza di errori durante l'esecuzione.
File