Termination

Warum terminiert folgender Algorithmus für alle a,b?

void m3(int a, int b) {
      for (; a<=b; a++) {
            b+=a;
      }
}

b wäre ja immer größer als a (z.b. für b > a und a > 0 am Anfang), also muss der Überlauf eine Rolle spielen, aber wie?

ich nehme mal a,b in [-intmax/2 + 1, intmax/2] an. Wenn nach dem "while" b < 1 ist, terminiert es beim nächsten Durchgang wegen b < 1 --> b-a < 1 --> b-a+1 < 1 ==> b < a. nach maximal intmax Schritten ist aber einmal a = intmax/2 und wenn bis dahin immer noch b >= 1 ist, ist im nächsten Schritt b < 1.

Stimmt das? (Problem mit den Ungleichungen bei modulo)

Wie schreibe ich das im Hoare-Kalkül?

*push*

CStoll

fraage schrieb:

b wäre ja immer größer als a (z.b. für b > a und a > 0 am Anfang), also muss der Überlauf eine Rolle spielen, aber wie?

Ja, ich vermute auch, daß der Überlauf "schuld" ist - wenn b über INT_MAX wachsen würde, springt es um auf INT_MIN (=-INT_MAX-1), und schon hast du die Situation a>b (a ist (noch) nicht übergelaufen, b liegt irgendwo im Negativ-Bereich) und die Schleife bricht ab

CStoll schrieb:

fraage schrieb:

b wäre ja immer größer als a (z.b. für b > a und a > 0 am Anfang), also muss der Überlauf eine Rolle spielen, aber wie?

Ja, ich vermute auch, daß der Überlauf "schuld" ist - wenn b über INT_MAX wachsen würde, springt es um auf INT_MIN (=-INT_MAX-1)

sicher, dass der auf INT_MIN geht und nicht das Ergebnis modulo genommen wird?

sarfuan

Wie wär es, wenn ihr euch einfach den Wert von ~0+1 mal ausgeben lasst, anstatt hier fleißig (falsche) Vermutungen anzustellen?

CStoll

fraage schrieb:

sicher, dass der auf INT_MIN geht und nicht das Ergebnis modulo genommen wird?

relativ sicher - so funktioniert die Modulo-Arithmetik in C: INT_MAX+1 == INT_MIN (für unsigned: UINT_MAX+1 == 0)

PS: sarfuan's Vorschlag klingt sicher hilfreich - bau mal ein "cout<<a<<' '<<b<<endl;" bzw. "printf("%d %d\n",a,b);" in die Schleife ein und beobachte, wie sich die Werte entwickeln.

CStoll schrieb:

fraage schrieb:

sicher, dass der auf INT_MIN geht und nicht das Ergebnis modulo genommen wird?

relativ sicher - so funktioniert die Modulo-Arithmetik in C: INT_MAX+1 == INT_MIN (für unsigned: UINT_MAX+1 == 0)

ja, das bezweifle ich ja nicht, aber INT_MAX + 100 ist z.b. größer als INT_MIN

aber nicht in c++

long int schrieb:

aber nicht in c++

echt? bei meinem g++ 4.0.2 ist das so