Lecture overview -- Keyboard shortcut: 'u'  Previous page: Andre anvendelser af assertions [Section] -- Keyboard shortcut: 'p'    Lecture notes - all slides and notes together  slide -- Keyboard shortcut: 't'  Help page about these notes  Alphabetic index  Course home  Play sound for this page -- Keyboard shortcut: 'y'  Page 31 : 31
Forelæsningsnoter i Objekt-orienteret Programmering
Designkontrakter og ansvarsfordeling
Løkkeinvarianter

Vi vender os her kort tilsidst mod andre anvendelser af assertions

Assertions finder anvendelse i andre sammenhænge end kontrakter

Løkkeinvarianter er en primær 'mekanisme' som tillader os at styre og ræsonnere om en løkke

  static int div(int x, int y){
    // require x > 0 && y > 0;   

    int rest = x;
    int quotient = 0;
    
    while (rest >= y) {
      // invariant rest + quotient * y = x;   
      // System.out.println(rest + quotient * y == x);   
      rest = rest - y;
      quotient = quotient + 1;
    }
    return (quotient);
    // ensure  rest + quotient * y = x && rest < y && rest >= 0;   
  } // end div

Et eksempel på en iterativ funktion med en løkke invariant.