Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

My main source of income is web development and through this I have come to enjoy the wonders of programming as my knowledge of different languages has increased over the years through work and personal play. At some point I reached a decision that my college education was not enough and that I wanted to go back to school to get a university degree in either computer science or software engineering. I have tried a number of things in my life and it took me a while before I found something that I feel is a passion and this is it.

There is one aspect of this area of study that I find throws me off though. I find the formal methods of proving program correctness a challenge. It is not that I have trouble writing code correctly, I can look at an algorithm and see how it is correct or flawed but I struggle sometimes to translate this into formal definitions. I have gotten perfect or near perfect marks on every programming assignment I have done at the college level but I recently got a swath of textbooks from a guy from univeristy of waterloo and found that I have had trouble when it comes to a few of the formalisms.

Well at this point its really just one thing specifically, It would really help me if some of you could provide to me some good examples of common mistakes which lead to corrupted invariants, especially in loops. I have a few software engineering and computer science textbooks but they only show how things should be. I would like to know how things go wrong so that it is easier to recognize when it happens. Its almost embarrassing to broach this subject because formalisms are really basic foundations upon which matters of substance are built.

I want to overcome this now so that it does not hinder me later.

share|improve this question
    
Thanks for the responses. Interesting things to think about. Cheers. –  Dave B. Jan 10 '11 at 21:32

3 Answers 3

Common Numeric Problems

Overflow, underflow.

What is wrong with

int newArrayLength = arr.length * 2;
T[] newArray = new T[newArrayLength];

?

Floating Point

Failure to account for NaN when comparing using <, >, <=, =>.

What is wrong with this

double max(double a, double b) { return a < b ? b : a; }

?

Filtering

Failing to account for duplicates.

What is wrong with

int numberOfInstancesIn(T[] items, T[] set) {
  int count = 0;
  for (int i = 0; i < items.length; ++i) {
    T item = items[i];
    for (int j = 0; j < set.length; ++j) {
      if (item == set[j]) { ++count; }
    }
  }
  return count;
}

Assuming two objects are not the same because they have different names

What is wrong with

class Pair {
  T* a;
  T* b;

  ~C() {
    delete a;
    delete b;
  }
}

?

share|improve this answer

My favorite: failure to initialize correctly

 minIndex = 0
 minValue= someRandomValue # NOT someList[minIndex]
 for i in range( 0, len(someList) ) # NOT range( 1, len(someList) ): 
     assert min(someList) == someList[minIndex] # not true initially
     if someList[i] <= someList[minIndex]:
         minIndex= i
         minValue= someList[minIndex]

The initialization should be based on actual data.

Other common one -- failure to maintain the invariant in the presence of if-statements.

oddSum= 0
evenSum= 0 
for i in range( 0, len(someList) ):
    if i % 2 == 0:
        evenSum += someList[i]
    else:
        # some random statement that doesn't update oddSum
    assert evenSum + oddSum == sum( someList[0:i] )
        # The above may not always be true

The trick is this.

For each "but they only show how things should be" you can mess up any statement and you'll have an error.

While you -- personally -- can see the mistake, you have to realize that other random programmers don't see the errors and write random code that doesn't satisfy the invariant.

It's an exercise in "Genetic Programming" -- introduce a random mutation and see if the invariant is true or not. As you read other people's code, you'll see that they make completely random errors.

share|improve this answer
    
An invariant has the assumption that it is correct before you execute the relevant code. I may be misunderstanding something, but that would mean that if something isn't initialized properly that would be a bug, but not necessarily a failed invariant. en.wikipedia.org/wiki/Invariant_(computer_science) –  Jason Baker Jan 10 '11 at 3:05
    
@Jason Baker: A failed invariant is a bug, so I'm not sure what hair you're splitting. Failure to initialize correctly means the invariant was never true. A common bug. –  S.Lott Jan 10 '11 at 3:23

In general, mutating state is the biggest cause (and may in fact be the only cause) of corrupted invariants. I don't mean to start the age-old imperative vs functional debate, but there's a reason why languages like Haskell are so popular amongst academics: it's much easier to prove purely functional code correct. Of course, whether functional code is better in general is a totally different discussion.

As an example, if I have an invariant that the variable foo must be less than 5 after each iteration of a loop, then the only way for that invariant to fail is to change the value of foo. Therefore if foo is less than 5 before the code starts and you don't change the value of foo, you can be sure that foo will be less than 5 when the loop ends.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.