12-invariant.html


<!doctype html>
<html lang="en" class="no-js">
  <head>
    
      <meta charset="utf-8">
      <meta name="viewport" content="width=device-width,initial-scale=1">
      
      
        <link rel="canonical" href="https://nus-cs1010.github.io/2021-s1/12-invariant.html">
      
      
      <link rel="shortcut icon" href="assets/images/favicon.png">
      <meta name="generator" content="mkdocs-1.1.2, mkdocs-material-6.0.2">
    
    
        <title>12. Loop Invariant - CS1010 Programming Methodology</title>
      
    
      <link rel="stylesheet" href="assets/stylesheets/main.38780c08.min.css">
      
        
        <link rel="stylesheet" href="assets/stylesheets/palette.3f72e892.min.css">
        
          
          <meta name="theme-color" content="#009485">
        
      
        <link href="https://fonts.gstatic.com" rel="preconnect" crossorigin>
        <link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Roboto:300,400,400i,700%7CRoboto+Mono&display=fallback">
        <style>body,input{font-family:"Roboto",-apple-system,BlinkMacSystemFont,Helvetica,Arial,sans-serif}code,kbd,pre{font-family:"Roboto Mono",SFMono-Regular,Consolas,Menlo,monospace}</style>
      
    
      <link rel="stylesheet" href="stylesheets/extra.css">
    
      <link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Roboto:400,700">
    
      <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Lora:ital,wght@0,400;0,500;0,600;0,700;1,400;1,500;1,600;1,700&display=swap">
    
    
  </head>
  
  
    <body dir="ltr" data-md-color-scheme="" data-md-color-primary="teal" data-md-color-accent="">
      
  
    <input class="md-toggle" data-md-toggle="drawer" type="checkbox" id="__drawer" autocomplete="off">
    <input class="md-toggle" data-md-toggle="search" type="checkbox" id="__search" autocomplete="off">
    <label class="md-overlay" for="__drawer"></label>
    <div data-md-component="skip">
      
        
        <a href="#unit-12-reasoning-about-loops" class="md-skip">
          Skip to content
        </a>
      
    </div>
    <div data-md-component="announce">
      
    </div>
    
      <header class="md-header" data-md-component="header">
  <nav class="md-header-nav md-grid" aria-label="Header">
    <a href="https://nus-cs1010.github.io/2021-s1" title="CS1010 Programming Methodology" class="md-header-nav__button md-logo" aria-label="CS1010 Programming Methodology">
      
  
  <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12 8a3 3 0 003-3 3 3 0 00-3-3 3 3 0 00-3 3 3 3 0 003 3m0 3.54C9.64 9.35 6.5 8 3 8v11c3.5 0 6.64 1.35 9 3.54 2.36-2.19 5.5-3.54 9-3.54V8c-3.5 0-6.64 1.35-9 3.54z"/></svg>

    </a>
    <label class="md-header-nav__button md-icon" for="__drawer">
      <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M3 6h18v2H3V6m0 5h18v2H3v-2m0 5h18v2H3v-2z"/></svg>
    </label>
    <div class="md-header-nav__title" data-md-component="header-title">
      
        <div class="md-header-nav__ellipsis">
          <span class="md-header-nav__topic md-ellipsis">
            CS1010 Programming Methodology
          </span>
          <span class="md-header-nav__topic md-ellipsis">
            
              12. Loop Invariant
            
          </span>
        </div>
      
    </div>
    
      <label class="md-header-nav__button md-icon" for="__search">
        <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M9.5 3A6.5 6.5 0 0116 9.5c0 1.61-.59 3.09-1.56 4.23l.27.27h.79l5 5-1.5 1.5-5-5v-.79l-.27-.27A6.516 6.516 0 019.5 16 6.5 6.5 0 013 9.5 6.5 6.5 0 019.5 3m0 2C7 5 5 7 5 9.5S7 14 9.5 14 14 12 14 9.5 12 5 9.5 5z"/></svg>
      </label>
      
<div class="md-search" data-md-component="search" role="dialog">
  <label class="md-search__overlay" for="__search"></label>
  <div class="md-search__inner" role="search">
    <form class="md-search__form" name="search">
      <input type="text" class="md-search__input" name="query" aria-label="Search" placeholder="Search" autocapitalize="off" autocorrect="off" autocomplete="off" spellcheck="false" data-md-component="search-query" data-md-state="active">
      <label class="md-search__icon md-icon" for="__search">
        <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M9.5 3A6.5 6.5 0 0116 9.5c0 1.61-.59 3.09-1.56 4.23l.27.27h.79l5 5-1.5 1.5-5-5v-.79l-.27-.27A6.516 6.516 0 019.5 16 6.5 6.5 0 013 9.5 6.5 6.5 0 019.5 3m0 2C7 5 5 7 5 9.5S7 14 9.5 14 14 12 14 9.5 12 5 9.5 5z"/></svg>
        <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M20 11v2H8l5.5 5.5-1.42 1.42L4.16 12l7.92-7.92L13.5 5.5 8 11h12z"/></svg>
      </label>
      <button type="reset" class="md-search__icon md-icon" aria-label="Clear" data-md-component="search-reset" tabindex="-1">
        <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M19 6.41L17.59 5 12 10.59 6.41 5 5 6.41 10.59 12 5 17.59 6.41 19 12 13.41 17.59 19 19 17.59 13.41 12 19 6.41z"/></svg>
      </button>
    </form>
    <div class="md-search__output">
      <div class="md-search__scrollwrap" data-md-scrollfix>
        <div class="md-search-result" data-md-component="search-result">
          <div class="md-search-result__meta">
            Initializing search
          </div>
          <ol class="md-search-result__list"></ol>
        </div>
      </div>
    </div>
  </div>
</div>
    
    
  </nav>
</header>
    
    <div class="md-container" data-md-component="container">
      
      
      <main class="md-main" data-md-component="main">
        <div class="md-main__inner md-grid">
          
            
              <div class="md-sidebar md-sidebar--primary" data-md-component="navigation">
                <div class="md-sidebar__scrollwrap">
                  <div class="md-sidebar__inner">
                    <nav class="md-nav md-nav--primary" aria-label="Navigation" data-md-level="0">
  <label class="md-nav__title" for="__drawer">
    <a href="https://nus-cs1010.github.io/2021-s1" title="CS1010 Programming Methodology" class="md-nav__button md-logo" aria-label="CS1010 Programming Methodology">
      
  
  <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12 8a3 3 0 003-3 3 3 0 00-3-3 3 3 0 00-3 3 3 3 0 003 3m0 3.54C9.64 9.35 6.5 8 3 8v11c3.5 0 6.64 1.35 9 3.54 2.36-2.19 5.5-3.54 9-3.54V8c-3.5 0-6.64 1.35-9 3.54z"/></svg>

    </a>
    CS1010 Programming Methodology
  </label>
  
  <ul class="md-nav__list" data-md-scrollfix>
    
      
  <li class="md-nav__item">
    <a href="index.html" class="md-nav__link">
      Home
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="midterm.html" class="md-nav__link">
      Midterm
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="final.html" class="md-nav__link">
      Final
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="pe1.html" class="md-nav__link">
      PE1
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="pe2.html" class="md-nav__link">
      PE2
    </a>
  </li>

    
  <li class="md-nav__item md-nav__item--nested">
    
      <input class="md-nav__toggle md-toggle" data-md-toggle="nav-6" type="checkbox" id="nav-6">
    
    <label class="md-nav__link" for="nav-6">
      General
      <span class="md-nav__icon md-icon"></span>
    </label>
    <nav class="md-nav" aria-label="General" data-md-level="1">
      <label class="md-nav__title" for="nav-6">
        <span class="md-nav__icon md-icon"></span>
        General
      </label>
      <ul class="md-nav__list" data-md-scrollfix>
        
        
  <li class="md-nav__item">
    <a href="about.html" class="md-nav__link">
      About CS1010
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="outcomes.html" class="md-nav__link">
      Learning Outcomes
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="schedule.html" class="md-nav__link">
      Schedule
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="accounts.html" class="md-nav__link">
      Accounts
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="policies.html" class="md-nav__link">
      Policies
    </a>
  </li>

        
      </ul>
    </nav>
  </li>

    
  <li class="md-nav__item md-nav__item--active md-nav__item--nested">
    
      <input class="md-nav__toggle md-toggle" data-md-toggle="nav-7" type="checkbox" id="nav-7" checked>
    
    <label class="md-nav__link" for="nav-7">
      Notes
      <span class="md-nav__icon md-icon"></span>
    </label>
    <nav class="md-nav" aria-label="Notes" data-md-level="1">
      <label class="md-nav__title" for="nav-7">
        <span class="md-nav__icon md-icon"></span>
        Notes
      </label>
      <ul class="md-nav__list" data-md-scrollfix>
        
        
  <li class="md-nav__item">
    <a href="01-program.html" class="md-nav__link">
      1. What is a Program?
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="02-algo.html" class="md-nav__link">
      2. Computational Problem & Algorithms
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="03-func.html" class="md-nav__link">
      3. Functions
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="04-type.html" class="md-nav__link">
      4. Types
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="05-first-c.html" class="md-nav__link">
      5. First C Program
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="06-cs1010-io.html" class="md-nav__link">
      6. CS1010 I/O Library
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="07-arithmetic-ops.html" class="md-nav__link">
      7. Arithmetic Operations
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="08-if-else.html" class="md-nav__link">
      8. Conditionals
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="09-logical-exp.html" class="md-nav__link">
      9. Logical Expressions
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="10-assert.html" class="md-nav__link">
      10. Assertion
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="11-loop.html" class="md-nav__link">
      11. Loops
    </a>
  </li>

        
  <li class="md-nav__item md-nav__item--active">
    
    <input class="md-nav__toggle md-toggle" data-md-toggle="toc" type="checkbox" id="__toc">
    
      
      <label class="md-nav__link md-nav__link--active" for="__toc">
        12. Loop Invariant
        <span class="md-nav__icon md-icon"></span>
      </label>
    
    <a href="12-invariant.html" class="md-nav__link md-nav__link--active">
      12. Loop Invariant
    </a>
    
      
<nav class="md-nav md-nav--secondary" aria-label="Table of contents">
  
  
    <label class="md-nav__title" for="__toc">
      <span class="md-nav__icon md-icon"></span>
      Table of contents
    </label>
    <ul class="md-nav__list" data-md-scrollfix>
      
        <li class="md-nav__item">
  <a href="#learning-objectives" class="md-nav__link">
    Learning Objectives
  </a>
  
</li>
      
        <li class="md-nav__item">
  <a href="#using-assertions" class="md-nav__link">
    Using Assertions
  </a>
  
</li>
      
        <li class="md-nav__item">
  <a href="#loop-invariant" class="md-nav__link">
    Loop Invariant
  </a>
  
</li>
      
        <li class="md-nav__item">
  <a href="#problem-set-12" class="md-nav__link">
    Problem Set 12
  </a>
  
    <nav class="md-nav" aria-label="Problem Set 12">
      <ul class="md-nav__list">
        
          <li class="md-nav__item">
  <a href="#problem-121" class="md-nav__link">
    Problem 12.1
  </a>
  
</li>
        
      </ul>
    </nav>
  
</li>
      
    </ul>
  
</nav>
    
  </li>

        
  <li class="md-nav__item">
    <a href="13-call-stack.html" class="md-nav__link">
      13. Call Stack
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="14-pointers.html" class="md-nav__link">
      14. Memory Addresses
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="15-array.html" class="md-nav__link">
      15. Array
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="16-string.html" class="md-nav__link">
      16. String
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="17-call-by-reference.html" class="md-nav__link">
      17. Call by Reference
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="18-heap.html" class="md-nav__link">
      18. Heap
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="19-md-array.html" class="md-nav__link">
      19. Multi-dimensional Arrays
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="20-macro.html" class="md-nav__link">
      20. C Preprocessing
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="21-assert.html" class="md-nav__link">
      21. The assert macro
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="22-efficiency.html" class="md-nav__link">
      22. Efficiency
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="23-search.html" class="md-nav__link">
      23. Searching
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="24-sort.html" class="md-nav__link">
      24. Sorting
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="25-tower.html" class="md-nav__link">
      25. Tower of Hanoi
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="26-permutation.html" class="md-nav__link">
      26. Permutation
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="27-queens.html" class="md-nav__link">
      27. N Queens
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="28-struct.html" class="md-nav__link">
      28. Struct
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="29-stdio.html" class="md-nav__link">
      29. Standard I/O
    </a>
  </li>

        
      </ul>
    </nav>
  </li>

    
  <li class="md-nav__item md-nav__item--nested">
    
      <input class="md-nav__toggle md-toggle" data-md-toggle="nav-8" type="checkbox" id="nav-8">
    
    <label class="md-nav__link" for="nav-8">
      Exercises
      <span class="md-nav__icon md-icon"></span>
    </label>
    <nav class="md-nav" aria-label="Exercises" data-md-level="1">
      <label class="md-nav__title" for="nav-8">
        <span class="md-nav__icon md-icon"></span>
        Exercises
      </label>
      <ul class="md-nav__list" data-md-scrollfix>
        
        
  <li class="md-nav__item">
    <a href="ex00.html" class="md-nav__link">
      0. Echo, Divide, Quadratic
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="ex01.html" class="md-nav__link">
      1. GCD, Day, Leap
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="ex02.html" class="md-nav__link">
      2. Binary, Rectangle, Fibonacci
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="ex03.html" class="md-nav__link">
      3. Weekday, Circle, Histogram
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="ex04.html" class="md-nav__link">
      4. Fill, Sudoku
    </a>
  </li>

        
      </ul>
    </nav>
  </li>

    
  <li class="md-nav__item md-nav__item--nested">
    
      <input class="md-nav__toggle md-toggle" data-md-toggle="nav-9" type="checkbox" id="nav-9">
    
    <label class="md-nav__link" for="nav-9">
      Assignments
      <span class="md-nav__icon md-icon"></span>
    </label>
    <nav class="md-nav" aria-label="Assignments" data-md-level="1">
      <label class="md-nav__title" for="nav-9">
        <span class="md-nav__icon md-icon"></span>
        Assignments
      </label>
      <ul class="md-nav__list" data-md-scrollfix>
        
        
  <li class="md-nav__item">
    <a href="assignment.html" class="md-nav__link">
      Overview
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as01.html" class="md-nav__link">
      1. Box, Digits, Suffix, Taxi
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as02.html" class="md-nav__link">
      2. Collatz, Triangle, Prime, Pattern
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as03.html" class="md-nav__link">
      3. ID, Kendall, Max, CountingSort
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as04.html" class="md-nav__link">
      4. SelectionSort, Mastermind
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as05.html" class="md-nav__link">
      5. Contact, Social, Life
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as06.html" class="md-nav__link">
      6. Add, Frequency, Permutation
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as07.html" class="md-nav__link">
      7. Peak, Sort, Inversion
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as08.html" class="md-nav__link">
      8. Walk, Maze
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="as09.html" class="md-nav__link">
      9. Digits
    </a>
  </li>

        
      </ul>
    </nav>
  </li>

    
  <li class="md-nav__item">
    <a href="readings.html" class="md-nav__link">
      Readings
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="c-in-cs1010.html" class="md-nav__link">
      C in CS1010
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="library.html" class="md-nav__link">
      CS1010 I/O Library
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="style.html" class="md-nav__link">
      C Style Convention
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="documentation.html" class="md-nav__link">
      C Documentation Guide
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="messages.html" class="md-nav__link">
      Compiler Messages
    </a>
  </li>

    
  <li class="md-nav__item md-nav__item--nested">
    
      <input class="md-nav__toggle md-toggle" data-md-toggle="nav-16" type="checkbox" id="nav-16">
    
    <label class="md-nav__link" for="nav-16">
      Software/Tools
      <span class="md-nav__icon md-icon"></span>
    </label>
    <nav class="md-nav" aria-label="Software/Tools" data-md-level="1">
      <label class="md-nav__title" for="nav-16">
        <span class="md-nav__icon md-icon"></span>
        Software/Tools
      </label>
      <ul class="md-nav__list" data-md-scrollfix>
        
        
  <li class="md-nav__item">
    <a href="environments.html" class="md-nav__link">
      Programming Environments
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="unix.html" class="md-nav__link">
      UNIX
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="clang.html" class="md-nav__link">
      CLang
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="vim.html" class="md-nav__link">
      Vim
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="tmate.html" class="md-nav__link">
      TMate
    </a>
  </li>

        
  <li class="md-nav__item">
    <a href="zoom.html" class="md-nav__link">
      Zoom
    </a>
  </li>

        
      </ul>
    </nav>
  </li>

    
  <li class="md-nav__item">
    <a href="archive.html" class="md-nav__link">
      Older Announcements
    </a>
  </li>

    
  <li class="md-nav__item">
    <a href="1819s1.html" class="md-nav__link">
      18/19 Sem 1
    </a>
  </li>

    
  </ul>
</nav>
                  </div>
                </div>
              </div>
            
            
              <div class="md-sidebar md-sidebar--secondary" data-md-component="toc">
                <div class="md-sidebar__scrollwrap">
                  <div class="md-sidebar__inner">
                    
<nav class="md-nav md-nav--secondary" aria-label="Table of contents">
  
  
    <label class="md-nav__title" for="__toc">
      <span class="md-nav__icon md-icon"></span>
      Table of contents
    </label>
    <ul class="md-nav__list" data-md-scrollfix>
      
        <li class="md-nav__item">
  <a href="#learning-objectives" class="md-nav__link">
    Learning Objectives
  </a>
  
</li>
      
        <li class="md-nav__item">
  <a href="#using-assertions" class="md-nav__link">
    Using Assertions
  </a>
  
</li>
      
        <li class="md-nav__item">
  <a href="#loop-invariant" class="md-nav__link">
    Loop Invariant
  </a>
  
</li>
      
        <li class="md-nav__item">
  <a href="#problem-set-12" class="md-nav__link">
    Problem Set 12
  </a>
  
    <nav class="md-nav" aria-label="Problem Set 12">
      <ul class="md-nav__list">
        
          <li class="md-nav__item">
  <a href="#problem-121" class="md-nav__link">
    Problem 12.1
  </a>
  
</li>
        
      </ul>
    </nav>
  
</li>
      
    </ul>
  
</nav>
                  </div>
                </div>
              </div>
            
          
          <div class="md-content">
            <article class="md-content__inner md-typeset">
              
                
                <h1 id="unit-12-reasoning-about-loops">Unit 12: Reasoning About Loops</h1>
<h2 id="learning-objectives">Learning Objectives</h2>
<p>After this unit, students should:</p>
<ul>
<li>understand how assertions can be derived in a loop;</li>
<li>understand how assertions can help us understand the behavior of a loop</li>
<li>understand what is a loop invariant;</li>
<li>be able to argue why a given loop invariant is true;</li>
<li>be able to derive simple loop invariant of a given loop.</li>
</ul>
<h2 id="using-assertions">Using Assertions</h2>
<p>We have seen how we can use assertions to reason about the state of our program at different points of execution for conditional <code>if</code>-<code>else</code> statements.  We can apply the same techniques to loops.  Take the simple program below:</p>
<table class="highlighttable"><tr><td class="linenos"><div class="linenodiv"><pre><span></span> 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15</pre></div></td><td class="code"><div class="highlight"><pre><span></span><code><span class="kt">long</span> <span class="nf">count</span><span class="p">(</span><span class="kt">long</span> <span class="n">n</span><span class="p">)</span> <span class="p">{</span>
  <span class="kt">long</span> <span class="n">y</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
  <span class="kt">long</span> <span class="n">x</span> <span class="o">=</span> <span class="n">n</span><span class="p">;</span>
  <span class="k">while</span> <span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="mi">0</span><span class="p">)</span> <span class="p">{</span>
    <span class="c1">// line A</span>
    <span class="n">x</span> <span class="o">-=</span> <span class="mi">1</span><span class="p">;</span>
    <span class="c1">// line B</span>
    <span class="k">if</span> <span class="p">(</span><span class="n">x</span> <span class="o">%</span> <span class="mi">5</span> <span class="o">==</span> <span class="mi">0</span><span class="p">)</span> <span class="p">{</span>
      <span class="c1">// line C</span>
      <span class="n">y</span> <span class="o">+=</span> <span class="mi">1</span><span class="p">;</span>
    <span class="p">}</span>
  <span class="p">}</span>
  <span class="c1">// line D</span>
  <span class="k">return</span> <span class="n">y</span><span class="p">;</span>
<span class="p">}</span>
</code></pre></div>
</td></tr></table>
<p>Before we continue, study this program and try to analyze what the function is counting and returning.</p>
<p>To do this more systematically, we can use assertions.  Let's ask ourselves: what can be said about the variables <code>x</code> and <code>y</code> at Lines A, B, C?  Let start with <code>x</code> first.</p>
<ul>
<li>Line A is the first line after entering the loop, so we can reason that to enter the loop (the first time or subsequent times), <code>x &gt; 0</code>.</li>
<li>We can also derive that, at Line A, <code>x &lt;= n</code>.  This is less obvious: since we initialize the <code>x</code> to <code>n</code>, and after Line A, we only decrease <code>x</code>, <code>x</code> can never be more than <code>n</code>.</li>
<li>At Line B, we decrease <code>x</code> by 1, so now <code>x &gt;= 0 &amp;&amp; x &lt; n</code> must be true.</li>
<li>At Line C, <code>x % 5 == 0</code> (i.e., x is multiple of 5) must <em>also</em> be true (since it is in the true block of the <code>if</code> block).</li>
<li>At Line D, we already exit from the loop, and the only way to exit here is that <code>x &gt; 0</code> is false.  So we know that <code>x &lt;= 0</code>.</li>
</ul>
<p>Let's annotate the code with the assertions:
<table class="highlighttable"><tr><td class="linenos"><div class="linenodiv"><pre><span></span> 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15</pre></div></td><td class="code"><div class="highlight"><pre><span></span><code><span class="kt">long</span> <span class="nf">count</span><span class="p">(</span><span class="kt">long</span> <span class="n">n</span><span class="p">)</span> <span class="p">{</span>
  <span class="kt">long</span> <span class="n">y</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
  <span class="kt">long</span> <span class="n">x</span> <span class="o">=</span> <span class="n">n</span><span class="p">;</span>
  <span class="k">while</span> <span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="mi">0</span><span class="p">)</span> <span class="p">{</span>
    <span class="c1">// { (x &gt; 0) &amp;&amp; (x &lt;= n) }</span>
    <span class="n">x</span> <span class="o">-=</span> <span class="mi">1</span><span class="p">;</span>
    <span class="c1">// { (x &gt;= 0) &amp;&amp; (x &lt; n) }</span>
    <span class="k">if</span> <span class="p">(</span><span class="n">x</span> <span class="o">%</span> <span class="mi">5</span> <span class="o">==</span> <span class="mi">0</span><span class="p">)</span> <span class="p">{</span>
      <span class="c1">// { (x &gt;= 0) &amp;&amp; (x &lt; n) &amp;&amp; x is multiple of 5 }</span>
      <span class="n">y</span> <span class="o">+=</span> <span class="mi">1</span><span class="p">;</span>
    <span class="p">}</span>
  <span class="p">}</span>
  <span class="c1">// { x &lt;= 0 }</span>
  <span class="k">return</span> <span class="n">y</span><span class="p">;</span>
<span class="p">}</span>
</code></pre></div>
</td></tr></table></p>
<p>What can be said about <code>y</code>?  It should be clear now that we increment <code>y</code> for every value between 0 and <code>n-1</code> (inclusive) that is a multiple of 5, based on the condition on Line C.  That is, it is counting the number of multiple of 5s between 0 and n-1.</p>
<h2 id="loop-invariant">Loop Invariant</h2>
<p>In the last unit, we say that there are five questions that we have to think about when designing loops.  The fifth question is: what is the <em>loop invariant</em>?  A loop invariant is an assertion that is true before the loop, after each iteration of the loop, and after the loop.  Thinking about the loop invariant is helpful to convince ourselves that a loop is correct, or to identify bugs in a loop.</p>
<p>Let's see an example of a loop invariant.  Consider the example of calculating a factorial using a loop as before.  To make the invariant simpler, let's tweak the loop slightly and start looping from <code>i</code> equals 1 up to <code>n</code>.</p>
<table class="highlighttable"><tr><td class="linenos"><div class="linenodiv"><pre><span></span> 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18</pre></div></td><td class="code"><div class="highlight"><pre><span></span><code><span class="kt">long</span> <span class="nf">factorial</span><span class="p">(</span><span class="kt">long</span> <span class="n">n</span><span class="p">)</span>
<span class="p">{</span>
  <span class="k">if</span> <span class="p">(</span><span class="n">n</span> <span class="o">==</span> <span class="mi">0</span><span class="p">)</span> <span class="p">{</span>
      <span class="k">return</span> <span class="mi">1</span><span class="p">;</span>
  <span class="p">}</span>
  <span class="kt">long</span> <span class="n">product</span> <span class="o">=</span> <span class="mi">1</span><span class="p">;</span>
  <span class="kt">long</span> <span class="n">i</span> <span class="o">=</span> <span class="mi">1</span><span class="p">;</span>
  <span class="c1">// Line A: before the loop</span>
  <span class="k">while</span> <span class="p">(</span><span class="n">i</span> <span class="o">&lt;</span> <span class="n">n</span><span class="p">)</span> <span class="p">{</span>
    <span class="c1">// Line B: beginning of each iteration</span>
    <span class="n">i</span> <span class="o">+=</span> <span class="mi">1</span><span class="p">;</span>
    <span class="c1">// Line C</span>
    <span class="n">product</span> <span class="o">*=</span> <span class="n">i</span><span class="p">;</span>
    <span class="c1">// Line D: after each iteration</span>
  <span class="p">}</span>
  <span class="c1">// Line E: after the loop</span>
  <span class="k">return</span> <span class="n">product</span><span class="p">;</span>
<span class="p">}</span>
</code></pre></div>
</td></tr></table>
<p>Line A is where we want to identify the assertion before the loop; Line D is where we want to identify the assertion after each iteration of the loop.  Line E is where we want to identify the assertion after the loop.  We added Lines B and C to help us reason about the assertions at Line D.</p>
<p>For this function, the assertion at line A, D, and E are the same, they are all <code>{ product == i! }</code>!  Thus, we say that this loop has the invariant <code>{ product == i! }</code>.</p>
<table class="highlighttable"><tr><td class="linenos"><div class="linenodiv"><pre><span></span> 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18</pre></div></td><td class="code"><div class="highlight"><pre><span></span><code><span class="kt">long</span> <span class="nf">factorial</span><span class="p">(</span><span class="kt">long</span> <span class="n">n</span><span class="p">)</span>
<span class="p">{</span>
  <span class="k">if</span> <span class="p">(</span><span class="n">n</span> <span class="o">==</span> <span class="mi">0</span><span class="p">)</span> <span class="p">{</span>
      <span class="k">return</span> <span class="mi">1</span><span class="p">;</span>
  <span class="p">}</span>
  <span class="kt">long</span> <span class="n">product</span> <span class="o">=</span> <span class="mi">1</span><span class="p">;</span>
  <span class="kt">long</span> <span class="n">i</span> <span class="o">=</span> <span class="mi">1</span><span class="p">;</span>
  <span class="c1">// A: { product == i! }</span>
  <span class="k">while</span> <span class="p">(</span><span class="n">i</span> <span class="o">&lt;</span> <span class="n">n</span><span class="p">)</span> <span class="p">{</span>
    <span class="c1">// B: { product == i! }</span>
    <span class="n">i</span> <span class="o">+=</span> <span class="mi">1</span><span class="p">;</span>
    <span class="c1">// C: { product == (i-1)! }</span>
    <span class="n">product</span> <span class="o">*=</span> <span class="n">i</span><span class="p">;</span>
    <span class="c1">// D: { product == i! }</span>
  <span class="p">}</span>
  <span class="c1">// E: { product == i! }</span>
  <span class="k">return</span> <span class="n">product</span><span class="p">;</span>
<span class="p">}</span>
</code></pre></div>
</td></tr></table>
<p>Let's see why the assertions labeled above hold.</p>
<p>On Line A, the assertion is obvious.  Since <code>product</code> is 1, <code>i</code> is 1, and 1! is 1.  The assertion <code>{ product == i! }</code> holds.</p>
<p>Let's look at Line B.  We need to argue that this assertion holds for every iteration.  This is a bit more tricky.  Let's first consider the first iteration and come back to the subsequent iterations later.  In the first iteration, the values of <code>product</code> and <code>i</code> do not change from Line A to Line B, so the assertion still holds.</p>
<p>On Line 11, we increment <code>i</code>.  So, at Line C of the first iteration, we have <code>{ product == (i-1)! }</code>.</p>
<p>On Line 13, we update <code>product</code> by multiplying it with <code>i</code>.  So, we have on Line D of the first iteration that <code>{ product == i! }</code> again.</p>
<p>Now, let's look at the second iteration.  There is no change to the variables <code>product</code> and <code>i</code>, between Line D of the first iteration and Line B of the second iteration.  So the assertion <code>{ product == i! }</code> still holds.  From this point onwards, we can apply the same argument over and over again, and see that the assertions on Lines B, C, and D hold for every iteration!</p>
<div class="admonition tips">
<p class="admonition-title">Link to CS1231</p>
<p>A more succinct and formal way to prove the above is to use a technique call <em>induction</em> taught in CS1231.  We will not require the use of induction in CS1010, however.</p>
</div>
<p>After we exit the loop, we can also assert that <code>i == n</code>, and so combining <code>product == i! &amp;&amp; i == n</code> we have <code>product == n!</code>, which is what we want.  The loop therefore correctly computes <code>n!</code>.</p>
<h2 id="problem-set-12">Problem Set 12</h2>
<h3 id="problem-121">Problem 12.1</h3>
<p>(a) Consider the algorithm to find the maximum among a list of integers <span class="arithmatex">\(L\)</span> with at least one element (<span class="arithmatex">\(k &gt; 0\)</span>) below:</p>
<p><img alt="max" src="figures/max-flowchart/max-flowchart.013.png" /></p>
<p>The loop invariant for this loop must hold at the three points marked with the red dots: before the loop, after each iteration of the loop, and after the loop.</p>
<p>State the loop invariant, explain why it holds at the three points above, and threfore argue that the loop above correctly finds the maximum among the elements of the list <span class="arithmatex">\(L\)</span>.  </p>
<p>(b) Now, consider a slightly different algorithm to find the maximum among a list of integers <span class="arithmatex">\(L\)</span> with at least one element (<span class="arithmatex">\(k &gt; 0\)</span>) below:</p>
<p><img alt="max" src="figures/max-flowchart/max-flowchart.014.png" /></p>
<p>Explain why you cannot find a loop invariant similar to Part (a) above, and therefore show that the algorithm does not correctly find the maximum in certain cases.</p>
                
              
            </article>
          </div>
        </div>
      </main>
      
        
<footer class="md-footer">
  
    <div class="md-footer-nav">
      <nav class="md-footer-nav__inner md-grid" aria-label="Footer">
        
          <a href="11-loop.html" class="md-footer-nav__link md-footer-nav__link--prev" rel="prev">
            <div class="md-footer-nav__button md-icon">
              <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M20 11v2H8l5.5 5.5-1.42 1.42L4.16 12l7.92-7.92L13.5 5.5 8 11h12z"/></svg>
            </div>
            <div class="md-footer-nav__title">
              <div class="md-ellipsis">
                <span class="md-footer-nav__direction">
                  Previous
                </span>
                11. Loops
              </div>
            </div>
          </a>
        
        
          <a href="13-call-stack.html" class="md-footer-nav__link md-footer-nav__link--next" rel="next">
            <div class="md-footer-nav__title">
              <div class="md-ellipsis">
                <span class="md-footer-nav__direction">
                  Next
                </span>
                13. Call Stack
              </div>
            </div>
            <div class="md-footer-nav__button md-icon">
              <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M4 11v2h12l-5.5 5.5 1.42 1.42L19.84 12l-7.92-7.92L10.5 5.5 16 11H4z"/></svg>
            </div>
          </a>
        
      </nav>
    </div>
  
  <div class="md-footer-meta md-typeset">
    <div class="md-footer-meta__inner md-grid">
      <div class="md-footer-copyright">
        
          <div class="md-footer-copyright__highlight">
            Copyright by Department of Computer Science, National University of Singapore 2020
          </div>
        
        Made with
        <a href="https://squidfunk.github.io/mkdocs-material/" target="_blank" rel="noopener">
          Material for MkDocs
        </a>
      </div>
      
    </div>
  </div>
</footer>
      
    </div>
    
      <script src="assets/javascripts/vendor.77e55a48.min.js"></script>
      <script src="assets/javascripts/bundle.9554a270.min.js"></script><script id="__lang" type="application/json">{"clipboard.copy": "Copy to clipboard", "clipboard.copied": "Copied to clipboard", "search.config.lang": "en", "search.config.pipeline": "trimmer, stopWordFilter", "search.config.separator": "[\\s\\-]+", "search.result.placeholder": "Type to start searching", "search.result.none": "No matching documents", "search.result.one": "1 matching document", "search.result.other": "# matching documents", "search.result.more.one": "1 more on this page", "search.result.more.other": "# more on this page", "search.result.term.missing": "Missing"}</script>
      
      <script>
        app = initialize({
          base: ".",
          features: [],
          search: Object.assign({
            worker: "assets/javascripts/worker/search.4ac00218.min.js"
          }, typeof search !== "undefined" && search)
        })
      </script>
      
        <script src="javascripts/config.js"></script>
      
        <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
      
        <script src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js"></script>
      
    
  </body>
</html>