Termination

• Geradeausprogramme halten (terminieren) immer:

  Eingabe a, b;  int c := a; a := b; b := c; Ausgabe a, b;
  

• Zählschleifen halten immer:

  für Zahl a von 0 bis 9 { Ausgabe (a); }
  

• beliebige Schleifen?

  Zahl a = 0;
  while ( a*a != 125 ) { a := a + 1; }