Methoden Schleifeninvariante Assert Anweisungen

[vaults]

Moin Leute,

ich soll für folgende Methode, zu Beginn herausfinden was Sie berechnet, und dann geeignete Vorbdingung, Nachbedinung und Schleifeninvariante finden.

Hier ist die Methode:

public static int unknown(int x, int n){
		// Vorbedingung P
		int i, s;
		i = 0;
		s = x;
		// Schleifeninvariante Q
		while (i<n){
			i = i + 1;
			s = s + x + i;
			// Schleifeninvariante Q
		}
		// Nachbedingung R
		System.out.println("I ist: "+i+" S ist: "+s);
		return s;
	}

Das Problem ist, dass ich mir nicht klar ist, was diese Funktion mathematisch berechnet, grundsätzlich liefert Sie ja für alle Zahlen ein Ergebnis.

Die Vorbedingung P beschreibt die mathematischen bedingungen welche beim Aufruf der Methode erfüllt sein müssen.

Die Schleifeninvariante beschreibt die mathematische Zusammensetzung von (in diesem Falle) s

Die Nachbedingung überprüft das Ergebnis von s.

Ich habe mir nun als Vorbedingung, da er sonst in die Schleife nicht reingeht überlegt,

assert n > 0;			// Vorbedingung P

zu schreiben.

i wird pro Iterationsschritt lediglich einen hochgezählt, n-mal und erhät daher den Wert von n.
Die Nachbedingung sollte daher folgendes enthalten:

assert .... && i == n

Außerdem lässt sich s wie folgt berechnen:

s = (Summe von i=0 bis n für x) + (Summe von i=o bis n für i)
Tut mir leid, hab keinen Matheeditor gefunden.

Grundsätzlich sollte dies schon die Schleifeninvariante sein, bzw. die Nachbedingung R.
Allerdings weiß ich nicht wie ich dies schreiben soll.

Vielleicht gibt es ja jemanden der sich mit sowas gut auskennt und mir helfen kann, freue mich über jede Hilfe.

LG,
Alex

 

[Hüte]

Die Schleife wird n-mal ausgeführt

In der Schleife wird x+x+0 + x+1 + x+2 ... usw. berechnet

Die Invariante wäre dann x + (Sum i=0 bis n-1 von x+i), sie gilt vor, nach und in der Schleife

 

[vaults]

Moin,

danke für die Antwort, ich versuch deine Antwort noch mathematisch nachzuvollziehen, dann melde ich mich nochmal

Danke an dieser Stelle auch an Gauß für die Summenformel!

Die Nachbedingung R ist auf jeden Fall:

assert s == (n+1)*x + (i*(i+1))/2  && i == n;

 

[Hüte]

Ja, wenn du die Summenformel zerrupfst erhälst du

(i*(i+1))/2

. x ist ja unabhängig von der Zählervariable und kann desshalb außerhalb der Summe geschrieben werden. Die Invariante beeinflusst das aber nicht, sie bleibt die Summenformel

 

[vaults]

Moin,

danke nochmal, hier sind die fertigen Anweisungen:

public static int unknown(int x, int n){
		assert n > 0;			// Vorbedingung P
		int i, s;
		i = 0;
		s = x;
		assert s == x + (i*x) + (i*(i+1))/2;  	// Schleifeninvariante Q
		while (i<n){
			i = i + 1;
			s = s + x + i;
			assert s == x + (i*x) + (i*(i+1))/2;			// Schleifeninvariante Q
		}
		assert s == x+(i*x) + (i*(i+1))/2  && i == n;        // Nachbedingung R
		System.out.println("I ist: "+i+" S ist: "+s);
		return s;
	}

Einzig bei der Vorbedingung bin ich mir nicht sicher, die kann in diesem Fall meiner Meinung auch weggelassen werden.

LG,
Alex

 

[Hüte]

Die Vorbedingung (wenn es eine gibt) gehört auch mit zur Invariante

 

[vaults]

Danke dir, denke das Thema ist damit erledigt.