Dans la preuve de la justesse, une désignation indiquant que les assertions de sortie du programme découlent logiquement ses assertions d'entrée et les étapes de traitement.