Frans Bouma's blog - All Comments

re: "Re: I have a question about proving code correctness"

mattjcowan — Sun, 22 Jan 2012 07:02:30 GMT

Great post. I hope this is the beginning of a series of posts :-) The question you are responding to in this post is a great question, one that I've asked myself. Also, while startups are usually very different one from the other, they usually have unique pressures, such as out-of-band deadlines, competing agendas sometimes by stakeholders, chaotic resourcing, and having to be a scientist in the middle of all of it can be grueling. It would be interesting to take this discussion to a team, and see how to make this work out in a team atmosphere (ie: roles and responsibilities, scientist v. engineer). I appreciated the statement "it's sometimes not possible to do every step in the time it requires", that's a breath of fresh air, when sleep is becoming rare :-). Now, I need to learn more about describing and designing algorithms (without code), and "Formal methods". Keyvan, can you write some more about that ;-)

Cheers.

re: "Re: I have a question about proving code correctness"

Patrick Smacchia — Fri, 20 Jan 2012 19:11:47 GMT

IMHO there are two essential practices that makes unit testing extremely efficient to find bug, that you don't really mention: Code Contract (you barely mention it) and 100% Code Coverage.

When both Contracts and Full Coverage are used, one can be pretty confident that the code portion tested is pretty close to bug free (not 100% sure of course!). I wrote a post on that last week actually:

codebetter.com/.../non-trivial-and-real-world-feedbacks-on-writing-unit-tests

Also, you often mention the number of unit tests as a testing metric, while the metrics that really matters (IMHO) are the number of assertions checked (in tests or in contracts) and the percentage of code covered.

re: "Re: I have a question about proving code correctness"

FransBouma — Fri, 20 Jan 2012 15:58:55 GMT

@Keyvan Nayyeri

Thanks for your post :) As I (apparently not correctly) tried to explain in my post, I'm not a specialist in this field, so I tried to describe what I knew of software correctness proving and how I apply it in practice.

So what I tried to do was giving developers who have no notion of formal proving (as you said, it's a complicated field) some tools/ways of working that they can apply in their own daily work so they create more reliable / less buggy software. What you described so well 'software testing can at most only show there are bugs, not the absence of them', is unfortunately not well known among developers: what they most of the time think when they see all green unittests: "bugs are gone, ship it!". Some teams realize this though, and write a tremendous amount of tests, have rules like 'we need 100% code coverage' and other time wasters.

IMHO time not well spend. But as you said, it's very hard (complex, lot of work) to reach the goal of proving the complete system to be bugfree so some ways to get near that goal might already be helpful. That's what I tried to describe. Of course my post isn't a way to write software for a plane, it's not formal enough as you know.

re: "Re: I have a question about proving code correctness"

Keyvan Nayyeri — Fri, 20 Jan 2012 15:44:25 GMT

Frans,

I thought I have to jump in and leave some comments because your post includes some incorrect information. Unfortunately, this area is one of those areas where programmers and testers have a lot of misbeliefs because all they know is software testing.

You have to distinguish two different fields called Software Testing and Formal Methods. The former is relatively easily and includes all the things you know about unit testing and integration testing, and the latter is totally different and almost all the industrial programmers don't know about it because it's an advanced and complicated mechanism.

With software testing, what you're trying to achieve is improving the quality of software by reducing the number of bugs, exceptions, and errors that you can predict before a user catches them. With software testing what you can achieve at most is proving the presence of bugs not their absence. Even if you write millions of tests, you can't guarantee that there is no other bug or error.

Software testing works great for most industrial software systems that are not critical. At most, there is an incorrect output or an exception, but there are critical software systems that must be bug-free like those used in aviation, healthcare, or automotive.

Formal methods are a set of mathematical techniques to actually prove that a program runs without any bugs, errors, or exceptions in order to make sure that it's not going to kill somebody or make a catastrophic failure. Formal methods require a deep knowledge of mathematics and programming and it's the purpose of research at academia and industry for doctoral students and graduates (that's what I'm doing).

Formal methods like abstract interpretation or other techniques are used in systems like Astree (developed in France) that proves the absence of bugs in systems used in Airbus planes. There are also similar systems used in BMW cars and healthcare systems. There are also software verification tools used by NASA.

So unlike what you said, proving the correctness of a program doesn't involve those steps. It's a totally formal procedure that is hard to explain in a comment but you can read a book entitled Principles of Program Analysis on that.

You also mentioned that proving the correctness of a big software system is very difficult. It is, indeed, but that's done many times for many big systems and I mentioned some examples above.

I hope this helps clarifying the issue.

re: "Re: I have a question about proving code correctness"

Fri, 20 Jan 2012 15:16:02 GMT

"One problem I have with the agile mantra of 'Red, green, refactor' is that if you have a failing test but you don't know why it failed then it is useless."

Maybe worse than useless. If a test asserts failure without a message and without a clear test name its worse than useless. If a test blows up in an unexpected manner, not just a failed assert, it can be a good thing because it shows that you have a coverage problem.

In most of my day to day work, the idea of proofing is moot because the specifications are minimal or non-existent :P

re: "Re: I have a question about proving code correctness"

Eric K. — Fri, 20 Jan 2012 15:15:57 GMT

@Richard - I would suggest that writing the initial failing test is not useless, even if you don't know (or care) why it fails.

The point of the initial failing test is to show that the functionality you are testing doesn't *already* pass, before you write your implementation. Then, when you write your implementation and the test passes, you'll know it's your new code that causes the success, and not something incidental or overlooked.

It's the *combination* of the initial failing test run and the subsequent passing test that tells the developer what they need to know, not simply the passing test.

re: "Re: I have a question about proving code correctness"

Tudor — Fri, 20 Jan 2012 15:01:49 GMT

About "If you write a method that fails your test because it gives you back a NotImplementedException then you have wasted your time because you haven't learnt anything."

That's not quite true: checking that the unit test fails when the method is not implemented is also a way to make sure that the unit test is well written from the start, even in the simple of cases.

Also, it encourages the developer to write the test (executable specification) first, before the code is written, not the other way around, when he might be tempted to write a test that just reflects what the method is already doing, even if that is not the expected behavior.

So the general rule would be: never add/modify functionality, before writing at least a test first.

All unit tests don't prove in a mathematical way that the code is without bugs, just reduce that possibility.

re: "Re: I have a question about proving code correctness"

Richard Wright — Fri, 20 Jan 2012 14:03:47 GMT

Frans,

One problem I have with the agile mantra of 'Red, green, refactor' is that if you have a failing test but you don't know why it failed then it is useless.

If you write a method that fails your test because it gives you back a NotImplementedException then you have wasted your time because you haven't learnt anything.

But if your test fails for a reason that you weren't expecting then you have learnt something. Maybe your algorithm is incorrect.

Blindly following the agile method is pointless, IMHO. But using unit tests intelligently can teach you a lot about your code.

But, as you say, proving correctness is extremely difficult, if not impossible.

re: ORM Profiler release celebration: LLBLGen Pro 100 EUR discount

FransBouma — Sat, 01 Oct 2011 07:11:39 GMT

No not this month, upgrades get the same discount as always.

re: ORM Profiler release celebration: LLBLGen Pro 100 EUR discount

WayneBrantley — Sat, 01 Oct 2011 04:02:34 GMT

Any celebration for upgrades?