Go backward to 2.3 Predicate Logic Go up to 2 The Language of Logic

2.4 Example

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).

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

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)

fun program(n) =
  such(p in nat(n, *(2, n)): isNextPrime(n, p), p);

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;
}