Computation Models and Design by Refi nement 111
Algorithm design and analysis We can now develop a functional algorithm for primality testing
based on the Fermat’s Little theorem. We start by defi ning an iterative function prime(n, q) of the type
prime : P × N → {true, false}, where n is the number whose primality is to be tested and q is the maximum
number of times the Fermat’s test is to be applied.
prime(n, q) =
if 2
_(,
, )otherwise
true n
prime test n q false
=
⎧
⎨
⎩
where the iterative function prime test : P × N × {true, false} → {true, false} is defi ned using the invariant
P = (¬ failed = (n has passed the Fermat’s test (q
0
− q) times) )
(where q
0
is the initial value of q) as
prime_test(n, q, failed) =
if 0
if failed
_(,1, _())otherwise
true