Sign in to follow this  
joeyg2477

Program Semantics and Derivation!!!

Recommended Posts

I am currently a junior pursuing a bscs degree and there 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.
    http://cs.olemiss.edu/abet/csci550.pdf

Share this post


Link to post
Share on other sites
Formal verification is interesting stuff. Not likely to be particularly useful for game development, except insofar as it makes you more adept at analyzing code structure and operation. If you like the theoretical side of CS, go for it.

Share this post


Link to post
Share on other sites
Quote:
Original post by joeyg2477
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.

I think it's fair to say that the usefulness of formal verification is in question at the moment. (However, there's no doubt that it's theoretically sound, since all of the math is predicated on well-established principles.) That said, there are three or four schools of thought in academia at the moment with regards to formal verification. They are, approximately,

0.) Relying on formal verification alone is outright dangerous because it instills a false sense of security. Programs can only be proven correct in extremely restricted and limited circumstances. If the verifier is incorrect in establishing that these circumstances have been satisfied, it may report that the code is correct when in fact it has a fatal error.

1.) Only the most trivial and smallest of programs can really be proven correct; complicated programs are often impossible to verify. Therefore, formal verification is generally a waste of everyone's time, and static analysis (a weaker version of formal verification) is a much better and more cost-efficient solution, even if it can't always guarantee program correctness.

2.) Formal verification is useful for understanding how your program works, but it's not viable a tool in most commercial software-development settings. It does have applications in mission-critical software segments and for complicated, independent chunks of code.

3.) Formal verification is an invaluable analysis tool for scrutinizing code. Because it's automated, it's virtually free in terms of developer time,. Even when it can't completely determine whether a program is correct, it may be able to highlight potentially problematic segments and alert you to possible mistakes, saving you time down the road when bugs are costly to fix. While no tool is perfect for every programming style, FA definitely runs the gamut in its utility.

Share this post


Link to post
Share on other sites

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now

Sign in to follow this