Schleifeninvariante & Nachbedingung

[Lunarix94]

Huhu,
ich konnte mein Problem von gestern lösen, jedoch geht es nun mit großen Schritten auf die Klausur zu.

Eine Aufgabe, dieser Typ kam die letzten Jahre immer dran, verstehe ich noch nicht.
Es geht um die Bildung der Schleifeninvariante & Nachbedingung.

Um mal ein Klausurbeispiel zu geben, gegeben:

static int f(int m, int n) {
  assert m>=0 && n>0; // Vorbedingung P
  int s = 0,
  i = 0;
  assert ... // Schleifeninvariante Q
  while ( s <= m ) {
    s = s + n;
    i = i + 1;
    assert ... // Schleifeninvariante Q
  }
  i= i-1;
  assert ... // Nachbedingung R
  return i;
}

Die Aufgabe, auch immer identisch:
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.


So. Nun stehe ich aber vor der Frage wie ich anfangen soll.
Ich schätze es ist auch am schlausten mit a anzufangen, also was berechnet die Methode.

i ist gesucht. i wird immer um 1 erhöht wenn s <= m ist und dabei s = s + n.
Das heißt doch, dass ich wissen muss wie oft diese while ausgeführt wird. Das kann man vielleicht in einer Summe ausdrücken. Also von s = 0 sum bis m+1 von n. Oder? Wie gehe ich vor? (auch bei den anderen Teilaufgaben habe ich keine Ahnung.


Hier noch eine andere Aufgabe dazu, vielleicht versteh ichs besser anhand von 2 Beispielen:

Spoiler

static int f(int n) {
assert n >= 1; // Vorbedingung P
int s = 1,
i = 0;
assert ...; // Schleifeninvariante Q
while (s < n) {
s = 2*s;
i = i + 1;
assert ...; // Schleifeninvariante Q
}
assert ...; // Nachbedingung R
return i;
}

Vielen lieben Dank an alle die mir bisher so gut geholfen haben und helfen werden!

 

[kaoZ]

Ok ich versuchs mal ,

zu Aufgabe a).

Die Methode berechnet die Division, des

Devidenden m

durch durch den angegebenen

Divisior n

man könnte also die Nachbedingung dementsprechend formulieren

assert i != m / n : "Die Eingabeparameter erfüllen die Nachbedingungen nicht !"

zu Aufgabe b)

 

[Lunarix94]

Und der Weg dahin? Die Lösung stimmt, aber wie kommst du darauf? Bitte so ausführlich wie möglich, damit ich es nachvollziehen und selber umsetzen kann

 

[kaoZ]

Nehmen wir uns mal die eigentliche Methode ohne assertions vor:

	static int f(int m, int n){
		
		int s = 0;
		int i = 0;

		while( s <= m){
			s = s + n;
			i++;
		}
		
		i--;
		return i;
	}

Solange s kleiner oder gleich m ist,

wird s + n addiert und die Summe in s gespeichert.
i jeweils um +1 inkrementiert.

sobald bis die Bedingung erfüllt ist, sprich

s == m

ist wird die Schleife nach nochmaliger ausführung verlassen,

i um -1 dekrementiert
und i zurückgegeben.

Konkret bedeutet das jetzt wenn wir z.B für m 30 einsetzen würden, und für n 3:

solange s(0) <= m(30) ist s = s(0) + n(3)

dies bedeutet konkret

i = 1 | s = 3
i = 2 | s = 6
i = 3 | s = 9
i = 4 | s = 12
i = 5 | s = 15
i = 6 | s = 18
i = 7 | s = 21
i = 8 | s = 24
i = 9 | s = 27
i = 10 |s = 30
i = 11 | s = 33

jetzt wird die Schleife Verlassen und

i um -1 dekrementiert ( da die Schleife 11 mal duchlaufen wird , was an der bedingung <= liegt )

dies führt du der Ausgabe und dem Ergebnis 10 , wobei s in diesem Fall dann 33 und nicht wie angenommen 30 wäre , dies liegt an der Bedingung

<=

würdest du dies

gleich

weglassen wäre die Ausgabe 9 und nicht 10.

[TIPP]Wenn du dieses Programm im Debugger laufen lässt kannst du die Wertbelegung der Variablen Schritt für Schritt beobachten.[/TIPP]

[EDIT]Ich vermute mal Stark das es einfach nur des Schwierigkeitsgrades halber mit dieser unnötigen Bedingung geknüpft ist , vereinfacht dargestellt wäre es ( allerdings würde dann wiederrum bei 20 : 3
7 und nicht 6 als Wert herauskommen ) [/EDIT]

Spoiler: Vereinfacht

public class Foo {

	static int f(int m, int n){
		
		int s = 0;
		int i = 0;

		while( s < m){
			s = s + n;
			i++;
		}
		return i;
	}

 

[Lunarix94]

Gut soweit verstehe ich es, aber wie kommst du dann auf die Lösung m/n? Es könnte ja genauso auch m-n-irgendwas oder sonstwas sein. wie kannst du diesen weg als einzig richtigen finden?


[EDIT]Ich mein, ich kann es durchlaufen, das bekomm ich hin, aber ich kann daraus dann nicht schlussfolgen wie das Ergebnis ist. ich sehe zwar Eingabe m = 30, n = 3, -> i =10, da kann ichs mir denken, ja, aber was wenn ich z.b. m = 5 und n=2 nehme? Dann kann ich da ja niemals drauf kommen, dass es m/n ist, es kann dann ja genausogut ein anderer Weg sein[/EDIT]

 

[kaoZ]

Du meinst wenn man diese Methode jetzt nicht ausführen könnte und lediglich vor sich auf einem Blatt stehen hat ?

Naja dies kannst du an der Schleife erkennen.

Nehmen wir doch mal an wir hätten keine Werte die wir einsetzen könnten ,

das bedeutet nichts anderes als das i sowie auch s inkrementiert werden .

sprich beide Werte werden erhöht bis die Schleifenbedingung erfüllt ist, i wird dann um 1 dekrementiert und ausgegeben ( dies bedeutet i ist immer kleiner als s , und s wird bei jedem Schleifendurchgang um +n erhöht, demnach müsste n * i = m sein ).

da in der lokalen Hilfsvariable jeweils immer der Wert aus n + s gespeichert wird weißt du das dieser Fall n-mal eintritt bis s == m ist.

würdest du rein gedanklich jetzt für beide Eingabeparameter 10 einsetzen,

sähe die "Konkrete" Bedingung in Pseudocode so aus

solange( s <= 10){
  s = 0 + 10;
  i = i + 1;
}

anhand der Bedingung (kleiner ODER gleich) kannst du sehen das diese Schleife 2 mal ausgeführt wird.

Daraus lässt sich schließen das Quotientenwert eines Terms(Quotienten) gesucht wird.

leicht schwer verständlich in Worte zu fassen

 

[Lunarix94]

Ja so mein ich das. In der Klausur hab ich das wie im ersten Post geschrieben liegen, mehr nicht, und muss die Aufgaben lösen :/.

Wie siehts denn mit diesem Beispiel aus?
Wie löse ich das nur vom Angucken?

static int f(int m, int n) {
  assert m>=0; // Vorbedingung P
  int i = m-1,
  x = 0;
  assert ... // Schleifeninvariante Q
    while (i >= 0) {
    x = x-2*i+n;
    i = i-1;
    assert ... // Schleifeninvariante Q
  }
  assert ... // Nachbedingung R
  return x;
}

Und generell, wie bastel ich dann die Scheifeninvariante dazu?

Lösung dazu:

Spoiler

a) Die Methode berechnet offensichtlich den Wert m· n−(SUMME:j=0 bis m-1 von 2j). Eine entsprechende Nachbedingung ist daher R : x = m · n − (SUMME:j=0 bis m-1 von 2j).

b) Eine zum Nachweis der partiellen Korrektheit von f bezüglich P und R geeignete
Schleifeninvariante ist Q : x = (m − 1 − i) · n − (SUMME:j=i+1 bis m-1 von 2j) ^ −1 <= i <= m − 1.

c) Mögliche Java-Ausdrücke für R und Q lauten:
R: assert x==m*n-(m-1)*m;
Q: assert x==(m-1-i)*n-(m-1)*m+i*(i+1) && -1<=i && i<=m-1;

Leider hab ich keine Plan wie auf das kommen soll...

[EDIT]Super wäre ein "Kochrezept" für alle diese Aufgabentypen[/EDIT]