How to prove correctness of algorithm
My thesis mentor told me that try to understand the structural working and the relationship between statements inside your programs and let explain them transparently.
By this reason, I look back my programs understanding and illustrate these on interesting algorithms by myself on Java implementation.
What is algorithm correctness of computer program?
The correctness of the program represented in the product precisely execute the goals and specifications that developers have proposed at the design stage.
In another way, the program P is correct if P performs precisely and totally requirements from design specifications. For example, if you have input A after finished program P, you had to get output B where A and B are logic expressions.
What is the approach proving correctness of the program that I used?
Firstly, I need consider and understand to formal semantics of the program which specify its technical characteristics under a formal representation.
Then, I realized that need two things for this. One I have to find out some semantic specifications as definitions can take the form of a set of axioms. And a set of inference rules show that how the semantics of any code block in the program are correct.
So for one year ago, I have studied to program verification based on formal semantics approach due to C. A. R. Hoare. This is also my thesis, which is the bulk of the development concentrates on a rather small core language of Java-programs to demonstrate the applicability of formal semantics show:
- How to use semantics for validating prototype implementations of programming languages.
- How to use semantics for verifying analyses used in more advanced implementations of programming languages.
Why spend time to study formal semantics of programs?
Computer programming are tasks wherein talent mathematician is urgently required. Mathematics of programming is interested topic for researching programming languages.
I believe that mathematical understanding and software engineering will improve product reliability and services valuable.
Formal semantics are concerned with the rigorous mathematical study of the meaning of programming languages that describes the processes a computer follows when executing a program in that specific language.
This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will execute on a certain platform, hence creating a model of computation.
Formal semantic understanding increase development productivity. Productivity I mentioned that it doesn’t go to saving bits, bytes or millisecond performance.
It intends to correctness, readability, maintainability, take full advantage of the capabilities of the programming language and still not depend on them.
This is what I do to proving algorithm correctness partially?
I pretend to you already read about semantics description methods:
- Operational semantics
- Denotational semantics
- Axiomatic semantics
It is important to note that these kinds of semantics are note rival approaches, but they are different techniques appropriate for different purpose and to some extent for different programming languages.
So, here I scoped to axiomatic semantics that often one is interested in partial correctness properties of programs.
A program is partially correct, with respect to a precondition and a postcondition, if whenever the initial state fulfils the precondition and the program terminates, then the final state is guaranteed to fulfil the postcondition.
Thus a partial correctness property of a program don’t need ensure that it terminates.
This is contrary to total correctness properties which express that the program will terminate and that there will be a certain relationship between the initial and final values of the variables.
Thus we have:
Partial Correctness + Termination = Total Correctness
Bases on a set of Hoare axioms as providing a set of rules to a inference system of the correctness of computer programs via the accuracy of mathematics.
A Hoare Triple of the form:
{ P } C; { Q }
Where P and Q are logic expressions, C is a statement; Additional P is pre-condition and Q is post-condition.
Hello World!
I will examine to the assignment statements in Java language.
Assignment axiomatic for partial correctness:
{ P[x/a] } x = a; { P }A simple method specification:
Given a, b parameters are integers, a ⋮ d and b ⋮ d. After the method executed, return a and a ⋮ d.
I have Java implement block like this:
public int helloWorld(int a, int b){ a = a — b; return a;}
And want to prove this program execute and return a with precisely properties ( a ⋮ d ).
From method specification, I have inserted logic predicates into the program
public int helloWorld(int a, int b){
// P: a mod d = 0 ∩ b mod d = 0 a = a — b;
// Q: a mod d = 0 return a;}
Using Hoare assignment axiom, put predicates before the statement with inversed deduce from post-condition Q
public int helloWorld(int a, int b){
// P: a mod d = 0 ∩ b mod d = 0 // P1 = Q[a/a-b]: (a-b) mod d = 0 a = a — b;
// Q: a mod d = 0 return a;}
Need to prove P → P1, given P: a mod d = 0 ∩ b mod d = 0
P → P1: (a-b) mod d = 0 is correct too because algebra logic. So it can resolved relationship between the initial state P → the final state Q.
For another example program in Java, we have swap integers function like:
public void swap(int x, int y){ // P: x = n ∩ y = m
int z = x; x = y;
y = z;
// Q: y = n ∩ x = m}
Where x = n ∩ y = m is the precondition and y = n ∩ x = m is the post-condition. The names n and m are used to explicit to the initial values of x and y.
Thus, if the initial state [x → 5, y → 7, z → 0] satisfies the precondition by taking n = 5 and m = 7 and when we have proved the partial correctness property we can deduce that if the program terminates then it will do so in a state where y is 5 and x is 7.
However the partial correctness property does not ensure that the program will terminate although this is clearly the case for the above example program.
The axiomatic semantics provides a logical system for proving partial correctness properties of individual programs.
A proof of the above partial correctness property may be expressed by the following proof tree:
{ P } z = x; { P1 } { P1 } x = y; { P2 }
------------------------------------------------- { P } z = x; x = y; { P2 } { P2 } y = z; { Q }
-------------------------------------------------------------------- { P } z = x; x = y; y = z; { Q }
And we can prove relationship between P → Q by mathematic inference when execute through each statements:
// P: x = n ∩ y = mz = x;// P1: z = n ∩ y = mx = y;// P2: z = n ∩ x = my = z;// Q: y = n ∩ x = m
It’s just the started answer my deeper questions
The partial correctness properties expose to the logical system as a specification, assertions of only certain aspects of the semantics.
The benefits of the axiomatic approach are that the logical systems provide an easy way of proving properties of programs. And to a large extent it has been possible to automate it.
For the above examples, I implemented under Java language. But logic assertions are based on axiomatic semantics that do not depend on specific programming languages, just concerned with the semantics of structured programs.
On complex programs, we can build programs which are totally correct with a based-on accuracy of logic mathematics.
It also leads me to take automate program verification where you are required to ensure to programs are totally correct but you can not run to test programs in real environment.
References:
If you also interested in, let read more from
