Io-7-wyk-Slajd63
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwaniaImplementacje niestandardowe
Załóżmy, że chcemy napisać specyfikację prostego pakietu wykonującego elementarne operacje arytmetyczne na liczbach naturalnych. Punktem wyjścia będzie dla nas aksjomatyczna definicja operacji arytmetycznych, którą można znaleźć w wielu książkach. Zawiera ona dwa aksjomaty. Po pierwsze, dodanie zera do dowolnej liczby x daje liczbę x.
W drugim aksjomacie występuje pojęcie następnika. Następnik jest to kolejna liczba naturalna względem podanej, np. następnikiem 2 jest 3, a następnikiem 3 jest 4. Niech funkcja succ(y) (od angielskiego „successor”, czyli następnik) podaje następnik liczby y.