Tekst źródłowy strony Niestandardowy model liczb naturalnych

Klasa NSN przytoczona poniżej spełnia aksjomaty liczb naturalnych z operacją dodawania, ale wykonywanie algorytmu Euklidesa w środowisku zdefiniowanym przez tę klasę nie zawsze kończy się po skończonej liczbie kroków.

Czego dowodzi ten przykład?

Do udowodnienia poprawności algorytmu Euklidesa potrzebny jest inny zestaw własności (niezmienników, aksjomatów) liczb naturalnych. Poniżej przytoczone specyfikacje (''inaczej'' interface, aksjomatyzacje) liczb naturalnych nie wystarczają. 
------

'''program''' NonstandardNaturalNumbers;

:   '''unit''' NSN: Nat '''class'''(cecha,licznik, mianownik: integer);
::      '''unit''' '''virtual'''  add: '''function'''(m: NSN) : NSN;
::      '''begin'''
:::          result:= '''new''' NSN(cecha+m.cecha, licznik*m.mianownik+mianownik*m.licznik)
::      '''end''' add;
::      '''unit virtual''' isequal: '''function'''(n: NSN): Boolean;
::      '''begin'''
:::         result := (cecha=m.cecha) and (licznik*m.mianownik=mianownik*m.licznik)
::      '''end''' isequal;
  
:   '''begin'''
::      '''if''' licznik=0 '''and''' cecha <0 '''then''' raise Exception '''fi''';
::      '''if''' licznik < 0 '''then''' '''raise''' Exception '''fi''';
::      '''if''' mianownik =0 '''then''' '''raise''' Exception '''fi'''
:   '''end''' NSN;

:   unit Nat: class; (* specyfikacja 1sza *)
::      unit virtual add: function(x:Nat): Nat; end add;
::      unit virtual isequal: function(x:Nat): Boolean; end isequal; 

:     (* -------------------------------------------------------- *)
:     (*  forall n in Nat,  not( n.add(one).isequal(zero)
:         forall n,m in Nat not n.isequal(m) implies not n.add(one).isequal(m.add(one))
:         dla kazdej formuły alpha(x)
:            {alpha(x/zero) and forall n [alpha(n) implies alpha(n.add(one))]} implies forall n alpha(n)
:     *)
:   end Nat; 
   
:   unit Nat2: class; (* specyfikacja 2sza *)
:      unit virtual add: function(x:Nat): Nat; end add;
:      unit virtual isequal: function(x:Nat): Boolean; end isequal; 
 
:     (* INVARIANTS *) 
:     (* -------------------------------------------------------- *)
:     (*  forall n in Nat,  not( n.add(one).isequal(zero)
:         forall n,m in Nat not n.isequal(m) implies not n.add(one).isequal(m.add(one))
:         INNY SCHEMAT zob. A. Grzegorczyk Zarys Arytmetyki Teoretycznej, PWN, Warszawa, 1971, str.239
:     *)
:   end Nat2; 
   
::   (* Tw. Te dwie specyfikacje są równoważne i zupełne  *)
   
:   '''var''' (* final *) zero, one: Nat;
'''begin''' (* main *)
:   zero := '''new''' NSN(0, 0,1);
:   one := '''new''' NSN(1,0,1);
   
'''end'''
-------
'''Twierdzenie'''
''Zbiór obiektów klasy NSN wraz z metodami .add i .isequal spełnia aksjomaty liczb naturalnych z dodawaniem, w tym wszystkie formuły schematu indukcji''.

Dowód można znaleźć w książce Andrzeja Grzegorczyka.