Schleifeninvariante bestimmen

[vaults]

Hallo Leute,

ich habe folgende Aufgabe und leider keinen Schimmer wie ich sie lösen soll.
Hier erstmal der Code:

static int f(int m, int n) {
  assert m <= n; // Vorbedingung P
  int s = m+n,
  i = m;
  assert ... // Schleifeninvariante Q

  while ( i <= n ) {
    s = s - 2*i;
    i = i + 1;
    assert ... // Schleifeninvariante Q
  }
  assert ... // Nachbedingung R
  return s;
}

Die Aufgaben lauten:
a)
Welchen Wert berechnet diese Methode? Formulieren Sie eine entsprechende Nachbedingung
R.

b)
Geben Sie eine geeignete Schleifeninvariante Q an, mit deren Hilfe die partielle Korrektheit
der Methode bezüglich P und R nachgewiesen werden kann. Sie brauchen
den Nachweis nicht zu führen.

c)
Formulieren Sie Q und R als Java-Ausdrücke, sodass diese in den obigen assert-
Anweisungen verwendet werden können.

Soweit ich das Verstanden habe ich eine Schleifeninvariante eine Beziehung zwischen den höchsten Werten die vor dem Eintritt in die Schleife gelten und den Werten die unverändert bleiben?

Wäre klasse wenn mir jemand helfen könnte wie ich da ran gehen muss.
Ich habe noch nicht einmal rausgefunden was die Funktion berechnet, mir ist klar wie die Schleife funktioniert, aber was sie berechnet ist mir schleierhaft.

Liebe Grüße

 

[SlaterB]

eine Schleifeninvariante bzw. jedes assert sagt irgendwas über Variablen aus,
am Anfang werden z.B. m und n verglichen,

in der Schleife verändern sich nur i und s, über i etwas zu erzählen/ zu prüfen wäre langweilig, i beginnt bei m, und wandert bis n,
dass i immer zwischen m und n liegt ergibt sich so automatisch, dass das nichtmal ein assert wert ist,

ganz offensichtlich geht es um s, was als einziges übrig bleibt und außerdem wird s schon am Anfang aus den Parametern m + n berechnet und dann ist s auch noch der Rückgabe wert,
s ist sowas von wichtig,

die Schleifeninvariante soll irgendwas über s aussagen, s = 4*m - n*i oder irgend sowas, also i spielt auch noch eine Rolle,
kannst du die Formel bestimmen?

stelle doch eine Wertetabelle auf, nimm bestimmte Beispiel-Paramater, z.B. 5 und 10, was ist s am Anfang, was ist in jedem Schleifendurchlauf s und i, was ist s am Ende?

 

[Der Müde Joe]

Was du weisst:
1. s <= 2 * n da (m <= n)

dann:
s = s - ( (2*m) + (2 * (m+1)) + (2 * (m+2)) +..+ (2 * n) )

da i = m im ersten durchlauf
dann i++ = (m+1) .... bis i<=n was heisst i==n also bis (m == n), da i anfangs m ist und immer +1 gerechnet wird.

 

[vaults]

Hallo Leute,

vielen Dank für eure Hilfe.
Ich habe mittlerweile rausbekommen was die Funktion berechnet, ob ich das in der Klausur auch rauskriege ist eine andere Frage, finde die Funktion sehr ominös.

Für obige Funktion kann auch geschrieben werden:

s = (m+n)*(m-n)

So wie ich den Sachverhalt verstanden habe ist dies auch gleichzeitig die Nachbedingung:

assert s == (m+n)*(m-n);

Jetzt fehlt mir nur noch der Schlüssel zum Verstehen der Schleifeninvariante, vielleicht könnt ihr mir noch ein wenig weiter helfen

Liebe Grüße

 

[vaults]

Moin Leute,

so ich habe folgende Schleifeninvariante bekommen:

l<=n && (l+n)*(m-n) == ((m+n)*(m-n))

Allerdings sollen scheinbar laut Aufgabenstellung die Invarianten Q ident sein.

Ich bekomme jedoch bei folgendem Code einen Fehler:

assert l<=n && (l+n)*(m-n) == ((m+n)*(m-n)); // Funktioniert wunderbar
		while (l <= n ){
			s = s - 2*l;
			l = l +1;
			assert l<=n && (l+n)*(m-n) == ((m+n)*(m-n)); // Hier Fehler

Zum einen wird l im letzen Schritt über n hochgezählt und fällt damit schon in die assert Anweisung rein.
Was habe ich falsch gemacht?

Gute Nacht und liebe Grüße

 

[SlaterB]

das mit dem l statt i kannst du jetzt grob vermutet vielleicht auch mit || abtrennen,
"entweder ist durch die Schleife l > n, (dann kann keine Aussage mehr getroffen werden, oder andererseits (für den spannenden Fall solange noch l <= n gilt: ..."
wobei hier l nach der Berechnung von s geändert wird, das ist sowieso bisschen komisch, das aktuelle s vom assert hängt doch eher von l-1 ab,

> (l+n)*(m-n) == (m+n)*(m-n)
ist dann in jedem Fall Quatsch, der rechte Teil ist doch eine Konstante, während links l variabel ist, zudem könnte man das meiste kürzen, bliebe l == m rüber, was auch recht wenig hilft,

ich habe in meinem vorherigen Posting ja nicht viel erzählt, aber zumindest eins doch ganz deutlich: Aussagen nur über l sind langweilig, es muss um s gehen!
s = irgendwas aus m und n und l,
wenn das die ganze Zeit gilt (vom Anfangswert aus leicht zu erkennen und in der Schleife halbwegs auch)
und am Ende dann l einen bestimmten bekannten Wert hat, erst dann kann man das Endergebnis aus n und m ausdrücken

 

[vaults]

Hallo,

vielen Dank für die Antwort so früh morgens.

es muss um s gehen! s = irgendwas aus m und n und l,

Ist es ja auch, es gilt:

s = (l+n)*(m-n)

sowie am Ende

(l+n)*(m-n) == (m+n)*(m-n)

LG

 

[SlaterB]

wieso schreibst du dann in der Schleife
> assert l<=n && (l+n)*(m-n) == ((m+n)*(m-n)); // Hier Fehler
?
da taucht nirgendwo s auf,
wenn du Gedanken neu sortiert hast kann man ja weiter überlegen

> (l+n)*(m-n) == (m+n)*(m-n)
ist nach wie vor triviale nichts aussagene Gleichung, daraus folgt nur dass l == m ist, was sowieso bekannt ist,
über den Wert von s wird nichts gesagt

-----


ist gewiss nichts einfaches, ich weiß die Lösung selber auch noch nicht unbedingt,
Der Müde Joe hat ja schon bisschen was geschrieben, was hoffentlich noch irgendwie Formel-hafter zu formulieren ist,
Beispiele und Wertetabellen könnten nach wie vor helfen

 

[vaults]

Moin,

also es gibt ein Beispiel mit Lösungen, anhand dieser Lösungen habe ich mich an der eigentlichen Schleife versucht und bin genau so vorgegangen.
Ich habe mal ein Bild gemacht, ich hoffe es wird klar wie ich auf meine Lösungen für meine eigentliche Schleife gekommen bin.

PS: Das Vorgehen ist von mir, nur der Code und die Lösungen waren gegeben.

Liebe Grüße,
Alex

 

[SlaterB]

viel neues ist ja nicht zu sagen, aber eins möchte ich anhand dieser Zusatzinfos erneut betonen:
in dem Beispiel geht es in der Schleifeninvariante auch um w, den letztlichen Rückgabewert,
i ist am Ende 0 und fällt deshalb aus der Nachbedingung raus, es bleibt eine Formel für w übrig

also was immer du auch machst,
in der Schleifeninvariante muss s in der Formel vorkommen,
alles andere ist unter Garantie entweder gleich falsch oder nur irrelevant