Re: Prime Number Program

Re: Prime Number Program

[Michael F Brenner]

In comp.land.ada #54048,
Jeff Habermann <jhabermann@earthlink.net> said:
    > Im tying to write a Program in Ada that finds the first 50 prime numbers.
    > Im having trouble with my for loops and array.  Any help will be very
    > appreciated.

This message will try to help with the loops. Note that the example given
here does not require an array.

The purpose of this message is not primarily to give working code for 
prime numbers, although filling in the body of the procedures
report and goldbach_conjecture_is_true below would create a 
computer program that prints out a bunch of prime numbers.

One way to reduce trouble with loops is to use a commenting style
that reflects the philosophy of <Edsger Dijkstra, The Discipline
of Programming>, which works in several steps.

Step 1. Before the loop, place either a comment or an assertion of
the Precondition of the loop. The precondition is a boolean 
expression which asserts that the computer memory is in the 
required state such that the loop will work. An assertion is
better because (by means of short-circuit operators or pragmas)
it is easy to turn the execution of the assertion on (for debugging
or for safety) and off (for efficiency). In the example below, the
loop uses a very unusual way of attempting to find the first 50 prime
numbers in an unsorted manner by means of the Goldbach conjecture.
It remains to be proven, that among the 458 prime numbers reported
by this program, whether each of the first 50 prime numbers actually
appears. Exercise for the reader: is this a function of the 
implementation of the Goldbach_conjecture_is_true function, or will 
it always include the first 50 prime numbers, or will it always be 
missing at least one of the first 50 prime numbers?
The loop desires to check every even number from 458 down to zero, 
to see if it satisfies the Goldbach conjecture. 
The precondition is that the number_under_test is 458,
and that the Goldbach conjecture is true for all prime numbers less
than or equal to 229, that is, all even numbers from 2 to 458. The
first part of the precondition appears as an assertion, and the
second part as a comment. 

Step 2. In the loop body, place the loop Exit condition, to guarantee that
the loop terminates. Some of the most interesting problems in computer
science are related to this step, and in some cases, there are loops
which never terminate. Even more interestingly, there are loops that we
do not know whether they terminate or not. This program, however, contains
a loop which we intend to terminate, and we know that it will terminate. 
This termination is celebrated with an exit statement, although
alternatives exist (such as for statements, raise statements, goto 
statements, abort statements, and infinite loops). In our example, 
we show our belief that the loop will terminate by two constructs: 
(a) we always subtract two from a number that started as an even number, 
and (b) we exit when the number reaches down to 2.

Step 3. In the loop body, document the loop Invariant condition. The loop
invariant condition is based on a metric which measures what has been
accomplished so far in the loop, or, contrapositively, what remains 
to be accomplished. Such a function might compute that we have accomplished
(458 - number_under_test) / 2 + 1
even number checks out of the 228 we intended to accomplish. The
alternative is to compute the function
  number_under_test/2 - 2
which is the number of loop iterations remaining.
A simple check on these two functions shows that they add up to 228,
which is the number of even numbers to be checked against the Goldbach
conjecture (since the loop exits when it reaches 2, without actually
checking the number 2 against Goldbach. Loop invariant conditions help
show why we believe that the loop terminates, why we believe the loop
is accomplishing our objective (to transmute the precondition into the
postcondition), and why we believe that the loop is as fast as we claim
it is (in this example, we claim that the loop executes in cubic time
because we intend to write Goldbach_conjecture_is_true in such a way
that it can check an integer for being the sum of two primes in 
quadratic time).

Step 4. Document the loop postcondition. In this example, the postcondition
is stated by a comment that the required numbers have been reported. 
However, this example is incomplete in three ways: report is missing,
Goldbach_conjecture_is_True is missing, and, most importantly, the proof
that this approach will not be missing any of the first 50 primes is 
missing. So this approach has NOT established the postcondition, but is
just an experiment that will eventually inspire us to prove or disprove
the attainment of the postcondition. Mostly, this example is just an
introduction to discussing what we need to think about when we code
a loop.

Example Code:    

  With text_io;
  with report;
  procedure prime_exercise is
    type exact_numbers is range 0..458;
    number_under_test: exact_numbers := 458;

    left, right: exact_numbers;
    Goldbach_conjecture_is_false: exception;

    procedure assert (condition: boolean) is
      assertion_failure: exception;
    begin
      if not condition then
        raise assertion_failure;
      end if;
    end assert; 

    function Goldbach_conjecture_is_true (for_integer: exact_numbers)
        return boolean is
      truth_value: boolean;
      left_value, right_value: exact_numbers;
    begin
      -- Fill in your code here to check the Goldbach conjecture.
      -- Set the variables left and right to the prime numbers
      -- which add up to the value of for_integer. Then set the
      -- truth_value to true. If the Goldbach conjecture fails
      -- on this number, then simply set truth_value to false,
      -- and redesign this program from scratch.

      left := left_value;
      right := right_value;
      return truth_value;
    end Goldbach_conjecture_is_true;
  
  begin
    -- Precondition 

    -- The Goldbach conjecture works on all integers from 2 to 458,
    -- as demonstrated by this program. 

    assert (number_under_test = 458);

    loop

      -- announce where we are up to

      text_io.put_line ("we are executing the loop");


      -- loop exit condition

      exit when number_under_test = 2; 

      if Goldbach_conjecture_is_true (for_integer => number_under_test) then
        report (left, right, number_under_test);
      else
        raise Goldbach_conjecture_is_false;
      end if;

      -- loop invariant condition: 
      -- We have tested all numbers from number_under_test .. 458
      -- against the Goldbach conjecture, and reported all of those
      -- as Goldbach numbers generated from primes, if they indeed
      -- were generated from prime numbers, as Goldbach conjectured. 
      -- That is to say, the loop has been executed exactly           
      --     (458 - number_under_test) / 2 + 1 
      -- times, in an amount of time not exceeding O(number_under_test**3).

      number_under_test := number_under_test - 2; 

    end loop; 
    -- Postcondition: 
    -- This program has now printed out 458 prime numbers, which when
    -- sorted, and duplicates are eliminated, are shown to be exactly
    -- the first 50 prime numbers.

    -- Comment on the Postcondition:
    -- The discussion above and the comments in this code do not 
    -- establish that it is possible to write the Goldbach_conjecture_is_true
    -- function in a manner that guarantees the postcondition. 
    -- Proving that this is possible (preferably by construction) would
    -- be necessary before believing that this postcondition will be
    -- realized. Therefore, at this point in the code, the reported
    -- outputs should actually be sorted, duplicated eliminated, and
    -- the results should be counted. To make sure there are 50 unique
    -- prime numbers among them.
  end prime_exercise;