Nella prova di correttezza, una denominazione che indica che un programma uscita asserzioni logicamente seguono dal suo ingresso asserzioni e fasi di lavorazione, e che, inoltre, il programma termina sotto tutti specificate condizioni di ingresso.