Io-7-wyk-Slajd63

Implementacje 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.

<< Poprzedni slajd | Spis treści | Następny slajd >>