CSE2011 Lecture 8

Loop invariants

• What is the loop invariant
  
  • In general it is an extremely difficult question to answer. It contains the essential difficulty in programming
    
  • Fundamentally it is the following
    
    • LI = totalWork = workToDo + workDone
      
  • Question a: does the loop terminate?
    
  • Question b: is the postcondition of OP true at loop end
    

Loop Design

• Find the loop invariant
  
• After consulting an oracle we have determined that the following is an appropriate loop invariant
  
  • This is the create part of programming
    
• Question 1
  
  • Make the loop invariant true at the start
    
• Question 2
  
  • Is the loop invariant still true after operation 2 is executed?
    
  • After operation2 show li first part is true
    
  • See effect of moving data from workToDo to workDone while maintaining the invariant