Programming Language and Verification summary.

In order to make a computer function according to your precise instruction (i.e. make it run your program), you need to communicate with it. Although there are various methods of communicating with a computer which can be as sophisticated as voice command, the most primitive, widely used and effective method of such communication is via a programming language. Programming languages are uniquely designed in essence to bridge the communication gap between the computer’s language (computers only understand binary at fundamental hardware level) and complex human languages. Since the advent of computers, these languages started and kept on being created, with the emerging ones consisting of enhanced properties necessary for easier usage, faster application etc.

A software requires to be verified in order to ensure that it meets the particular requirements that could be as important as the ones for which the very software was created. However, it is quite different from validation. On one hand, verification deals with whether a program is designed accurately while on the other hand, validation focuses on the validity of the program that is designed. Furthermore, the verification process is even different from the notion of testing in several ways. First, testing essentially decreases the frequency of the cases at which the software fails, while verification makes detects the reasons behind the failures and fixes them. Testing is only possible after the creation of the software by passing a collection of input data and scrutinizing the output. But verification can start right from the beginning, throughout the process of creation and even after the completion of it.

Verification is of two types, namely dynamic and static. Dynamic verification can be termed as “behavior analysis” of a program. In other words, it examines the structure and performance of the functions, classes etc. of a software. This verification type can be subdivided in to three categories: first one being verification based on testing whether the program can satisfy a particular criterion. The second one deals with testing on a large scale (often with multiple classes, functions etc.) and finally the third one is more interested in the acceptability of the program.

Meanwhile, static verification, without any execution of the program, tries to find out whether the developer adhered to the conventional coding processes and principals. Methods of static verification include, but are not limited to model checking, data flow analysis and abstract interpretation.

A notable drawback of verification methods are their inability to deal with large software such as operating systems in an efficient manner. The reason behind this is their broad expanse of functions which are too large in number to be meticulously verified. For this reason, special software and utilities are being developed to ease this task. Nevertheless, verification remains a crucial component of software development as it confirms that the produced software can meet the demands that lead to its birth.

Questions:

Is autolab, a verification software? If yes then what kind of verification does it perform?

How are programming language created? What are the prime pocus during initial stages of their development?

Is it possible in future that voice, gesture and other physical techniques that are used by humans be applied to communicate with computers?

References:

http://www.contrib.andrew.cmu.edu/~tjabban/proglangandverif.html

http://cs.stackexchange.com/questions/13785/formal-program-verification-in-practice

http://www.eecs.berkeley.edu/~necula/Papers/nelson-thesis.pdf

http://www.ted.com/conversations/10140/creating_a_high_level_programm.html

http://en.wikipedia.org/wiki/Formal_verification