The programing language that we write is actually not understood by the computer. The computer translates the program into binary code so that it can understand. Semantics as defined by Wikipedia is “semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages. It does so by evaluating the meaning of syntactically legal strings defined by a specific programming language, showing the computation involved.” In other words, semantics is the meaning of the program or what the line in the program mean.
The next step after making the program is to check if it works and there are no holes in the program. Verification means making sure that that the program works properly without any flaws and with the required requirement. If the program is not well-written then during verification many hurdles might arise due to errors in program. There are two types of verification: dynamic verification and static verification.
Dynamic verification is also known as test or experimentation. It is further divided into three families ‘Test in the small’, ‘Test in the large’, and ‘acceptance test’. Test in small is where the program tests or checks a single function or class. Test in the large is where the program checks a group of classes like a single module, more than one module, and/or the entire system. Whereas the acceptance test is used to check the acceptance criteria of the software. On the contrary, Static verification checks and analyzes whether the code follows acceptance criteria for a software.
In conclusion, a program is well-built if there exists no error in them. There are many programming languages available and they have to be truly verified to define them as perfect code.
Questions on ‘Programming Languages and Verification’:
1. What kind of research is done in this field?
2. What are the limitations of verification and programming languages?
3. How long is the verification process for any program?