PLV

What are programming languages? They are man-made languages created for computers for us to be able to communicate with machines, which would otherwise be impossible. Programming languages are divided into two components, syntax and semantics, where syntax basically means the same as correct grammar, i.e. it checks whether everything abides by the rules of the programming language, similar to correct grammar in languages, and semantics means meaning, whether what we write makes any sense at all, whether the things we wrote make sense as a whole. Both of these, semantics and syntax use binary code, the only language a computer can understand, and name them, thus making them easier to understand. But what are programming languages used for anyways? To make all the software we are using nowadays with an ever increasing influence each day. They are used to make our iPhones, Androids, and all the other products we use, work. But which programming languages are used to make them? Theres Python, theres C++, Java and a whole lot more less/more known languages. But why don’t people (programmers) use one programming language over the other? The reason for that, is that each programming language offers several advantages over the others, but also comes with disadvantages of its own, for example C++ is the most flexible language while also being the most difficult to learn. All of this is good and all, however how do we know whether the programming language we’re using is correct, whether the algorithms run properly? For that we have several ways of verification which include program analysis, automated theorem proving, model checking and abstract representation. Program analysis is divided into two parts, static and dynamic analysis. Dynamic verification deals with the behavior of the software execution, while static verification is when the code is analyzed to make sure that the coding rules are being followed, without using the code itself. Automated theorem proving is used to test mathematical theorems inside programs to check whether they work or not. Model Checking checks whether the program meets safety requirements, to ensure that the program does not crash under certain situations. Abstract Representation focuses on static analysis, which is extracting the information on the possible uses of the computer program, which is mainly used in two cases, to find whether the program may be made more effective in certain cases, or if it is possible to protect the program from bugs.

Questions

Is a perfect programming language possible?

How many programming languages are there?

What are the limitations of using programming languages?

What are effective ways to verify a programming language?

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

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

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

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

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

http://www.webopedia.com/TERM/P/programming_language.html

http://www-verimag.imag.fr/Program-Verification.html