Termination (Beispiele)

• solange (a ungleich b) {
      if (a > b) { a := a - b; }
      else       { b := b - a; }
  }
  

  beachte Invariante: a und b sind positive ganze Zahlen. a + b > 0 und a + b nimmt ab.

• solange (a > 0) { a := abrunden (a/2); }
  

  beachte: a nimmt ab.

• solange (x > 1) {
      if (x ist gerade)  { x := x/2; }
      else { x := 3 * x + 1; }
  }