Common mistakes which lead to corrupted invariants
- by Dave B.
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.
