Χρήση βεβαιώσεων

Προγραμματίζουμε με σιγουριά αν εκφράζουμε τους αλγορίθμους μας με βάση:

Προϋποθέσεις
Μετασυνθήκες
Αναλλοίωτες συνθήκες (Invariants)
Συνθήκες σύγκλισης (Convergents)

Παράδειγμα

Είσοδος:
  Α(1..Ν): πίνακας ακεραίων
  N : ακέραιος
Έξοδος:
  Β(1..Ν): πίνακας ακεραίων

Προϋποθέσεις:
  Ν >= 1
Μετασυνθήκες:
  Β(1..Ν) περιέχει τις τιμές του Α(1..Ν)

Μεταβλητές
  Ι : Ακέραιος

I := 1
Όσο Ι <= Ν
  Β(Ι) := Α(Ι)
  Αναλλοίωτη συνθήκη: Β(1..Ι) := Α(1..Ι)
  Συνθήκη σύγκλισης: Ν - Ι
  Ι := Ι + 1
Τέλος

Σε στρατηγικά σημεία του κώδικα μπορούμε να εκφράζουμε τις παραπάνω έννοιες με τη βοήθεια μιας βεβαίωσης (assertion). Παράδειγμα:

void
arraycopy(int a[], int b[], int n)
{
assert(n >= 0);
// ...
}