Ťahák1 s. / 2. roč. / pdf
Ťahák na zápočtovku, ale dobre poslúži aj na skúške.Ukážka:Formálna špecifikácia ADT prirodzené číslastructure NATNOdeclare ZERO() →natnoISZERO(natno) →booleanSUCC(natno) →natnoADD(natno,natno) →natnoEQ(natno,natno) →booleanfor all x,y natnoletISZERO(ZERO) = trueISZERO(SUCC(x)) = falseADD(ZERO,y) = yADD(SUCC(x),y) = SUCC(ADD(x,y))EQ(x,ZERO) = if ISZERO(x) then true else falseEQ(ZERO,SUCC(y)) = falseEQ(SUCC(x),SUCC(y)) = EQ(x,y)endend NATNO