Ťahák k zápočtu - Dátové štruktúry a algoritmy

Ťahák na zápočtovku, ale dobre poslúži aj na skúške.

Ukážka:

Formálna špecifikácia ADT prirodzené čísla
structure NATNO
declare ZERO() →natno
ISZERO(natno) →boolean
SUCC(natno) →natno
ADD(natno,natno) →natno
EQ(natno,natno) →boolean
for all x,y natnolet
ISZERO(ZERO) = true
ISZERO(SUCC(x)) = false
ADD(ZERO,y) = y
ADD(SUCC(x),y) = SUCC(ADD(x,y))
EQ(x,ZERO) = if ISZERO(x) then true else false
EQ(ZERO,SUCC(y)) = false
EQ(SUCC(x),SUCC(y)) = EQ(x,y)
end
end NATNO