Programming Languages and Verification
Programing language
To automat a process, computer scientist computes programs. Since computers are only machines that preform given tasks, it does not have the required intelligence to solve problems. That makes delivering the solutions to the computers quite difficult. The way solutions have to be delivered to the computer have to be communicated explicitly, precisely, stepwise constructed, and without any ambiguity. This can be accomplished with programming languages. A programming language is defined in Introduction to Programming Languages as “an organized way of communicating with a computer, such that the computer behaves faithfully, according to instruction given by the programmer.” It is also known to be a notational system for describing computation in a machine-readable and human-readable form.
Programming languages development depends on many things like evolution of technology, computer architecture, operating system modular software, and the need to maintain the software for a long time. Since there are many types of programs, there is a different programming language designed to it.
There are different types of programming languages starting from first to fifth generation languages. And there are classified into two groups:
1- Traditional programming languages
• Sequence of instruction
• First, second and some third generation languages.
2- Object-oriented languages
• Objects are created rather than sequence of instructions.
• Some third generation, and forth and fifth generation languages.
Criteria in a good language is:
1- Writability
2- Readability
3- Orthogonality
4- Reliability
5- Maintainability
6- Generality
7- Uniformity
8- Extensibility
9- Standardability
10- Implementability
Program language verification
Verifying a program or software is very crucial. Errors in those can coast as much as $3 billion a year. Airlines for example estimate a reservation system shutdown with $70,000 lost for every minute. You may not think about it, but on average a programmer make around 50 errors for every 1000 lines of code.
Some of the examples of simple errors that have contributed to very serious consequences, and how significant verification tools could be in such situation in reducing the impact are The Bank of New York disaster, the all-time most expensive single-character error, the Ariane 5 failure, Millions inconvenienced, millions paid in compensation, Testing is not proof. Some other errors can be life threatening, like Programmer error in air traffic control software, Ambulance Dispatch System failure, and Software that kills
For those reasons, verification is as important as programming, because without it a program can preform it’s opposite purpose.
References
Garg, V. (2013, January 30). Lect 1. introduction to programming languages. Retrieved September 13, 2015, from http://www.slideshare.net/VarunGarg7/lect-1-introduction-to-programming-languages
Bansal, A. (2014). Introduction. In Introduction to programming languages. Florida, New York: Boca Raton.
ROOSEN, P. (2000). Part 1. In Software Verification Tools. Toronto: YORK UNIVERSITY.