Invariante gesucht

Wissenschaft Informatik
#1

Hallo, suche zu folgendem Java-Programmfragment die Invariante:

IF (x!= 0) {
WHILE (n != 0) {
IF (n mod 2 == 1) p = p * x;
n = n div 2;
x = x * x;
}
}

Danke :smile:

#2

Jetzt mit ganzem Quelltext 
 sorry
Vielleicht sollte ich zur Lösung den vollstÀndigen Quelltext schreiben (man sollte ja schon wissen, was p ist:

Vorbedingung: {x == X AND n == N}
p = 1;
IF (x!= 0) {
WHILE (n != 0) {
IF (n mod 2 == 1) p = p * x;
n = n div 2;
x = x * x;
}
}
ELSE p = 0;
Nachbedingung: {p == POW(X, N)}

wobei POW(X, N) = X^N (also Potenzfunktion)

#3

Hallo,
betrachte mal folgenden Ablauf fĂŒr x=2 und n=5 (n wird binĂ€r dargestellt):

p=1 x=2 n=101
p=2 x=4 n=10
p=2 x=16 n=1
p=32 x=256 n=0

Das legt POW(X,N)=p*POW(x,n) nahe. Am Ende der Schleife gilt n=0 womit POW(x,n)=1 und damit p=POW(X,N) folgt.

Gruss
Enno

#4

Nachtrag
Hallo,
die Behauptung muß natĂŒrlich noch bewiesen werden, also

n>0 => POW(X,N)=p*POW(x,n)

Dazu kann man die Werte von p,x und n als Zahlenfolgen auffassen mit

(1) p(0)=1, x(0)=X und n(0)=N

(2) p(i+1)=p(i)*x(i) falls n(i) mod 2=1 p(i+1)=p(i) falls n(i) mod 2=0
x(i+1)=x(i)*x(i)
n(i+1)=n(i) / 2

Den Anker liefert klarerweise (1) und (2) den Induktionsschritt. Z.Z. ist hier

POW(X,N)=p(i)*POW(x(i),n(i)) & n(i+1)>0 => POW(X,N)=p(i+1)*POW(x(i+1),n(i+1))

bzw.

n(i+1)>0 => p(i)*POW(x(i),n(i))=p(i+1)*POW(x(i+1),n(i+1))

Gruss
Enno

#5

Verifikation der inneren If-Bedingung
Danke das hilft mir schonmal weiter, habe aber noch ein Problem mit der Verifikation:

Da in der While-Schleife ja noch eine If-Bedingung verschachtelt ist - wie verifiziere ich diese?

Nehme ich ich die entsprechend geÀnderte Invariante als Nachbedingung?

Und wenn ja, wieso folgt dann in diesem Fall aus

{POW(X,N)==p*POW(X,N) AND n!=0 AND n mod 2==1}
=> {POW(X,N)==p*x*POW(x*x, n div 2)}

bzw. aus

{POW(X,N)==p*POW(X,N) AND n!=0 AND n mod 2!=1}
=> {POW(X,N)==p*POW(x*x, n div 2)}

Oder habe ich hier einen Denkfehler bzw. ein VerstÀndnisproblem?

#6

Hallo,
z.Z. wÀre

  1. {POW(X,N)==p*POW(x,n) AND n!=0 AND n mod 2==1} => {POW(X,N)==p*x*POW(x*x, n div 2)}
    (also „kleines“ x und n bei dem p*POW(x,n)). Dazu reicht es unter den Annahmen bzw. der PrĂ€misse

p*POW(x,n)=p*x*POW(x*x, n div 2)

z.Z. Wg. n=2k+1 und damit n div 2=k gilt mit den Potenzgesetzen:

p*POW(x,n)=p*POW(x,2k+1)=p*x*POW(x,2k)=p*x*POW(x,k)*POW(x,k)=
p*x*POW(x*x,k)=p*x*POW(x*x,n div 2)

  1. {POW(X,N)==p*POW(x,n) AND n!=0 AND n mod 2!=1} => {POW(X,N)==p*POW(x*x, n div 2)}

Analog zeigt man fĂŒr n=2k, also n div 2=k

p*POW(x,n)=p*POW(x,2k)=p*POW(x,k)*POW(x,k)=p*POW(x*x,k)=p*POW(x*x,n div 2)

Gruss
Enno

#7

Danke :smile:
.