The Artima Developer Community
Sponsored Link

Weblogs Forum
Correcting Correctness

1 reply on 1 page. Most recent reply: Sep 1, 2005 8:32 PM by Christopher Diggins

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 1 reply on 1 page
Michael Feathers

Posts: 448
Nickname: mfeathers
Registered: Jul, 2003

Correcting Correctness (View in Weblogs)
Posted: Nov 9, 2004 3:55 PM
Reply to this message Reply
Summary
Many people in our industry have wanted to prove programs correct for years, but is that a correct goal?
Advertisement

A little while ago, I went back to my old university’s website and flipped through the course catalog. It brought back memories. I learned a lot of interesting things when I was in school but in hindsight one of the most striking things about the experience was the mathematical focus of my coursework. I had courses in programming and software engineering, but I also spent a lot of time learning about abstract machines and languages, how to prove and disprove assertions about the complexity of algorithms, and all sorts of other things that really seem much more akin to mathematics than design. I remember one professor who felt strongly that we would soon have smart tools that would help us prove the correctness of our programs. It’s an old idea, and a very seductive one. If we could easily prove the correctness of our programs, wouldn’t that completely change the industry? We could have fewer bugs, fewer security problems and easier development overall?

This meme, program verification, has been around for a long time, but it isn’t as popular as it used to be. Superficially, the desire to prove programs correct sounds wonderful, until you realize that correctness means “matches specification.” How do we create a specification which is complete, concise, and unambiguous? It sounds suspiciously like writing a program in the first place. And, even if we were able to do that well, we’d have to hope that we are able to do it quickly. Every time we change a “correct” program, we’d have to re-prove its correctness, wouldn't we?

A few weeks ago, I went to the OOPSLA conference and I saw a demo by a company named Ergnosis. They are in the process of developing an IDE that really knows its language intimately. If you bring up a piece of a program and select it you get a menu of a large number of changes that you can make without altering the behavior of the program at all. Some are things I’ve been wanting for years. For instance, you can select a statement and drag it after a subsequent statement or take an expression that is in the argument list of a method and push it into the method. These actions are only allowed if they preserve behavior.

Interestingly, one of the things that their tool doesn’t do yet is allow users to manually edit the code. I’m sure they’ll have that feature eventually, but the fact that they have put off adding it for so long is pretty tantalizing. It is like a question that hangs in the air for people who notice it. How much of our editing has to be risky? Can tools get us to the point where we can assume that most of our editing doesn’t change behavior but only a small subset of it does? If we can’t easily prove correctness, couldn’t we get a leg up if we tackled the derivative: if we could be certain of the correctness of most of our changes? If we could work like that, we could add tested features into a system very directly and use a wide palette of safe automated moves to make the code more easily understandable.

Regardless of the amount of tool support that we achieve, programming is a human activity and we will make mistakes. However, it is great to see some emphasis on this other point of view: that demonstrating that we’ve preserved behavior matters. I think it would be great if more of the energy that has gone into program verification could go into change verification. To me, it just seems to be the more important thing right now.


Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: Correcting Correctness Posted: Sep 1, 2005 8:32 PM
Reply to this message Reply
I have to say Michael your ideas are starting to sink through my thick skin.

"How do we create a specification which is complete, concise, and unambiguous? It sounds suspiciously like writing a program in the first place"

I have heard it stated before that the only complete specification of a program is the program itself. Intuitively it feels that there is truth to that.

Flat View: This topic has 1 reply on 1 page
Topic: Graceful Failure Previous Topic   Next Topic Topic: Policy Based Range Checking Class for C++


Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2014 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use - Advertise with Us