Reading material

Pages 97-99.

Additional material

The Java Modelling Language

Implementation of a queue by means of an array and an integer.

val c = 10; (* capacity of the array *)
val v = 0;  (* value initially stored in the array cells *)

val empty = (Array.array(c, v), 0); (* empty queue *)
fun add(x, (a, i)) = ((Array.update(a, i, x); a), i+1);
local
  fun left(a, j, i) = 
    if (j = i+1) then a 
    else left((Array.update(a, j-1, Array.sub(a, j)); a), j+1, i)
in
  fun drop(a, i) = (left(a, 1, i), i-1)
end;
fun front(a, i) = Array.sub(a, 0);

Computing the Fibonacci series

fun fib(0) = 1
  | fib(1) = 1
  | fib(n) = fib(n-1) + fib(n-2)

local
  fun itfib(n, prev, curr) =
    if n = 0 then prev
    else itfib(n-1, curr, curr+prev)
in
  fun fib(n) = itfib(n, 0, 1)
end

Question

Give a pre- and postcondition for
public static int fib(int n)
{
    int prev = 0;
    int curr = 1; 
    for (int i = 0; i < n; i++) 
    {
        int temp = curr;
        curr = prev + curr;
        prev = temp; 
    }
    return prev;
}