🔒 Locked

Progam Semantics and Derivation!!

Started by joeyg2477 Nov 28, 2005 at 11:36 PM 0 replies 500+ views

Original Post

Nov 28, 2005 at 11:36 PM

I am currently a junior pursuing a bscs degree and thier is a class offered next semester called Program Semantics and derivation being taught by the chair of the department. Well he of course says I should take it, but I wonder if anyone that reads this post has ever heard of this kink of practice? Here is a link to a description of the class http://cs.olemiss.edu/abet/csci550.pdf .He has done a seminar this semester on it and the bese I can describe it is as taking the specifications of a very small but critical part of code and using predicate logic to derive that code theoretically. If anyone has heard of this practice or have used this practice please comment on the usefullness of it. I'm thinking of not taking the class because I have never heard of this before.

ToohrVyk

238

ToohrVyk

Nov 29, 2005 at 2:33 AM

I can think of several uses off the top of my head:
- Proving that your program works (the next step is usually abstract analysis, which can be used to prove that no asserts will ever be triggered by your code, ergo it does not contain bugs if you use a correct assert net). Helps making sure critical on-board programs for airplanes don't send you crashing into the ground.
- Proving that if a program is correctly typed (that is, compiles), then it works as expected and does not crash (but may fire assertions, such as out-of-bounds on arrays or divide-by-zero). This is obviously not the case for all languages, especially when you can cast at will between pointer types.
- Applications to linear logic and automatic proof system, but you probably don't want to hear about it.

So, this is of large importance when creating or studying programming languages, as well as when creating automatic debugging tools.

Topic Locked

This topic has been locked by a moderator. New replies are not allowed.