Program verification process make sure that the software functionless as per design requirements. This could be verified by inspection of the source code, or by running a pre-defined (as per software requirements) test cases. The process is semi-automated by usage of automated testing software (for example, HP WinRunner) to run test case scenario against the assessed software, but those need to be configured/loaded by a human operator. Recently, due to the rising number of security exploit in applications, software vendors began using automated software capable assessing the application for flaws leading to security vulnerabilities such as Cross Site Scripting (XSS), Buffer Overflow, Cross Site Request Forgery (CSRF). Although the automated tools are very efficient in running the per-defined test case scenario, human interaction requires to define the test cases. Furthermore, number of functional flaws are a result of logical incorrectness and will require assessment by human capable of understanding the application as demonstrated by the following code:
- procedure login(user, password)
- (
- success <--- true
- if call authenticate(user, password) = true
- then (...)
- else (success <--- false)
- return success
- ) end procedure
Performance tuning, on the other hand, can achieve a fairly good results using automated tools. Of course, an experienced software architect can make a difference at the design stage by choosing efficient algorithms and implementation technologies, but reusable designed and patters can compensate for lack of experience. Additional tuning could be achieved by optimization on the source code level and using an optimizing compiler which relies on different tuning techniques such as loop optimization, common sub-expression elimination and redundant store elimination. It could be demonstrated by the following code:
- procedure calculate(a ,b)
- (
- c <--- 4
- result <--- (a+b)-(a+b)/4
- return result
- ) end procedure
Program tuning could be achieved by removing line 3 and calculating the expression a+b in line 4 only once. The result of compiler optimization could be:
- procedure calculate (a,b)
- (
- c <--- a + b
- result <--- c – c/4
- return result
- ) end procedure
Bibliography
- Wikipedia (n.d.), Formal verification [online].
Available from: http://en.wikipedia.org/wiki/Program_verification
(accessed 30 October 2010).
- Wikipedia (n.d.) , Program optimization [online].
Available from: http://en.wikipedia.org/wiki/Program_optimization
(accessed 30 October 2010).