------
Creating Error-Less programs Tutorial By Sean Greasley (
------
CONTENTS
1.0 Introduction
2.0 Example Program
3.0 Assertions
4.0 Hoare Rules
5.0 Summary
------
------
1.0Introduction
------
It comes a time when you’re making a problem public and you want to make sure you have correct validation procedures. This mostly occurs when your have user interaction.
For example: If you requested a 4 digit number from a user, there are chances when the user may put 3 digits, 5 digits, letters, symbols etc.
The aims of this document is to use a series or ‘Hoare’ rules to iron out where these errors may occur so you have a functioning, hopefully error-less, program.
------
2.0Example
------
void main(void) {
int i, n;
i = 2; n = 12;
while (i <= n)
{ n--; i++; }
cout < “i = ” < i < “ n = ” < n;
}
Here is a sample program written in C++. Syntactically it is correct but conventionally, the programming style is bad. We know it is bad because values of ‘i’ and ‘n’ are modified within the while loop.
For what values of ‘i’ and ‘n’ would you expect from this program?
As you can see, if a program is more complex, it would pose a very difficicult task to determine an output. This is a reason why formal semantics is needed.
------
3.0Assertions
------
A well known method of solving this problam is using assertion of mathematical formulae and proving them correct. Lets have a look at an example…
The following program calculates a Fibonacci number. (Fibonacci numbers are a sequence of numbers whereby a number is the sum of the previous two. I.e. 1, 1, 2, 3, 5, 8, 13, 21…)
void main(void)
{
int Number;
int Index, Last, LastButOne, Current;
int Answer;
cout < “Enter a positive number: ”;
cin > Number;
if (Number <= 2)
Answer = 1;
else
{
Last = 1;
Current = 1;
Index = 3;
while (Index <= Number)
{
LastButOne = Last;
Last = Current;
Current = Last + LastButOne;
Index++;
}
Answer = Current;
}
cout < “The fibonacci number at position: ” < Number;
cout < “ is ” < Answer < endl;
}
If you take a look at the previous program, it may look correct, but how can we proveits correct for all values of ‘n’?
Simple, We use assertion!
This most important part of this program is the section where the loop is executed (where a value of n is greater than 2).
// Number >= 3
Last = 1;
Current = 1;
Index = 3;
// Index = 3, Last = fib(1), Current = fib(2)
while (Index <= Number)
{
LastButOne = Last;
Last = Current;
Current = Last + LastButOne;
Index++;
}
// Index = Number + 1, Last = fib(Number – 1), Current = fib(Number)
The comments within this program provide a little bit how the variable function. They also provide a pre and post condition.
The precondition is that (Number >= 3)
The postcondition is that (Current = fib(Number))
The assertions carried out so far don’t clarify much on what happens within out while loop.
So far: We know what the values must be to enter the loop, and what values come out of it. We now need to process the code and fill in the missing piece of the jigsaw to prove that the program is correct.
// Number >= 3
Last = 1;
Current = 1;
Index = 3;
// Index = 3, Last = fib(1), Current = fib(2)
while (Index <= Number)
{
// Let Index = i, Last = x, Current = y
LastButOne = Last;
// Index = i, Last = x, LastButOne = x, Current = y
Last = Current;
// Index = i, Last = y, LastButOne = x, Current = y
Current = Last + LastButOne;
// Index = i, Last = y, LastButOne = x, Current = x + y
Index++;
// Index = i + 1, Last = y, LastButOne = x, Current = x + y
}
// Index = Number + 1, Last = fib(Number – 1), Current = fib(Number)
It is now clear that the value of ‘Last’ is the value of ‘Current’ before the loop is carried out.
The value of current is the sum of Last and Current.
The value of index is one more than the value before.
Lets add one more assertion into the picture….
// Number >= 3
Last = 1;
Current = 1;
Index = 3;
// Index = 3, Last = fib(1), Current = fib(2)
// Last = fib(Index – 2) ^ Current = fib(Index – 1) ^ 2 <= Index – 1 <= Number
while (Index <= Number)
{
// Let Index = i, Last = x, Current = y
LastButOne = Last;
// Index = i, Last = x, LastButOne = x, Current = y
Last = Current;
// Index = i, Last = y, LastButOne = x, Current = y
Current = Last + LastButOne;
// Index = i, Last = y, LastButOne = x, Current = x + y
Index++;
// Index = i + 1, Last = y, LastButOne = x, Current = x + y
// Last = fib(Index – 2) ^ Current = fib(Index – 1) ^ 2 <= Index – 1 <= Number
}
// Index = Number + 1, Last = fib(Number – 1), Current = fib(Number)
The new assertion..
// Last = fib(Index – 2) ^ Current = fib(Index – 1) ^ 2 <= Index – 1 <= Number
Is the same before the loop and after each iteration of the loop. This is therefore called a loop invariant.
It is clearly true before the loop because since index = 3, if we can prove it is true at the end of the final iteration, we are well on our way to proving our program is correct.
------
4.0Hoare Rules
------
Hoare rules are used to prove assertions are correct. In order to carry out a hoare rule, you must have asserted your program with the above syntax in the last section. Once you have done this, use one of the following hoare rules according to what function you would like to prove correct.
Hoare rule for assignment: B[a/X]{X = a; } B
Hoare rule for sequence:
A {s1} B B{s2}C
A{s1, s2} C
Hoare rule for a loop:
(A ^ b){s}A _
A{while(b){s}}(A ^ ¬b)
Hoare rule for conditional: (if/else statements)
(A ^ b){s1}B ( A ^ ¬b){s2}B
A{if(b){s1}else{s2}}B
Ok, lets take these steps one at a time. These formulas may look foreign to you, but will a little explanation they should be understandable and with a little practise, you can perfect them.
Lets have a look at our previous program….
// Let Index = i, Last = x, Current = y
LastButOne = Last;
// Index = i, Last = x, LastButOne = x, Current = y
Last = Current;
// Index = i, Last = y, LastButOne = x, Current = y
Current = Last + LastButOne;
// Index = i, Last = y, LastButOne = x, Current = x + y
Index++;
// Index = i + 1, Last = y, LastButOne = x, Current = x + y
I have taken the contents out of the while loop and placed them here. NOTE: If I included the while loop itself, we would use the hoare rule for a loop. As I haven’t, we will take a look at the hoare rule for sequence.
Hoare rule for sequence:
A {s1} B B{s2}C
A{s1, s2} C
A, B, C - assertions
Sx - statements
Syntax - if the top line is true, then the bottom line is true.
A// Let Index = i, Last = x, Current = y
S1 LastButOne = Last;
B // Index = i, Last = x, LastButOne = x, Current = y
S2 Last = Current;
C // Index = i, Last = y, LastButOne = x, Current = y
S3 Current = Last + LastButOne;
D // Index = i, Last = y, LastButOne = x, Current = x + y
S4 Index++;
E // Index = i + 1, Last = y, LastButOne = x, Current = x + y
We have now labelled our program, with this, we can apply the formulae.
A// Let Index = i, Last = x, Current = y
S1 LastButOne = Last;
B // Index = i, Last = x, LastButOne = x, Current = y
A{s1} B - A is true before the command, s1 is carried out, if the program doesn’t fail, B is true. We can then move onto the next statement
A{s1} B - TRUE
B // Index = i, Last = x, LastButOne = x, Current = y
S2 Last = Current;
C // Index = i, Last = y, LastButOne = x, Current = y
B{s2} C - TRUE
C // Index = i, Last = y, LastButOne = x, Current = y
S3 Current = Last + LastButOne;
D // Index = i, Last = y, LastButOne = x, Current = x + y
C{s3} D - TRUE
D // Index = i, Last = y, LastButOne = x, Current = x + y
S4 Index++;
E // Index = i + 1, Last = y, LastButOne = x, Current = x + y
D{s4} E - TRUE
As all of the previous statements are true, we can say that…. A{s1, s2, s3, s4}E is TRUE
And this sequence is therefore true!
------
5.0Summary
------
With this tutoial, you should now be able to prove your problems correct under a variety of programming languages. I have used C++ as the basis of this tutorial, but the same applies for Java, VB, PHP etc.
At the moment my tutorials are on astalavista until I have enough tutorials and tools to make a web with.
Previous tutorials include:
* C++ For Beginners and Advanced.txt
* PHP For Beginners
* Proving programs correct
Tools
* PHP Email Bomber
* Protection PHP Email Bomber
~ Sean Greasley