(1) En formel teknik, der bruges til at bevise matematisk, at et edb-program opfylder sin angivne requirements.~(2) et bevis, som er et resultat af anvendelsen af teknik i (1).