I think the confusion you're having is because in the Fibonacci example it is specifying what the Fibonacci function is by one way to calculate it. Try the foll

I think the confusion you're having is because in the Fibonacci example it is specifying what the Fibonacci function is by one way to calculate it. Try the following natural number division example instead. In this example the spec doesn't show how to calculate the function: spec: Function NatDiv implements a "division" function that given two natural numbers "dividend" and "divisor" (with the guarantees that "divisor" < "dividend" and "divisor" is not 0) either- 1) returns "quotient" an integer such that either quotientdivisor = dividend (here quotient will obviously be >=0), or, if no such number exists, returns "-1", 2) always terminates. where we assume your computer's hardware doesn't have an inbuilt division operation but has at least natural number addition, along with common comparison operations (eg: <, equality, etc) and logic ops (eg: OR, AND, NOT, etc). Notice that here the spec doesn't specify the function by detailing what it does. In fact it specifies the division function by using multiplication which is the opposite of division. And we're not even guaranteed that our hardware has multiplication- so the spec itself gives no detail how to compute the division. One possible NatDiv implementation: define two variables- counter and sum and set to 0. Create a while loop where the while condition to enter inside the loop is that sum is less than dividend's value. Inside the loop in each iteration sum is increased by divisor's value and counter is incremented. So when the loop terminates sum is greater than or equal to dividend's value. The function returns counter's value if sum = dividend or returns "-1" otherwise. Notice that we can argue that the loop always terminates because sum can only increase inside the loop while the value of dividend never changes thus eventually the loop condition will eventually fail to hold at some point. And when it terminates counterdivisor=sum (by the fact that multiplication of ab is equivalent to summing "a" occurrences of "b") and that counter is returned when sum=dividend or -1 is returned otherwise. Thus the requirements of the spec are satisfied. *in reality, the spec would have to account of the size limitations of the physical machine- but here we're unrealistically assuming that it can handle any sized natural numbers.