   Go backward to 2.3 Predicate LogicGo up to 2 The Language of Logic ## 2.4 Example

We demonstrate the beauty and usefulness of the language of logic on a simple example. Suppose we are given the following problem statement:
Write a program that takes a number and returns the next prime number.

Specification  The task can be formally specified as follows:

• Input: n such that isNumber(n);
• Output: p such that isNextPrime(n, p).
Here isNumber is the input condition (Eingabebedingung), a unary predicate that describes the property that every well-formed input n has; isNextPrime is the output condition (Ausgabebedingung), a binary predicate that describes how the output p shall be related to n. Our goal is to construct these two conditions.

As for the input condition, we can reasonably assume from the problem statement that the input is a natural number. We denote by N the set of natural numbers and define

isNumber(n) : <=> n in N
using the set theoretic predicate ` in ' ("is element of") to be introduced in the next chapter and the notion `: <=> ' to define a new predicate.

The output condition is a bit more complicated. Apparently, the result p shall be again an object of the same kind as input n; but it shall be also a prime and it shall be the "next" such number. Thus we define

isNextPrime(n, p) : <=> isNumber(p) /\  isPrime(p) /\  isNextP(n, p).

A natural number p greater than 1 is a prime if and only if there is no number n between 1 and p that divides p

 isPrime(p) : <=> 1 < p /\ ~(exists 1 < n < p: n | p).

This can be written a bit more elegantly as

 isPrime(p) : <=> 1 < p /\ forall 1 < n < p: n not | p.

The number n divides m if there exists some p such that the product of n and p is m:

n | m : <=> exists p: n*p = m.

Thus we have reduced the description of the predicate isPrime to formulas that only use the function constant * and the predicates = and < with their usual interpretation on natural numbers.

Now we proceed to the question what n's next prime p is. A little thinking reveals that the notion "next" intends to express that there is no other number between n and p that is also a prime. But what if n is itself prime? Shall we then return n itself or the smallest prime greater than n? The natural language term "next" is somewhat ambiguous in this respect, so we discuss with our client and learn that the first interpretation is the desired one. Thus we write:

 isNextP(n, p) : <=> n <= p /\ ~(exists n <= q < p: isPrime(q)).

The predicate isNumber is rather trivial and the predicate isNextP in isolation does not describe a very interesting property; thus we insert the corresponding formulas to yield the final specification:

• Input: n in N;
• Output: p in N such that isNextPrime(n, p).
 isNextPrime(n, p) : <=> n <= p /\  isPrime(p) /\ ~(exists n <= q < p: isPrime(q)) isPrime(p) : <=> 1 < p /\ forall 1 < n < p: n not | p n | m : <=> exists p: n*p = m.

These predicates can be defined in the Logic Evaluator as follows:

```pred <(m, n) <=> and(<=(m, n), not(=(m, n)));
pred divides(n, m) <=> exists(p in nat(1, m): =(*(n, p), m));
pred isPrime(p) <=>
and(<(1, p),
forall(n in nat(2, -(p, 1)): not(divides(n, p))));
pred isNextPrime(n, p) <=>
and(<=(n, p), isPrime(p),
not(exists(q in nat(n, -(p, 1)): isPrime(q))));
```

The only difference to the mathematical definitions is that we have to explicitly restrict the range of the existentially quantified variable p in the definition of `divides` (which is easy, because any divisor of m is in the range [1...m]).

We can use these definitions to check the validity of input/output pairs:

We will now use the "such" quantifier

````such(x: A, T)`
```
which returns a value of term T such that A holds (for some value of x, provided that such an x exists). With the help of this quantifier we can define a function
```fun program(n) =
such(p in nat(n, *(2, n)): isNextPrime(n, p), p);
```
We restrict our search for the next prime to the range [n...2n] applying the mathematical knowledge that between every number and its double there exists at least one prime number. Thus we can simulate a program that satisfies our specification:

Operational Interpretation  From the formal specification constructed above, one can already derive a straight-forward program that solves the stated problem. We recall the operational interpretations of formulas introduced in the previous sections and encode every formula (forall a <= x <= b: A) as the following piece of code

```boolean forallX = true;
for (int x = a; x <= b; x++)
{
// value of A(x)
boolean isTrue = ...;
...

if (!isTrueA)
{
forallX = false;
break;
}
}
```

Then the variable `forallX` is true after the termination of the loop if and only if the universal formula is true.

Correspondingly, we can encode (exists a <= x <= b: A) as

```boolean existsX = false;
for (int x = a; x <= b; x++)
{
// value of A(x)
boolean isTrue = ...;
...

if (isTrueA)
{
existsX = true;
break;
}
}
```

Here the variable `existsX` is true after the termination of the loop if and only if the existential formula is true.

Based on this idea, we implement the predicates as the following Java methods:

```// -------------------------------------------------------
// divides(m, n) :<=> (exists p in 1..n: m*p = n)
// -------------------------------------------------------
boolean divides(int m, int n)
{
// exists p in 1..n
boolean existsP = false;
for (int p = 1; p <= n; p++)
{
// m*p = n
boolean equalsMPN = (m*p == n);
if (equalsMPN)
{
existsP = true;
break;
}
}
return existsP;
}

// -------------------------------------------------------
// isPrime(p) :<=>
//   1 < p /\
//   (forall n in 2..p-1: ~divides(n, p))
// -------------------------------------------------------
boolean isPrime(int p)
{
// p > 1 /\
if (p > 1)
{
// forall n in 2..p-1
boolean forallN = true;
for (int n = 2; n <= p-1; n++)
{
// ~divides(n, p)
boolean notDividesNP = !divides(n, p);
if (!notDividesNP)
{
forallN = false;
break;
}
}
return forallN;
}
else
return false;
}

// -------------------------------------------------------
// isNextPrime(n, p) :<=>
//   n <= p /\ isPrime(p) /\
//   ~exists(q in n..p-1: isPrime(q))));
// -------------------------------------------------------
boolean isNextPrime(int n, int p)
{
// n <= p /\
if (n <= p)
{
// isPrime(p) /\
if (isPrime(p))
{
// ~exists q in nat(n, p-1):
boolean existsQ = false;
for (int q = n; q <= p-1; q++)
{
boolean isPrimeQ = isPrime(q);
if (isPrimeQ)
{
existsQ = true;
break;
}
}
if (existsQ)
return false;
else
return true;
}
else
return false;
}
else
return false;
}

// -------------------------------------------------------
// program(n) := such(p in n..2*n: isNextPrime(n, p))
// -------------------------------------------------------
int program(int n)
{
for (int p = n; p <= 2*n; p++)
{
if (isNextPrime(n, p))
return p;
}
return -1; // not reached
}
```

While above program solves the stated problem, a little bit of thinking reveals that we can do this more efficiently. The first prime number found is exactly the wanted "next" prime such that we do not need an extra check for this property. Thus we write:

```// ------------------------------------------------------
// program(n) := such(p in n..2*n: isPrime(p))
// ------------------------------------------------------
int program(int n)
{
for (int p = n; p <= 2*n; p++)
{
if (isPrime(p))
return p;
}
return -1;
}
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   