Frans Bouma's blog

Generator.CreateCoolTool();

Syndication

News

    Visit LLBLGen Pro's website

    Follow FransBouma on Twitter

    Add to Technorati Favorites

About me

Fun stuff I created

My work

Correctness provability should be the goal, not testability

(edited. s/proof/prove/gc and some sentences which were 'out of wack' have been corrected as well)

Phil Haack today posted an article about Writing Testable Code Is About Managing Complexity. He says:

Of course, when I'm done un-bunching my knickers, I realize that despite all the benefits of unit testable code, the real benefit of testable code is how it helps handle the software development's biggest problem since time immemorial, managing complexity.
There are two ways that testable code helps manage complexity.

1. It directly helps manage complexity assuming that you not only write testable code, but also write the unit tests to go along with them. With decent code coverage, you now have a nice suite of regression tests, which helps manage complexity by alerting you to potential bugs introduced during code maintenance in a large project long before they become a problem in production.

2. It indirectly helps manage complexity because in order to write testable code, you have to employ the principle of separation of concerns to really write testable code.

I find that a little backwards. It's not that due to focusing on testability, you get separation of concerns, but by applying the principle of separation of concerns you get code that's easier to test as a bonus. For people who think that's the same thing, it's not. Getting easy testability as a bonus means that testability is not the goal of why you set up your architecture using the principle of separation of concerns, it's a side-effect; the main goal was to get separation of concerns to be able to prove code is correct.

Scientific research has shown that in the end, separation of concerns is inevitable to get solid software which is correct. (Peri Tarr, Harold Ossher, William Harrison, and Jr. Stanley M. Sutton. N degrees of separation: multi-dimensional separation of concerns. In Proceedings of the 21st international conference on Software engineering, pages 107-119. IEEE Computer Society Press, 1999. (PDF). Who said Computer Science research is out of touch with reality, eh?

When focusing on testability, one can fall into the trap of believing that the tests proof that your code is correct. That's not true: the set of tests prove that your code is correct in the solution space defined by the tests. Take for example this simple routine:

for(int i=0;i<100;i++)
{
	if(SomeMethod())
	{
		// code
	}
	else
	{
		// code
	}
}

This routine has 2100 code paths. It's nearly impossible to test them all out with unit-tests in normal time. To say that this code is correct, one has to prove the code is correct, a set of tests won't cut it. Code can only be proven to be correct if it is predictable (deterministic). Dijkstra's famous rant against 'goto' statements is mainly based on that: a goto could create unpredictable code and therefore non-provable code.

Proving code correctness
Proving code to be correct isn't easy, but it should be your main focus when writing solid software. Your first step should be to prove that your algorithms are correct. If an algorithm fails to be correct, you can save yourself the trouble typing the executable form of it (the code representing the algorithm) as it will never result in solid correct software.

After you have proven your algorithms are correct, your second step should be to implement the algorithms in executable form by taking extra care in the projection that you are applying while doing it: you should write sourcecode which reflects the algorithm(s) you designed and of which you have proven to be correct. Writing sourcecode is making a projection of an algorithm on an executable form, as the sourcecode is the algorithm, but in another form: the executable form. This is essential knowledge, as you can use that to prove that your code you wrote to represent the algorithm or algorithms is indeed the projection of the algorithm in executable form. Typically this is done by using pre/post conditions for example, checking if the code indeed traverses from state n to state n+1 if event e occurs, etc. One way to do this is for example by writing other code which tests your code's algorithm implementation, however that creates in effect an infinite loop: to prove that your test is correct, you either have to prove that with conventional tools or with yet another test.

By applying the principle of separation of concerns, one will quickly learn that proving code-correctness is easier: algorithms are projected only once, in isolated form so the end result is deterministic and therefore a candidate to be proven to be correct.

There's another benefit of taking these steps and sticking to it no matter what: debugging an application becomes easy. As you've already proven that the algorithms are correct, you only have to confirm that the code you wrote is indeed the the algorithm in executable form. That doesn't even need a debugger at all, you can do that in the editor, whiteboard, sheet of paper or whatever rocks your boat. If it becomes complex, you can revert to the debugger but you know what to look for: you know what to expect, as you know the algorithm.

Testing your code can be a way to prove that code obeys a given set of standards, does things as expected. It's a tool to be used to reach the goal called correct software, it's not a goal on its own.

Published Wednesday, November 14, 2007 11:30 AM by FransBouma

Comments

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 10:06 AM

> When focusing on testability, one can fall into the trap of believing that the tests proof that your code is correct. That's not true: the set of tests proof that your code is correct in the solution space defined by the tests.

Finally, someone that understands logic.

I wish more people understood this.

foobar

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 11:49 AM

Minor nitpick - and I know that English isn't your first language, so I really hate to do this... The way you are using "proof" as a verb has to do with making bread rise or "proofing" something against water (for example); the verb you want is "to prove"... Sorry, I'll go back to reading the content and not the semantics :-)

Mike

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 12:25 PM

Mike: thanks for that, I'll update the text. I think that I have the title correct, but for the rest I'll check if I can find any prove/proof mistakes ;)

FransBouma

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 4:07 PM

Frans, believe it or not, the proof/prove mistake really peeks my eyes out (despite not being a native speaker): go to weblogs.asp.net/.../developing-linq-to-llblgen-pro-day-4.aspx

and search for "to proof"... Your English is perfect otherwise - you just need to sort out the proof/prove thing :)

Keep up the good work!!!

Anonymous Nitpicker

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 4:51 PM

Yes I made the mistake OFTEN :) I was convinced that it was 'to proof', so I wrote that everywhere. From now on I'll use 'to prove'. :)

This community server system is too cumbersome to update all the posts, so you'll have to live with the 'kromme tenen' the mistakes'll give you ;)

FransBouma

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 4:54 PM

So... are you saying we shouldn't write test code, or that we should rely on it? How do approach this problem in your own code?

Thanks.

PBZ

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 5:04 PM

"So... are you saying we shouldn't write test code, or that we should rely on it?"

I am saying that you shouldn't see tests as the proof that your software is correct, and that testability isn't a goal, it's a side effect of separation of concerns.

You should focus on proving that your code is correct, which CAN be done by testing your algorithm implementations with tests, but these tests then have to be proven to be correct, which is often ignored. You can also prove that a piece of code is correct without writing 1 line of testcode. It's a myth that you need automated tests to get correct code.

So in short: automated tests can show you you broke something which did work before. So they can prove your code ISN'T correct. They can't prove your code IS correct. That's a big difference and often overlooked.

FransBouma

# re: Correctness provability should be the goal, not testability@ Wednesday, November 14, 2007 5:25 PM

I agree, I've seen lately ugly code caused for trying too hard to make it testable

Eber Irigoyen

# re: Correctness provability should be the goal, not testability@ Thursday, November 15, 2007 2:35 PM

[Dijkstra's famous rant against 'goto' statements is mainly based on that: a goto could create unpredictable code and therefore non-provable code.]

Er... no. Goto is totally deterministic, just like every other statement. Dijkstra was worried about complexity, especially when it came to humans trying to comprehend the code, not with determinism.

As for proving one's algorithms... yea, absolutely. Right after solving the comparatively minor problem of the Sun running out of "steam" in a few billion years.

Finally: [One way to do this is for example by writing other code which tests your code's algorithm implementation, however that creates in effect an infinite loop: to prove that your test is correct, you either have to prove that with conventional tools or with yet another test.]

Hmm. The same thing - with the same flaws - can be said about proving that the algorithm works. You have to prove that the proof is correct. Yuck.

In practice, things are much weirder: how do you prove that a test that says

Assert(2, MyClass.Add(1, 1));

is correct? What does that even mean? It compiles? Hell yeah. It matches its specifications? There are none for a test. It says what I meant? Obviously.

Hmm. I don't think I liked this article that much :)

Marcel Popescu

# re: Correctness provability should be the goal, not testability@ Monday, November 19, 2007 8:43 AM

You have a response to this article on haacked.com/.../what-exactly-are-you-trying-to-prove.aspx

Not sure if this blog supports trackback because I didn't see it on here.

Sameer

# re: Correctness provability should be the goal, not testability@ Monday, November 19, 2007 9:13 AM

Sameer: I know there was a response, but I decided  not to continue this discussion as the basic idea of proving the correctness of an algorithm is apparently not accepted as something perfectly doable. (it's just logic). I mean: when someone wants to sort elements in a list, one picks a sort algorithm. It's easy to prove these are correct or not.

So the discussion then becomes a silly exercise where the 'confidence' meter of some person is apparently the thing to use when one decides if software is correctly doing what it should.

With a simple example it's shown that what Phil said is pretty meaningless in this regard. Take the following:

- you are given an object. The object has references to other objects, which have references to other objects, via collections or directly etc. etc.

- you are given the task to put the objects in the right order so when the data inside the objects is saved to the DB, no FK constraints are violated.

Say you write code for that: you think about how you would do this, cook up some algorithm and write code for that. You write 10,000 unittests to see if you're done or if it needs more work. They all pass.

Then a customer calls, who says: "I get an FK violation". The customer shows you a complex graph of objects and indeed, when that graph is used with your code in the 10001st unittest, it fails.

Edge case? Who knows, there are unlimited graphs to think of, so there are in theory unlimited unittests necessary to see if your code is correct.

However, what does that failing 10001st unittest show you?

1) Your algorithm sucked, but your implementation of it was correct

2) Your algorithm is OK, but your implementation of it sucked

3) All of the above

You can't possibly FIX this, unless you know your code is failing because of 2) and not because of 1).

So you have to know if your algorithm is correct. Now, if you would have implemented a proven algorithm like Topologically sorting of graphs, you would know your code is failing because of an implementation error and you should review the code again. Topologically sorting is provable by simple logic. As with a lot of other algorithms, in fact a LOT of algorithms are already proven to be correct for you, and the last couple of years a lot of research has been done to prove algorithms.

What I was trying to say in my article above, is that if you don't know if your algorithm is correct, you can forget the rest. With the example given above, I have proven that to be true, as you can't say what's wrong with your code when the unittest fails if you don't know if your algorithm is the cause or your implementation of it.

So do I then have to continue this discussion with someone who is apparently deeply convinced that what people do in the CS field is apparently not really interesting, all what matters is confidence based on a lot of green lights in the unittesting tool? I have respect for Phil Haack, but I think we have incredibly different views on the matter that discussing this further isn't that useful.

 Trackbacks are disabled because trackback spam to .info sites became too much of a burden.
 

FransBouma

# re: Correctness provability should be the goal, not testability@ Monday, November 19, 2007 9:21 AM

"Er... no. Goto is totally deterministic, just like every other statement. Dijkstra was worried about complexity, especially when it came to humans trying to comprehend the code, not with determinism."

Please re-read Dijkstra's paper:

www.cs.uakron.edu/.../dijkstra68goto.pdf

In there, he argues that a program execution is traversing a graph. This means that it's predicatable where you end up, by just following the graph. However with goto that's not the case.  

FransBouma

# re: Correctness provability should be the goal, not testability@ Tuesday, November 20, 2007 5:14 AM

Interesting discussion although I do wonder what your point is. Are you talking about some theoretical goal to strive for in the future? I mean proving code-correctness in all but some trivial examples is just not feasible. You agree on that don't you?

"Proving code to be correct isn't easy, but it should be your main focus when writing solid software" Really? How do you suggest I go about doing that? Let's say I've got a modest program with 3000 lines of code using some third party libraries. Do you have any idea what kind of work would be involved in proving that to be correct? We're not just talking elbow-grease here. We're talking a team of people working fulltime for a looooong time. All for a program you should be able to write by yourself in a couple of weeks. Would your customers pay for that?

"Your first step should be to prove that your algorithms are correct."

Good we've now proven that maybe 1% of our program is correct. Maybe we've even gotten our projection correct. (We've been really really careful so it's still correct right? riiiiight)

What about the rest. What about the code to render the ui, reset your teatimer and open the harddrive tray? I don't think they would qualify as alghorithms in any realistic sense, yet they have a huge potential for bugs.

I think unit tests are a way to aleviate the uncertainty and unpredictability of the rest. At least that way you can add some constraints that 'll make sure you don't repeat past mistakes. It's nowhere near a proof that your code is correct but I honestly don't know anyone who really thinks that.

stephan

# re: Correctness provability should be the goal, not testability@ Tuesday, November 20, 2007 6:01 AM

"Interesting discussion although I do wonder what your point is. Are you talking about some theoretical goal to strive for in the future? I mean proving code-correctness in all but some trivial examples is just not feasible. You agree on that don't you?"

I'm not posting articles about open-door snake-oil, Stephan.

"Really? How do you suggest I go about doing that? Let's say I've got a modest program with 3000 lines of code using some third party libraries. Do you have any idea what kind of work would be involved in proving that to be correct? We're not just talking elbow-grease here. We're talking a team of people working fulltime for a looooong time. All for a program you should be able to write by yourself in a couple of weeks. Would your customers pay for that?"

I hope you've read what I wrote. If you think proving algorithms is undoable, we're done debating the point. It's not about the code, it's about what the code represents: after all the code is an executable form of an algorithm or set of algorithms: i.e. it's a result of a projection, not something which is the origin of a projection, but a result of it.

Let me reverse the question: you're asked to produce a given set of functionality in executable form. You write some code and apparently something triggers you to say: "it's done, it works, lets ship this to the customer".

Unless that 'something' is actual proof that it works, you are shipping something to the customer which can fail miserably in some occasion.

A system which can receive an infinite amount of possible inputs can and WILL fail if you haven't proven that the system can handle these infinite amount of inputs. It's not hard, although it's necessary.

Take our O/R mapper system. Do you think we simply ship it because it passes our unittests? Or do you think we ship it because it passes our code reviews of implementations of our proven algorithms AND it passes our integration tests? Mind you: our system has to deal with every possible input, and there's no room for failure: if our system fails, the application build with it fails!

""Your first step should be to prove that your algorithms are correct."

Good we've now proven that maybe 1% of our program is correct. Maybe we've even gotten our projection correct. (We've been really really careful so it's still correct right? riiiiight)"

I don't think you understood what I meant with proving algorithms. If you think proving the algorithms of your software means you've proven 1% of your software to be correct, you have no clue what programming is all about. Hint: it has nothing to do with typing code.

"What about the rest. What about the code to render the ui, reset your teatimer and open the harddrive tray? I don't think they would qualify as alghorithms in any realistic sense, yet they have a huge potential for bugs."

You think in 'code', but that's not what you should do. 'Code' is the end result, it theoretical basis is somewhere else. If you give me a piece of code you wrote, it effectively has NO MEANING. What's more important is the theory behind that code: why did you write it the way you wrote it? If you're a professional, you'll answer: "because the design dictated that", which comes down to the algorithms designed dictated your code that way. If you're an amateur, you'll likely mumble something about wind direction, the temperature of your coffee etc.

"I think unit tests are a way to aleviate the uncertainty and unpredictability of the rest. At least that way you can add some constraints that 'll make sure you don't repeat past mistakes. It's nowhere near a proof that your code is correct but I honestly don't know anyone who really thinks that."

You firmly believe that anyone who unittests is doing that solely to prevent future mistakes? Or do you think they unittest to be sure what they wrote works?

Did you read the post I wrote above? What if I have a failing unittest? What does that mean, really? You can't answer that if you don't know that the algorithm is correct or not.

Next time you ship something to a customer, think about WHY you made the decision to ship it at that moment and not a week before that. Was it because all unittests succeeded? (which shouldn't be a guideline according to you because succeeding tests don't prove correctness, right?) or was it because some 'confidence' or other 'believe-driven-development' hogwash rose above a given threshold? ;)

FransBouma

# re: Correctness provability should be the goal, not testability@ Tuesday, November 20, 2007 8:42 AM

I'm not saying you're a snake-oil salesman, I just think you have an unrealistic view of provability of a program.

"It's not about the code, it's about what the code represents: after all the code is an executable form of an algorithm or set of algorithms: i.e. it's a result of a projection, not something which is the origin of a projection, but a result of it."

That's true for a very small subset of the entire codebase of an average application. The rest is based on assumptions what you think your customer want and needs. I've seen some very detailed specification in my time, none were anywhere near complete enough to use as mathematical specifications usable for proving the correctness of a certain piece of code. Besides my point wasn't that the code is the algorithm, I know you see it as a representation of an algorithm, I'm saying you have to translate this algorithm by hand into code which by definition breaks the provable correctness of the resulting code.

"Unless that 'something' is actual proof that it works, you are shipping something to the customer which can fail miserably in some occasion."

Yes that is exactly right. That's the reality we live in. Software can and will contain bugs. Bar some software in very specialized domains, no software is proven to be correct. Anyone who thinks that is seriously deluded. If you have such a proof for llblgen I suggest you post it on your website, because it would make an excellent promotional tool. I'm not talking about that one o-r mapping algorithm you proved on paper and then translated (by hand!) to code. I'm talking about the glue that holds these pieces (you know, probably 99% of the software) together. In addition I suggest you go to microsoft or any of the other major os vendors, because obviously you've discovered something incredible. They probably base most of their os code on proven algorithms, but somehow they can't seem to get it right. They and the rest of us I might add.

"A system which can receive an infinite amount of possible inputs can and WILL fail if you haven't proven that the system can handle these infinite amount of inputs."

I totally agree. And no you can't.

"Take our O/R mapper system. Do you think we simply ship it because it passes our unittests? Or do you think we ship it because it passes our code reviews of implementations of our proven algorithms AND it passes our integration tests? Mind you: our system has to deal with every possible input, and there's no room for failure: if our system fails, the application build with it fails!"

So you're saying unittests are not enough, code reviews, and integration test are necessary tools too. Totally agree. It won't give you a proof that you're software will be 100% correct though(although earlier you did say that was necessary...)

"I don't think you understood what I meant with proving algorithms. If you think proving the algorithms of your software means you've proven 1% of your software to be correct, you have no clue what programming is all about. Hint: it has nothing to do with typing code."

No that's not what I think and what I was saying. To be very clear:

I'm saying that the amount of code you can actually prove to be correct in the average application amount to 1% (a figure I just plucked out of the sky btw;), but very small nonetheless)

"You think in 'code', but that's not what you should do. 'Code' is the end result, it theoretical basis is somewhere else. If you give me a piece of code you wrote, it effectively has NO MEANING. What's more important is the theory behind that code: why did you write it the way you wrote it? If you're a professional, you'll answer: "because the design dictated that", which comes down to the algorithms designed dictated your code that way. If you're an amateur, you'll likely mumble something about wind direction, the temperature of your coffee etc."

I'll ignore all your assumptions about how I think and just ask you again, how do you prove all the 'soft' pieces of the software where you have no usably specification to be correct.

"Next time you ship something to a customer, think about WHY you made the decision to ship it at that moment and not a week before that. Was it because all unittests succeeded? (which shouldn't be a guideline according to you because succeeding tests don't prove correctness, right?) or was it because some 'confidence' or other 'believe-driven-development' hogwash rose above a given threshold? ;)"

The shipping point of software is always based on multiple concerns. Usually it comes down to this question: Is it good enough? Does my customer get what he expected? Not, can I prove that this will never fail. The answer to that is always no. If llblgen does meet that last requirement it should be in a museum, because it is truly unique.

Again I'm not saying you can't proof that algorithms can't be provably correct, just that the bulk of applications doesn't consist of 'algorithms' in the mathematical or complexity sense.

It is for these portions of the code that we can use all the help we can get. (unittests, integration tests, codereviews etc.)

Saying programmers first focus should be to prove their alghorithms to be correct is limiting and counterproductive.

stephan

# re: Correctness provability should be the goal, not testability@ Tuesday, November 20, 2007 10:16 AM

So in short: you're saying that most of the code in an application isn't about an algorithm and therefore proving it to be correct is pretty useless, as it makes up a very small part of the code, and therefore proving these to be correct is time consuming and the rest of the code isn't helped with it anyway?

I disagree. I find it essential that every random picked line of code has to have a theoretical basis, otherwise it can be removed because it's unnecessary.

Mind you: even some screen glue code might look dumb and boring, but it is code which represents an algorithm, because it was written in THAT order and not in a random other order. That must have a reason, and that reason is the important thing here.

I've proven the majority of the runtime code by hand indeed. It's not rocketscience. First of all, pre/post conditions are essential. Then you've to use algorithms which are already proven to be correct: this increases quality as the algorithm and its scope is known, so you can just implement it.

Our experience with the 300,000 lines of code of LLBLGen Pro is that almost all bugs in the code are in projection errors, i.e.: projecting the algorithm onto code. So i.o.w.: the algorithm wasn't implemented correctly.

There's unfortunately not a real automated scenario possible at the moment for checking projections onto code, (which basicly comes down to compiling the algorithm in a DSL to C#), so there will be mistakes in this, as a human has to read the code again and do the checking.

The main point is that you seem to argue that there's no real solid evidence what the code should do in the first place. I find that a little strange. I never write code without knowing exactly what it should do, how else can I write the code? I mean: the code is the representation of functionality in executable form, resulting from algorithms projected onto code, where the algorithms are the design how the functionality should work in executable form. That thus means that you can't have code which doesn't have a reason to be there.

Take a customer-order edit screen and its features. Algorithm: read customer, read orders of customer, display customer fields, display orders, let user select order -> display selected order -> enter edit loop -> exit edit loop -> persist changes (== other algorithm). After you know THAT, you can write it in code.

If you think that's code without an algorithm, how on earth can you possibly create such a screen which works properly?

Perhaps you find the software you ship to be good enough if it passes a set of tests and the customer likes the blue color of the screens. However it might be that the software has to produce results which are always correct, and the results are based on data which is entered into the system or calculated based on input, you know the core of your app.

You don't prove that kind of code? You 'trust' yourself that the code you wrote is correct? I don't think so.

As we're all human, we indeed need triggers which go off when we make a mistake. But that should be their only reason of existence.

What annoys me is that by saying people should strive for provability of software, it is apparently a bad thing to say, because it's impossible, or counterproductive etc. however at the same time, the alternatives are simply not there: according to test-oriented developers, what IS there to make the quality of software better (i.e. it works as expected)? More tests? How many?

Unclear. So people who want to improve the quality of their software are left in the dark with nothing that helps. As if writing software is something completely not scientific and equal to producing a work of art.

FransBouma

# re: Correctness provability should be the goal, not testability@ Tuesday, November 20, 2007 11:06 AM

There's a couple of things that puzzle me here.

One is, if you've proven that your codebase is correct, why would you need unit-tests then. If you've proven that for all inputs it produces correct outputs, feeding it some inputs and checking the corresponding output would seem to be an exercise in futility. I guess you need them for your projection which you do by hand again? Isn't that what a lot of bugs are? Errors in translating the recipe in your head to code on screen?

Secondly I would love all this theoretical stuff translated into a real-world scenario. You say it's not that hard. Prove it!(pun intended:)).

I've done some of this stuff in college and to produce a mathematical correct proof of a simple 4 line loop we needed more that 2 pages of pager. You can understand my skepticism...

You say you've done this for a codebase of 300000 so obviously we're not talking about the same thing. I know I know, you're proving the original algorith, but was does that mean eventually. You say pre and postconditions are  important. With a sorting algorithm I can say, pre: the list may or may not be sorted, Post: The list is sorted. Fine, that's seems very provable.(although by no means easy) But what happens on our order form where you have al sorts of buttons the user can push. Do I make seperate pre and postconditions for each button press? It's starting to sound like a unit test...:)

"Take a customer-order edit screen and its features. Algorithm: read customer, read orders of customer, display customer fields, display orders, let user select order -> display selected order -> enter edit loop -> exit edit loop -> persist changes (== other algorithm). After you know THAT, you can write it in code."

Yes let's take this screen. It seems like a very common scenario, and exactly what i'm talking about. What you've listed here is not an algorithm. Its a program flow. One of many many possible flows. (the user might cancel, enter strange values, open another screen etc. etc.)

I would very much (and I really mean this) like to see what your concept of a proof of it's correctness would look like. Perhaps we're using different definitions for proof. To clarify, I'm talking about an actual mathematical proof. One that is built upon axioms and one that doesn't reduce this complex real-world scenario to an empty shell.

"Perhaps you find the software you ship to be good enough if it passes a set of tests and the customer likes the blue color of the screens. However it might be that the software has to produce results which are always correct, and the results are based on data which is entered into the system or calculated based on input, you know the core of your app.

You don't prove that kind of code? You 'trust' yourself that the code you wrote is correct? I don't think so. "

No I don't, I believe that anyone who thinks their code is 'correct' is fundamentally wrong.

And again, except for some very specialized banking applications and maybe a nasa app, I don't know of any other software that has been proven to be correct. If all this stuff is not rocket science you'd think they would have done it for the mach kernel of linux. They haven't, so I guess they're just lazy, and only 'think in code'. Ps. My screens are never blue, my customers prefer yellow....

One final point, you seem to think I'm a huge test driven design proponent. I'm not, I think of unit-tests as one of a number of tools programmers can use to increase the quality of the products.

And no, building software in the real world is not entirely scientific. I would like it to be more like that, but this is an area of constant ongoing research. Frankly coming from someone who seems to hold an active interest in the science of our field it's kind of puzzling you treat this as a solved problem.

stephan

# re: Correctness provability should be the goal, not testability@ Tuesday, November 20, 2007 6:02 PM

It is rather obvious (at least to me) that you don't actually understand what you're saying. Proving algorithms is useless for a real application - it is not extremely difficult to prove the correctness of a Stack<int> implementation, but it is trivially easy to make it crash by trying to add 10 billion ints to it. Adding a requirement for "less than 10 billion elements" won't help, as 9 billion will crash it just as well.

On the other hand, proving actual programs is of course impossible, for several reasons - you're using a third-party library, a compiler, an OS and hardware that you cannot control. (You should read Anderson's "Programming Satan's Computer".)

As for this claim:

[Dijkstra] "argues that a program execution is traversing a graph. This means that it's predicatable [sic] where you end up, by just following the graph. However with goto that's not the case."

we must be reading different documents. There is no mention of graphs or predictions or determinism in the paper you linked to; what Dijkstra actually says has nothing to do with the weird claim that a goto statement makes an algorithm unpredictable (honestly, what were you thinking?). Just as I already told you, Dijkstra says "In such a coordinate system it becomes an extremely complicated affair...".

I admire you as a programmer, but as a theorist I find that you have some weird ideas. Really weird.

Marcel Popescu

# re: Correctness provability should be the goal, not testability@ Wednesday, November 21, 2007 4:03 AM

Marcel:

"It is rather obvious (at least to me) that you don't actually understand what you're saying. Proving algorithms is useless for a real application - it is not extremely difficult to prove the correctness of a Stack<int> implementation, but it is trivially easy to make it crash by trying to add 10 billion ints to it. Adding a requirement for "less than 10 billion elements" won't help, as 9 billion will crash it just as well."

I'm not sure, but the above suggests you don't really grasp what I was talking about. I am talking about proving algorithms. That means: no code, no physical borders other than logical borders. A stack algorithm therefore is provable without having to refer to physical memory. I mean: if the power fails, the app is also crashing.

Implementation specifics, i.e. the specifics of the projection of the algorithm, can introduce limitations, e.g. "Maximum throughput is 10,000 records per minute" etc. THat doesn't mean the algorithm is flawed at all, it's a limitation of the projection, not the source. THAT's the whole point. You seem to keep these two together as a single entity, which is precisely what I'm arguing against! Because if you keep them tied together as a single entity, you can never solve a problem in the algorithm if a test fails, because it might also be a code error. The code isn't the algorithm, it's the projection of the algorithm.

"we must be reading different documents. There is no mention of graphs or predictions or determinism in the paper you linked to; what Dijkstra actually says has nothing to do with the weird claim that a goto statement makes an algorithm unpredictable (honestly, what were you thinking?). Just as I already told you, Dijkstra says "In such a coordinate system it becomes an extremely complicated affair..."."

I was saying things about code, not algorithms. you made that mistake again. Dijkstra's paper is quite clear actually. He talks about pointers to locations, so the program moves from one location to the next. This is a directed graph. The paper isn't a book, it's formal, but it says everything that's necessary to understand the point.

FransBouma

# re: Correctness provability should be the goal, not testability@ Wednesday, November 21, 2007 4:51 AM

Frans, I think it would be better if you worded your arguments a little more carefully.

First you say the following:

"To say that this code is correct, one has to prove the code is correct, a set of tests won't cut it. " and "Proving code correctness

Proving code to be correct isn't easy, but it should be your main focus when writing solid software. Your first step should be to prove that your algorithms are correct. If an algorithm fails to be correct, you can save yourself the trouble typing the executable form of it (the code representing the algorithm) as it will never result in solid correct software."

Seems pretty clear to me. You're saying Proving code is correct is the goal and proving the original algorithms correct is the first step in obtaining that goal.

But now you're saying:

"I am talking about proving algorithms. That means: no code, no physical borders other than logical borders. A stack algorithm therefore is provable without having to refer to physical memory. I mean: if the power fails, the app is also crashing."

But that's your first step right? The goal is still to PROVE the code to be correct. Or is it?

I think the problem is that you seem to be inventing your own definitions of known scientific concepts.

First: Code correctness is usually done by formal verification using for various algebra's. This is an existing discipline and known to be quite difficult for all but the most trivial routines. Read the literature. You're talking about something totally different. You're proving some of the algorithms you're using are correct and very carefully translate (or project) those to code. This is simply not formal verification of your code and you do not end up with a proof that your code is correct.

That was the original point wasn't it? To prove the correctness of your code? You don't do that.

I guess you're in the same boat as the rest of us after all...

Secondly, and this is really besides the point but while we're at it: A non-deterministic algorithm (depending on whether you're looking at it from complexity theory or from traditional algorithm design has multiple paths it can take or can take multiple paths at once. You don't know or don't care which path is to be chosen.

See this wiki for a nice explanation:

en.wikipedia.org/.../Non-deterministic_algorithm

There is nothing non-deterministic about a goto. You know exactly which path will be chosen. You don't end up in a mystery location,it's not random where you end up and you don't jump to two places at the same time. The paper you cited does not in any way make any reference to non-deterministic behaviour. It does say that the go-to makes the relationship between the static and dynamic behaviour of an algorithm more difficult to understand. I think you probably meant something like this too, but the word non-deterministic is incorrect in this context.

Stephan

# re: Correctness provability should be the goal, not testability@ Wednesday, November 21, 2007 4:54 AM

(this is starting to become lengthy)

"One is, if you've proven that your codebase is correct, why would you need unit-tests then. If you've proven that for all inputs it produces correct outputs, feeding it some inputs and checking the corresponding output would seem to be an exercise in futility. I guess you need them for your projection which you do by hand again? Isn't that what a lot of bugs are? Errors in translating the recipe in your head to code on screen?"

You too seem to make the mistake Marcel made: I argued we should prove our algorithms to be correct. AFTER that, you can make a projection to code. THEN you should review the code to see if the code resembles the algorithm in executable form (i.e. if you have made the proper projection).

IF you then get an error in your code, it's the projection, not the algorithm. Without the prove, you can't be sure it's the code OR the algorithm or BOTH, you then will end up patching the code perhaps but you'll be unaware if that's even feasable (i.e.: if the algorithm is flawed, you can patch all you want, but it will never fix the problem).

People often focus on 'Oh dear, it has unlimited inputs, how am I going to prove this!", and give up. But it's not that hard, just use logic: is there a state possible when this can go wrong? If so, how do we get there? Ah, that's impossible, so the state is impossible, or: oh, we can get there -> algorithm has a flaw.

"I've done some of this stuff in college and to produce a mathematical correct proof of a simple 4 line loop we needed more that 2 pages of pager. You can understand my skepticism..."

Sure, as I've done that too. :) I'm not talking about mathematical correct proof (although you can often prove it mathematically), I'm talking about logical proof: is it possible that this fails? If not, it's correct. This is the core of scientific proof: you prove that it's unprovable that it's incorrect.

"You say you've done this for a codebase of 300000 so obviously we're not talking about the same thing. I know I know, you're proving the original algorith, but was does that mean eventually. You say pre and postconditions are  important. With a sorting algorithm I can say, pre: the list may or may not be sorted, Post: The list is sorted. Fine, that's seems very provable.(although by no means easy) But what happens on our order form where you have al sorts of buttons the user can push. Do I make seperate pre and postconditions for each button press? It's starting to sound like a unit test...:)"

heh :). I did say you can use automated tests to verify if your projection is correct, however you have to verify your tests as well (which means you have to verify that they verify what you want to verify).

For a lot of our code, proven algorithms are used, so that saved me from doing that again. Programming is a lot about graphs for example, so if you use the proven graph algorithms out there, you can get very far. The thing is that a lot of developers don't know that for the majority of things there are already proven algorithms out there. People should spend 5 minutes checking if there are proven algorithms for what they want to do, and if so, use these instead of cooking up some home-brewn algo which they also refuse to prove to be correct.

Then, you have the set of algorithms which are new, or specific to your application. I then take them one at a time. Write down an algorithm, first globally then detailed. Then I'll go over it and reason why this would fail. Often you'll then already run into things which make the algorithm a bit flawed so you either have to patch it there or opt for another one. You repeat this process until you can't find a possible state in which it can go wrong AND a path to that state which is possible. At that point, you can go to your editor and type in the code.

You're not done after that. The single most important thing after proving the algorithm is that you have to verify that your projection is indeed the projection of the algorithm you were suppose to implement. If you forget an element in the algorithm, if you write code which doesn't mimic a part of it, you have buggy code, and only THEN you can detect a bug and fix it, as it's in the projection which mismatches with what it should represent. If you don't have that check, if you think the algorithm IS the code, you can never verify if the code is correct. You can just assume it's correct because you wrote it ;).

After you've verified your projection (the code) with the algorithm, you are done. You can run unittests to see if you're indeed capable of doing a review of the code and you haven't overlooked something, but it's indeed a pretty redundant exercize: the necessity of testing suggests you are incapable somewhere else. However it doesn't hurt writing tests to see if you overlooked something in the verification, however you have to be sure the tests test your verification and not shoot some random things at the code.

Does this sound like a waterfall design approach? No not at all. A person who hammers out code is supposed to know what s/he's hammering in and the reason why THESE statements are written in THAT order and not some other code.

"

"Take a customer-order edit screen and its features. Algorithm: read customer, read orders of customer, display customer fields, display orders, let user select order -> display selected order -> enter edit loop -> exit edit loop -> persist changes (== other algorithm). After you know THAT, you can write it in code."

Yes let's take this screen. It seems like a very common scenario, and exactly what i'm talking about. What you've listed here is not an algorithm. Its a program flow. One of many many possible flows. (the user might cancel, enter strange values, open another screen etc. etc.)

I would very much (and I really mean this) like to see what your concept of a proof of it's correctness would look like. Perhaps we're using different definitions for proof. To clarify, I'm talking about an actual mathematical proof. One that is built upon axioms and one that doesn't reduce this complex real-world scenario to an empty shell."

I'm talking about proof similar to this proof:

en.wikipedia.org/.../Two_Generals_Problem

And in there the proof that there's no protocol possible which solves the problem.

I cooked that algo up when I was typing the text, so if it's not al algorithm to you, I'm sorry. The thing is that if I look up Algorithm on Wikipedia

en.wikipedia.org/.../Algorithm

I see that it describes a set of well defined instructions to complete a given task. Sorting a list isn't something different than editing an order record: both are tasks which steps, states etc.

Due to logical problems like the Halting problem (which is proven to be impossible), as Wikipedia describes here, en.wikipedia.org/.../Correctness, the correctness of a total application isn't that easy. That doesn't mean we can't seek for correctness in algorithms inside the application. Which is my point with the article. In theory I should use Hoare logic but as I'm the one doing the algorithm design, verification and projection, I use a less formal mathematical descriptions for algorithms also during proves. But as said, in a lot of cases, algorithms are already there and proving the rest is often a matter of pre-/post-condition determination, and reasoning why this wouldn't work.

"And again, except for some very specialized banking applications and maybe a nasa app, I don't know of any other software that has been proven to be correct. If all this stuff is not rocket science you'd think they would have done it for the mach kernel of linux. They haven't, so I guess they're just lazy, and only 'think in code'. Ps. My screens are never blue, my customers prefer yellow...."

The verification if something is correct is always about 'what's correctness in this context'. This means that if a programmer thinks the algorithm A is good enough for the task to complete, and the programmer is confident the code is correctly mimicing A, the programmer will likely skip the process of proving A is correct and also will skip verifying that the code written is actually A in executable form. If there's never a bugreport for A's implementation, the programmer will get away with it. We're all human, we're all taking that risk once in a while because there are other limitations in life like the amount of time given. That doesn't mean we shouldn't TRY. All I was saying is that people should focus on that and give it a TRY. Though people find writing a couple of unittests easier and take the chance of getting away with it and accept the fact that if a bug appears to be in the code they wrote, they will fix it. However, it might be that there are no ways to fix it, that the damage for the customer is too big. I.o.w.: I think we should try harder and also stop with the excuse that software development is an 'art' alone. There are definitely parts of our work which aren't formally provable to be correct in nominal time (so NP-hard ;)) but it is not impossible to prove core elements of our work to be correct, however we have to give it a try at least.

"And no, building software in the real world is not entirely scientific. I would like it to be more like that, but this is an area of constant ongoing research. Frankly coming from someone who seems to hold an active interest in the science of our field it's kind of puzzling you treat this as a solved problem. "

Perhaps I over-stated it a bit, as in todays agile-TDD oriented blog-osphere saying something that hurts TDD fans' believes isn't going to make you populair and definitely not understood.

It's not entirely scientific, but it's also not entirely unscientific. For the parts which are scientific (and I believe the majority of the work on a software project is based on that) we should put more effort in proving that what we're doing is actually right, as running tests isn't going to help one bit in that area.

I'll stop now, as I've said everything wanted say.

FransBouma

# re: Correctness provability should be the goal, not testability@ Wednesday, November 21, 2007 5:17 AM

(Ok one more then... :))

Stephan: Ok, I agree: code correctness (not algorithms) via formal analysis of that code is indeed not what I meant, that's why I described the steps to take. You can use Hoare logic for example, which can be formal but the idea is that you use logic with pre-/post-conditions which is something you have to do anyway for code, otherwise writing the code is an undoable exercise

The idea is that if you prove your algorithm to be correct, and verify that the code written is representing that algorithm, the code is then also correct. If not, the algorithm isn't correct. That's the idea. The weakest link is indeed the projection of the algorithm onto code.

However if you don't prove your algorithms, you have nothing to debug if a flaw is found in the code. If you HAVE proven the algorithms, you can debug the code as you know what to look for: the code apparently has a projection error.

In my interpretation of the paper, I concluded that it is indeed about making it impossible to understand why you arrive at the goto label and therefore not possible to determine if the code is correct or not. As this was several years ago, I should have looked it up before adding the sentence to the article, you're completely right in that case.

FransBouma

# re: Correctness provability should be the goal, not testability@ Thursday, November 22, 2007 3:52 AM

Ok I think we're more or less in line then;)

What's been bothering me for a long time is the huge divide between what everybody says programmers should be doing and what I actually see done around me. You know, common stuff like proper documentation, unit tests, gathering proper specification etc etc. I work with a lot of different teams and I see the same pattern each and every time. Nobody does all of it. Most teams don't even do half of it. To me that says our expectations of what the average programmer is willing to do is totally different from reality. I'll be the first to admin I don't always do this stuff either. I'm not saying we should then abandon all these useful concepts, but I do think maybe a healthy dose of realism might be in order. That's why someone saying you  should prove all your code seemed like the wrong way to go to me.

If anything I think these kind of discussions prove that we're still a long way off from working in a sane industry:)

stephan