Hoare-Calculus

[Nicole Gruber]

Can someone please explain to me how the Hoare-Calculus works??? Take this exercise for example:

 // precondition: 0 <= n 
i = 0;
x = 1;
while(i < n)
{
   i = i + 1;
   x = i * x;
}
// postcondition: x == n!
 

n, i , x are int and the notation n! = factorial

[Campbell Ritchie]

You can't find any books by Tony Hoare? See if you can get your hands on:
Hoare, CAR. (Charles Antony Richard), 1934-
Essays in computing science / CAR. Hoare ; C.B. Jones (editor).
Prentice Hall International series in computer science
New York ; London : Prentice Hall, 1989.
ISBN 0132840278 :
Physical details xii,412p : ill. ; 25 cm.
Bibliography: p393-397. - List of works by CAR. Hoare: p398-404. - Includes index.

It includes a reprint of the article about correctness.

A substitution S can require a precondition P to produce a result (or postcondition) Q. So, in your example, the substitution is supposed to establish the result/postcondition Q and Q is (x == n!). So you can work back from Q via S to work out what P is. You have actually got the mathematically correct value, but if you are using Java int arithmetic, you would actually want (n <= 12 && n >= 0). If you try to calculate 13! you overflow the limits of int arithmetic.
You now can write a Hoare triplet P[S]Q which means if P is true, then S will establish Q.
There are various ways you can implement this. The simplest is

/**
 * @param n The number whose factorial we wish to calculate.
 * Requires a non-negative argument.
 */

This is a plain simple precondition, which is stated; if the precondition is not fulfilled then the program is under no obligation to supply the correct answer, not even under any obligation to terminate or provide a result at all.

The next way up is rather more assertive, and even less friendly to the user.

/**
 * @param n The number whose factorial we wish to calculate.
 * Requires a non-negative argument.
 */
 public static int factorial(int n)
 {
    while (n < 0);
    . . .
    return x;
 }

This is equivalent to saying, " if you get it wrong I shall mess up your program by going into an infinite loop." This is permissible under the strict rules of engagement: no precondition no result.

Even more assertive, and what most people would regard as good programming practice, is to strengthen the precondition into a guard. My previous example was a bit like that, but this next example is easier to use because it returns what is obviously an impossible result. I wouldn't use this myself, but let's see what it does.

/**
 * @param n The number whose factorial we wish to calculate.
 * Requires a non-negative argument.
 * @return The factorial if a correct argument was supplied, otherwise -1.
 */
 public static int factorial(int n)
 {
    int x = -1;
    if (n >= 0);
    {
       x = 1;
        . . .
    }
    return x;
 }

That requires the user to check for an incorrect and impossible return value. As I said you are using the precondition as a guard, which can be written G---->[S]Q. If the guard is not fulfilled S never runs at all.

This last method, which is what I would use, looks like this

/**
 * @param n The number whose factorial we wish to calculate.
 * Requires a non-negative argument.
 * @throws IllegalArgumentException if the argument is negative.
 */
 public static int factorial(int n)
 {
    if (n < 0)
    {
        throw new IllegalArgumentException("factorial method: negative argument passed.");
    }
    . . .
    return x;
 }

This makes it clear to the user that S has never run at all. If there is a wrong argument, then either the user has to catch the Exception, or the application [more precisely the thread] will stop.
This is a very assertive guard, which builds on and enforces the precondition, and ensures that only correct values are returned.

I shall write about your postcondition very soon.

[Campbell Ritchie]

So far, so good. I had to call the middle step S; Hoare actually uses the first letter of Ritchie, but for reasons explained here you cannot use that letter on its own on JavaRanch.

So far we have seen that the precondition is part of the instructions for using the method/program, and failing to fulfil the precondition will preclude and excuse the program from providing the correct answer, or from providing an answer at all, or from starting to run or from terminating. We now have a method which looks like this

    /** 
     * @param n The number whose factorial we wish to calculate. 
     * Requires a non-negative argument. 
     * @throws IllegalArgumentException if the argument is negative. 
     */  
    public static int factorial(int n)  
    {  
        if (n < 0)  
        {  
            throw new IllegalArgumentException("factorial method: negative argument passed.");  
        }  
        //       . . .  
        return x;  
    }

Let us now enhance it by giving it a method body

    /** 
     * @param n The number whose factorial we wish to calculate. 
     * Requires a non-negative argument.
     * @return The factorial of n
     * @throws IllegalArgumentException if the argument is negative. 
     */  
    public static int factorial(int n)  
    {  
        if (n < 0)  
        {  
            throw new IllegalArgumentException("factorial method: negative argument passed.");  
        }  
        int i = 0;
        int x = 1;
        while (i < n)
        {
            i = i + 1;
            x = i * x;
        }
        return x;  
    }

You will now recognise that as your own code. Now it may be useful to check that you have fulfilled the postcondition. I shall use assertions, which are suitable for testing, but are normally disabled in deployed code. Let us assume you have some other method, let's call it factorial2(int) which you are confident calculates (or records) factorials accurately. Let us add an assertion to that method.

    /** 
     * @param n The number whose factorial we wish to calculate. 
     * Requires a non-negative argument.
     * @return The factorial of n
     * @throws IllegalArgumentException if the argument is negative. 
     */  
    public static int factorial(int n)  
    {  
        if (n < 0)  
        {  
            throw new IllegalArgumentException("factorial method: negative argument passed.");  
        }  
        int i = 0;
        int x = 1;
        while (i < n)
        {
            i = i + 1;
            x = i * x;
        }
        assert x == factorial2(n) : "Calculated " + n + "! = " + x + ". Correct value is " + factorial2(n);
        return x;  
    }

That assert statement will throw an Exception if that assertion fails to return true to the left of the : with the message on the right of the : passed as the message to the Exception. Let's expand that example and introduce a second method.

    /** 
     * @param n The number whose factorial we wish to calculate. 
     * Requires a non-negative argument.
     * @return The factorial of n
     * @throws IllegalArgumentException if the argument is negative. 
     */  
    public static int factorial(int n)  
    {  
        if (n < 0)  
        {  
            throw new IllegalArgumentException("factorial method: negative argument passed.");  
        }  
        int i = 0;
        int x = 1;
        while (i < n)
        {
            i = i + 1;
            x = i * x;
        }
        assert x == factorial2(n) : "Calculated " + n + "! = " + x + ". Correct value is " + factorial2(n);
        return x;  
    }
    
    private static int factorial2(int n)
    {
        return n <= 1 ? 1 : n * factorial2(n - 1);
    }

As long as you pass non-negative arguments < 13 you will get the correct answer, and the assertion will always return true, confirming that the postcondition has been correctly fulfilled. [I think that you will get the same error if you pass a larger argument, so that example will overlook the error.]

Remember you have to use the -ea command line option or the assertions will be disabled.

Final version: I have introduced line 20. Try running this lot with assertions enabled, and this will demonstrate that your postcondition has not been fulfilled.

    /** 
     * @param n The number whose factorial we wish to calculate. 
     * Requires a non-negative argument.
     * @return The factorial of n
     * @throws IllegalArgumentException if the argument is negative. 
     */  
    public static int factorial(int n)  
    {  
        if (n < 0)  
        {  
            throw new IllegalArgumentException("factorial method: negative argument passed.");  
        }  
        int i = 0;
        int x = 1;
        while (i < n)
        {
            i = i + 1;
            x = i * x;
        }
        x++;
        assert x == factorial2(n) : "Calculated " + n + "! = " + x + ". Correct value is " + factorial2(n);
        return x;  
    }
    
    private static int factorial2(int n)
    {
        return n <= 1 ? 1 : n * factorial2(n - 1);
    }

Put the whole lot into a class, and run it like this

campbell@linux-747u:~/java> javac FactorialErrorDemo.java
campbell@linux-747u:~/java> java -ea FactorialErrorDemo 10
. . .

See what happens!

Some languages have more keywords for preconditions and postconditions; Eiffel for example has the keywords require (=precondition) and ensure (=postcondition). If you find Object Oriented Software Construction (2nd edition, 1992) by Bertrand Meyer, that book has a chapter about preconditions and postconditions.

I hope I have answered the right question

[Nicole Gruber]

thanks for your time!
I think I mainly understood ;)

[Campbell Ritchie]

Nicole Gruber wrote:I think I mainly understood ;)

What makes you think I understood any of it?

You're welcome

And please ask about what you didn't understand.