hendrikboom ([personal profile] hendrikboom) wrote2011-06-21 09:53 am

An example why verified programming is hard.

Walking back from where I parked my car today, I realized how difficult it is to make sure specifications are satisfied, once you start looking at them formally. There are specifications with obvious meanings, and obvious algorithms to satisfy them. But ...

After passing the hospital front door, I decided to park in the first available space. The obvious way to do this is to keep driving until I see an available space, and then park in it. But, when I'm finally parking in that space, is it the first available space? Can I know that? When I walked back to the hospital, I saw another available space. It hadn't been available when I drove past it. Was it there when I entered my parking space? I have no idea.

Now this is everyday trivia. But if something like this were to happen in a computer program, and other formal reasoning depended on getting into the first available space, things might get difficult. Would I have to make the specifications weaker? Would I have to make it precise in a complicated way? Would I have to change other code that depended on the details of the spec I could not implement?

Formal verification is hard. Informal verification is impossible. We resort to debugging, and our systems are are vulnerable to attack.

Post a comment in response:

Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
Account name:
If you don't have an account you can create one now.
HTML doesn't work in the subject.


If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org

Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.