Many techniques for verification aim to reveals errors in the programs, because the ultimate goal is to make programs correct by removing the error. In proof of correctness, the aim is to prove a program correct. So, correctness is directly established, unlike the other techniques in which correctness is never really established but is implied by absence of detection of errors.
Any proof technique must begin with a formal specification of program. Here we will briefly describe a technique for proving correctness called the axiomatic method.
We’ll be covering the following topics in this tutorial:
The Axiomatic Approach
In principle, all the properties of program can be determined statically from the text of the program, without actually executing the program. The first requirement in reasoning about programs is to state formally the properties of the elementary operations and statements that the program uses.
In the axiomatic model of Hoare, the goal is to take the program and construct a sequence of assertions, each of which can be inferred from previously proved assertions and rules and axioms about the statement and operations in program. For this, we need a mathematical model of a program and all the constructs in the programming language. Using Hoare’s notation, the basic assertion about a program segment is of the form:
P{S}Q
Code Inspection or Reviews
The review process was started with purpose of detecting defects in the code. Though design reviews substantially reduce defects in code, reviews are still very useful and can considerably enhance reliability to reduce efforts during testing. Code reviews are designed to detect errors that originate during the coding process, although they can also detect defects in details design.
Code inspections or reviews are usually held after code has been successfully completed and other forms of static tools have been applied but before any testing has been performed. Therefore, activities like code reading, symbolic execution, and static analysis should be performed, and defects found by these techniques are corrected before code reviews are held.
The aim of the reviews is to detect defects in code. One obvious coding defect is that the code fails to implement the design. This can occur in many ways. The function implemented by a module may be different from the function actually defined in the design or the interface of the modules may not be same as the interface specified in the design.
In addition, the input-output format assumed by a module may be inconsistent with the format assumed by a module may be inconsistent with the format specified in the design.
In addition to defects, there are quality issues, which also review addresses. A module may be implemented in an obviously inefficient manner and could be wasteful to memory or the computer time. The code could also be violating the local coding standards.
A sample Checklist: The following are some of the items that can be included in a checklist for code reviews.
Do data definition exploit the typing capabilities of the languages?
Do all the pointers point to some object? (Are there any ‘ dangling pointer”?)
Is the pointer set to NULL, where needed?
Are all the array indexes within bound?
Are indexes properly initialized?
Are all the branch conditions correct
will a loop always terminated
Is the loop termination condition correct?
Dinesh Thakur holds an B.C.A, MCDBA, MCSD certifications. Dinesh authors the hugely popular