Programming Languages and Verifi
 

Programming Languages and Verification

I would like to start by defining the meaning of programming languages. Programming languages are unique languages, used for writing computer programs .They are considered as a bridge of communication between human and computer languages. Even though there are plentiful programming languages available, new languages are always being created, mainly for the purpose of making them easier to recognize, more effective, reliable and to create faster applications.

There is another terminology in computer science which is verification. Verification is the process of making sure that the software written fully fulfills with the definite requirements. But verification must not be mixed up with validation; one way to make a distinction between the two is by the following questions. Verifications asks “are we building the product right?” while validation asks “are we building the right product”. Nevertheless, verification is one of the most vital steps when writing programs. ‘Testing’ the program alone cannot guarantee that the program is completely correct. In fact, there are many differences between testing and verification. Testing shrinks the rate of recurrence of failures, while verification detects those letdowns or slips and rejects them absolutely. Testing is done only when the program is complete, and that is done by experimenting with a set of inputs (most regularly extreme values along with values in between) and examining the results. On the other hand, verification is done before, during and after the programming is complete.

There are two types of verification; dynamic verification and static verification. Dynamic verification deals with the behavior of the software execution. To further explain, dynamic verification are classified into three families; one is ‘testing in the small’, where a test checks a single function or class, another is ‘testing in the large’, where a test checks a group of classes, and finally, an acceptance test, which checks the acceptance criteria for a software (mainly functional and non-functional tests).Static verification is the set of processes that analyses code to make sure the defined coding practices are being followed; without running the program itself. Some of the methods of static verification are model checking, data flow analysis and abstract interpretation.

When it comes to large programs however, such as operating systems, the verification process will be tremendously time consuming. Such programs are too broad for them to be thoroughly verified, and hence there are special utilities and software for this purpose (in-depth verification of the full program). In conclusion, verification is an essential element in programs and programming languages. If a program isn’t fully verified, it would be ineffectual towards its desired goal, and thus fails.

 

Questions:

 1) How does the verification process work?

2) How are programming languages (and applications) created?

 

Useful links: