From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,e4346b721a16eb9c X-Google-Attributes: gid103376,public From: mfb@mbunix.mitre.org (Michael F Brenner) Subject: Re: Prime Number Program Date: 1996/12/03 Message-ID: <581m9r$dfi@top.mitre.org> X-Deja-AN: 202258250 references: <01bbe0a9$b31f7a20$d4cc95ce@jeff> organization: The MITRE Corporation keywords: precondition, invariant condition, postcondition, exit condition newsgroups: comp.lang.ada summary: Fixing troubles with loops Date: 1996-12-03T00:00:00+00:00 List-Id: In comp.land.ada #54048, Jeff Habermann 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 , 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;