• asserzione
• contratto
• correttezza
• design by contract
• invariante
• java
• postcondizione
• precondizione
• principio di sostituzione
• sottoclasse

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.