Poprawnosc specyfikacji

W jaki sposób formalnie można sprawdzać poprawność specyfikacji ?

Np. dla:
x >= 0 (warunek wstępny)
x = x+1
x >= 1 (warunek końcowy)

Jak określić jej poprawność.

przyjmijmy najmniejsze dopuszczalne x z pierwszego warunku czyli 0. Następnie mamy x = x (czyli 0) +1, czyli x jest od teraz równe 1, i spełnia drugi warunek. Biorąc pod uwagę warunki i sam algorytm, dla każdego x większego od 0 (czyli spełniającego pierwszy warunek), też będzie poprawny (bo liczba dodatnia po dodaniu jedynki nie może być mniejsza od jedynki, nawet jak będzie to 0.000000000000000000000001).

No, tak to oczywiście prawda. Ale to można tak zapisywać czy trzeba jakoś formalnie ?

To na uczelnie, zadanie do zrobienia samodzielnie, nie było żadnych dodatkowych informacji.

Dziękuję za odpowiedź :)