What every C Programmer should know about undefined behavior #2/3

There was another tool for Ruby that would randomly alter your code at runtime (!) and see how you handled the resulting errors. I am having a really hard time remembering the name, though...

The reason for using something like Z is that it is implementation-independent, so it doesn't make any difference if you're writing in C, C++, LISP or Prolog. There will be a valid mapping.

The disadvantage of Z is that in the same way the same specification can produce many implementations, the same implementation can produce many specifications. These will not be of equal use and I know of no easy way to generate the specification in a way that guarantees usefulness.

(For those more familiar with Z as the starting point, I'm totally inverting the flow. This may shock some. Sorry. With this scheme, I'm solely concerned with back-engineering what the specification of the code is from the code, not in generating code from a specification.)

The rationale is that Z is intended to be easier to validate than code. Easier, not easy. It's still hard work. But doing the validation (which is the hardest part) in a single frame of reference and converting to it from the different langauges (which is hard but not as bad) should require less work than writing a validator specific to each language.

That isn't quite right. You can easily write a program that answers those questions *if they have an answer* -- the halting problem is related to the fact that there might not be an answer at all. It's entirely possible that those particular questions do have answers, though, which case a computer program could find it. But this doesn't help much in practice because that computer program probably won't finish until sometime after the heat-death of the universe.

> You can say "all strings must be UTF-8", but how can you explain that to a computer? There's always exceptions to deal with (the result of read() for example).

Oh, but actually this is easy! Any reasonably competent statically-typed language can do this. E.g., in C++, you define a type "utf8_string", and you make sure that any publicly accessible way of constructing an instance does appropriate validity checking. Then code that assumes valid utf8 just declares that it takes input of type utf8_string. read(), of course, doesn't return a utf8_string, so if you want to read a string and then you want to pass it to some code that assumes utf8 (maybe somewhere else entirely in your program, after its been passed through 10 other functions), the compiler won't let you unless you sanitize it first. And as you refactor your APIs, the conversion naturally gets moved around to be in the right place.

It works great. But I've only seen one project that used C++ like this. It's very sad :-(.

> What if the RAM is bad? How about the hard disk?
Bad RAM is not a software bug, thus it's out of scope for software developers. It's like saying that you can't prove anything in math because your axiom or logic may be "broken". You just have to assume something. In Peano numerals, it's the existence of the number 0, and if you want to prove stuff about programs, you have to assume that the machine you run it on works.

In my experience, careful proofs can form a critical part of complex system design. I'm thinking of, for example, the problem of a VCS trying to merge a DAG of changes, each of which may contain arbitrary file adds/deletes/renames. This is a horrible problem with many incorrect solutions littering history, but, solvable with careful formal reasoning.

> Similarly, if you try to prove that your browser will successfully display a web page, you slam head-on into a mountain of difficulties. What if the RAM is bad? How about the hard disk? Will the network lose some packets? What if the web page is so complex that it takes 10 minutes to render on our puny CPU? What about the libraries I depend on? Is there a bug in there? What if the web page is rendered in an "ugly" way (a subjective term). Can I prove that that won't happen? Of course not.

Yes, but that just means you tried to prove the wrong thing.

Can that web page trigger writes to arbitrary pages on my hard disk? Is there anywhere in my program that uses latin1 when it should be using UTF-8? Will this image decoder return either valid data or a defined error code on arbitrary inputs? Does this program invoke undefined behavior? Can this data be corrupted if certain code is scheduled concurrently? Proving those kinds of properties is totally useful, possible in principle (if you set things up right), and in some cases easily doable today.

> The best I can do is set up a bunch of models and validate my program against them. Static type checking is one such model.

But static type checking *is* a way to prove global properties of your program! Or another example: C++'s "private:" keyword is useful not because it gives some kind of 'security' or something (like many documents about it seem to think), but because it lets me know for certain (i.e., prove) that I only have to look at a certain bounded amount of code if I want to see how certain variables are modified. (And then that in turn is useful because it lets me verify that all that code maintains the relevant invariants, which is another kind of informal proof.)

I just want better tools for *non-heuristic* reasoning about programs. That's really not impossible -- though it might require changes to everything from the programming languages to your program's architecture -- and it would be useful to people without tenure, too.

Such a statement requires omniscience.

I am afraid you are not omniscient

http://en.wikipedia.org/wiki/Polyspace (just a random example)