Opinion about "loop invariants", and are they often used in the industry?

Question

I recalled my first year of college (five years ago) when I passed the exam to take computer science out of the intro-level. The question arose about loop invariants, and I was wondering if cycle invariants were needed in this case, or if the question was just a bad example ... the question was to write an iterative definition for a factor function, and then prove that the function is correct.

The code I provided for the factorial was as follows:

public static int factorial(int x) { if ( x < 0 ){ throw new IllegalArgumentException("Parameter must be >= 0"); }else if ( x == 0 ){ return 1; }else{ int result = 1; for ( int i = 1; i <= x; i++ ){ result*=i; } return result; } } 

My own proof of correctness was a case-by-case proof, and in each I claimed that it was correct by definition (x! Is undefined for negative values, 0! Is 1, and x! 1 * 2 * 3 ... * x for positive x value). The professor wanted me to prove the cycle using the cycle invariant; however, my argument was that it was "by definition" correct, since the definition of "x!" for a positive integer, x is "the product of integers from 1 ... x", and the for-loop in the else clause is just a literal translation of this definition. Is the cycle invariant really necessary as proof of correctness in this case? How complicated should the loop be before the loop invariant (and the correct initialization and termination conditions) needed to prove the correctness?

Also, I was wondering ... how often is such formal evidence used in the industry? I found that about half of my courses are very theoretical and evidence-based, and about half are very realistic and coding, without any formal or theoretical materials. How much do they overlap in practice? If you use evidence in the industry, when do you use it (always, only if it's difficult, rarely, never)?

Edit
If we ourselves are convinced that part of the code is correct, can convince others (unofficially) that this is correct, and there are single tests in place, to what extent are formal proofs of correctness necessary?

Answer 1

To what extent does formal evidence need correctness?

It depends, of course, but I find it important that programmers know how to write code that is error-free, where it tends to be correct in design.

One example is the look-ahead concept, for example, in parsing, when the next input token is not “read”, then “looks,” and then possibly “returns” if it’s not that, but rather, “ looked, "and then maybe" accepted "if that's what you need. When, for example, writing loops to cycle through database records and retrieve subtotals, this simple change in perspective can lead to significant and more reliable code.

Another example is differential execution , a method that I came across many years ago. It seems that any algorithm should be re-executed in stages to gradually update its results. I use it extensively in user interfaces, where content can change dynamically. For a long time I felt that it worked in all cases, but could not be sure until I proved it, as at the bottom of my Wikipedia page . After that, I knew that if I adhered to some simple restrictions, I could rely on it to work, no matter how much code depended on it.

At the same time, we can be sure of the correctness of some algorithm, but it is very difficult to prove formally, because our methods of proof are bad. Consider a small type of bubbles. Obviously this works, but try to prove it formally by applying the rules to the source code. I did it, but it’s not easy. I have not tried more complex sorting algorithms.

Answer 2

The professor wanted me to prove the cycle using the cycle invariant;

Your professor wanted to make sure that you understood the invariants of the cycle, and not just something about a very simple function.

Is the cycle invariant really necessary as proof of correctness in this case?

Well, technically, no. For these reasons, you do not need to write a factorial function: just use the library function! But this is not an exercise item.

How complicated should the loop be before the loop invariant (and the correct initialization and termination conditions) needed to prove the correctness?

I know some smart people who can probably prove something without invariants, and then people who should use them even for trivial cases like the ones above. This is how to ask "how heavy is the rock before you need a wheelbarrow to move it?".

Also, I was wondering ... how often is such formal evidence used in the industry?

Is it written explicitly? Probably rare if you are not in certain industries . But I still think about them when writing any, but the simplest loop.

This is similar to the way I do not assign diagrams, but that does not mean that I never think about grammar, especially if I write some text that is really important. I can tell you what my pronoun is, even though I never bothered to put this fact on paper.

Answer 3

When you solve complex problems and write code that will be reused after you switch, you must go through the process of checking the correctness of each routine you write every day. Test-based development is a formalization of this idea, but its essence is as follows: you need to prove, at least for yourself and, preferably, for others (code review!), That the code you wrote will process all possible inputs and ways in the proper way.

Are we bickering about code invariants? Not. Do we add documents before you can register? Like. If the team does not like your code or your “proof”, you return to your box to fix it until it checks.

Answer 4

In recent years, “test-based development” under different names has been farthest from most people thinking about their code. This is rather a very cautious and repeated experimentation, rather than logical reasoning. Science versus math!

There is some use of preconditions, post-conditions, and loop / class invariants in languages ​​such as Eiffel, and upcoming support for "contracts" in .NET 4.0 may help to popularize these ideas.

Personally, I use statements quite rarely these days; when I iterate over a structure, I usually no longer write it as a loop. I write this as a request, for example. Linq in C # or similar things in other languages ​​like JS. Thus, there is less imperative manipulation of the state to make a mistake (usually it is not). And any statement about the results will be redundant, as it will simply repeat the conditions in the query: in the query approach, you describe the results that you want.

This does not mean that I never use statements; but I tend to use them in combination with unit test, and only for very complex algorithms that perform some complex in-place mutation of the collection; in such cases there is no “built-in” way to request the results that I want; I have to write the algorithm imperatively (perhaps because it would be terribly expensive to copy the entire data structure), so I cover it with statements to help my unit test flags identify internal problems.