Schleifeninvariante < Sonstiges < Hochschule < Informatik < Vorhilfe
|
| Aufgabe | Betrachtet folgenden Algorithmus.
calculateSomethin(x,y)
Input: x [mm] $\in \IN \setminus{0}$, [/mm] y [mm] $\in \IN$
[/mm]
Output: ???
p := y
WHILE p >= x DO
p := p - x
ENDWHILE
RETURN p
a) Was berechnet der Algorithmus? (ohne Begründung)
b) Nennt eine Schleifeninvariante des Algorithmus, mit der man die Korrektheit des Algorithmus beweisen kann. Sagt genau, zu welchem Zeitpunkt die Invariante bei jedem Schleifendurchlauf gültig ist.
c) Beweist formal, dass die Schleifeninvariante tatsächlich gilt. Warum folgt aus der Korrektheit der Schleifeninvariante die Korrektheit des Algorithmus? |
Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt.
Nun die erste Frage ist einfach.
a) Der Algorithmus berechnet den ganzzahligen Rest der Division von y/x.
Bei b) allerdings hab ich erst mal keine Ahnung.
Ich würde r = y - x*c als Invariante angeben. Aber ich hab keine Ahnung wie man das dann zu beweisen hat.
An sich würde ich sagen, gilt die Schleifeninvariante immer "zwischen" der Zeile in der p ersetzt wird und WHILE endet. Ist das richtig so?
Naja, da c) ja aus b) folgt, könnt ihr euch denken das ich dort noch nicht wirklich drüber nachgedacht habe.
Nur das die Korrektheit gilt, weil wir mathematischen bewiesen haben dass zu jedem Zeitpunkt diese Schleife das korrekte Ergebnis liefert.
Liebe Grüße
André
|
|
| |
|
Hallo Highchiller,
> calculateSomethin(x,y)
> Input: x [mm]\in \IN \setminus{0}[/mm], y [mm]\in \IN[/mm]
> Output: ???
>
> p := y
> WHILE p >= x DO
> p := p - x
> ENDWHILE
> RETURN p
>
> a) Was berechnet der Algorithmus? (ohne Begründung)
>
> b) Nennt eine Schleifeninvariante des Algorithmus, mit der
> man die Korrektheit des Algorithmus beweisen kann. Sagt
> genau, zu welchem Zeitpunkt die Invariante bei jedem
> Schleifendurchlauf gültig ist.
>
> c) Beweist formal, dass die Schleifeninvariante
> tatsächlich gilt. Warum folgt aus der Korrektheit der
> Schleifeninvariante die Korrektheit des Algorithmus?
> Ich habe diese Frage in keinem Forum auf anderen
> Internetseiten gestellt.
>
> Nun die erste Frage ist einfach.
> a) Der Algorithmus berechnet den ganzzahligen Rest der
> Division von y/x.
![[ok]](/images/smileys/ok.gif "[ok]")
> Bei b) allerdings hab ich erst mal keine Ahnung.
> Ich würde r = y - x*c als Invariante angeben. Aber ich
> hab keine Ahnung wie man das dann zu beweisen hat.
Gute Idee. Fragt sich nur, wie Du c definierst.
Es geht doch um die Restklasse. In der Modulrechnung würde man wie folgt formulieren: [mm] p\equiv y\mod{x}
[/mm]
- und zwar zu jedem Zeitpunkt. Nachzuweisen ist dies an der Zuweisung p:=p-x, überleg Dir mal, was genau da passiert. Mathematisch müsste man ja eigentlich sagen: [mm] p_{i+1}=p_{i}-x, [/mm] wobei der Index i natürlich einfach ein Schleifenzähler ist.
> An sich würde ich sagen, gilt die Schleifeninvariante
> immer "zwischen" der Zeile in der p ersetzt wird und WHILE
> endet. Ist das richtig so?
Wichtig ist, wo sie nicht gilt, und das ist in dem Moment, wo der Wert von p zur Berechnung von p-x benötigt wird, aber vor dem Moment, wo dieses Ergebnis wieder der Variablen p zugewiesen wird.
> Naja, da c) ja aus b) folgt, könnt ihr euch denken das ich
> dort noch nicht wirklich drüber nachgedacht habe.
> Nur das die Korrektheit gilt, weil wir mathematischen
> bewiesen haben dass zu jedem Zeitpunkt diese Schleife das
> korrekte Ergebnis liefert.
Grüße
reverend
|
|
|
| |
|
> Gute Idee. Fragt sich nur, wie Du c definierst.
> Es geht doch um die Restklasse. In der Modulrechnung
> würde man wie folgt formulieren: [mm]p\equiv y\mod{x}[/mm]
> - und
> zwar zu jedem Zeitpunkt. Nachzuweisen ist dies an der
> Zuweisung p:=p-x, überleg Dir mal, was genau da passiert.
> Mathematisch müsste man ja eigentlich sagen:
> [mm]p_{i+1}=p_{i}-x,[/mm] wobei der Index i natürlich einfach ein
> Schleifenzähler ist.
Ja zuerst hab ich auch überlegt wie ich c definiert bekäme. Allerdings wäre es verständlicher es so aufzuschreiben:
[mm]r = y - x \cdot i[/mm] Wobei i für die Anzahl der Iterationen steht. Richtig?
Mein größtes Problem besteht darin, es richtig auszuformulieren und aufzuschreiben.
Was meinst du damit, ich soll mir genau überlagen was wo passiert? Besonders komplex ist der Code ja nun nicht.
P wird der Wert von Y zugewiesen (obwohl dies eigentlich gar nicht nötig wäre, wenn es um einen möglichst kompakten Code geht)
Anschließend wird diesem Wert so oft X abgezogen, bis das neue P unter 0 sinken würde.
P wird dann ausgegeben.
Was hab ich jetzt von der Erkenntnis?
> Wichtig ist, wo sie nicht gilt, und das ist in dem Moment,
> wo der Wert von p zur Berechnung von p-x benötigt wird,
> aber vor dem Moment, wo dieses Ergebnis wieder der
> Variablen p zugewiesen wird.
Heißt das quasi, dass die Schleifeninvariante auf dem "ist-gleich" gilt?
|
|
|
| |
|
| Status: |
(Antwort) fertig  | | Datum: | 22:45 So 14.11.2010 | | Autor: | felixf |
Moin!
> > Gute Idee. Fragt sich nur, wie Du c definierst.
> > Es geht doch um die Restklasse. In der Modulrechnung
> > würde man wie folgt formulieren: [mm]p\equiv y\mod{x}[/mm]
Genau.
> > -
> und
> > zwar zu jedem Zeitpunkt. Nachzuweisen ist dies an der
> > Zuweisung p:=p-x, überleg Dir mal, was genau da passiert.
> > Mathematisch müsste man ja eigentlich sagen:
> > [mm]p_{i+1}=p_{i}-x,[/mm] wobei der Index i natürlich einfach ein
> > Schleifenzähler ist.
>
> Ja zuerst hab ich auch überlegt wie ich c definiert
> bekäme. Allerdings wäre es verständlicher es so
> aufzuschreiben:
Es ist nicht verstaendlicher. Schliesslich kommt $i$ im Programm nicht vor. Es ist also keine Gleichung in den Variablen des Programms und somit keine Schleifeninvariante. Es sei denn du modifizierst das Programm.
> [mm]r = y - x \cdot i[/mm] Wobei i für die Anzahl der Iterationen
> steht. Richtig?
Dann muesstest du eine Variable $i$ ins Programm einfuehren.
> Mein größtes Problem besteht darin, es richtig
> auszuformulieren und aufzuschreiben.
>
> Was meinst du damit, ich soll mir genau überlagen was wo
> passiert? Besonders komplex ist der Code ja nun nicht.
> P wird der Wert von Y zugewiesen (obwohl dies eigentlich
> gar nicht nötig wäre, wenn es um einen möglichst
> kompakten Code geht)
Natuerlich ist das noetig. Du kannst ja nicht $p$ einfach nicht initialisieren.
> Anschließend wird diesem Wert so oft X abgezogen, bis das
> neue P unter 0 sinken würde.
> P wird dann ausgegeben.
> Was hab ich jetzt von der Erkenntnis?
$p$ ist der kleinste nicht-negative Wert mit $p [mm] \equiv [/mm] y [mm] \pmod{x}$.
[/mm]
> > Wichtig ist, wo sie nicht gilt, und das ist in dem Moment,
> > wo der Wert von p zur Berechnung von p-x benötigt wird,
> > aber vor dem Moment, wo dieses Ergebnis wieder der
> > Variablen p zugewiesen wird.
>
> Heißt das quasi, dass die Schleifeninvariante auf dem
> "ist-gleich" gilt?
Die Schleifeninvariante $p [mm] \equiv [/mm] y [mm] \pmod{x}$ [/mm] gilt nach dem ersten $p := y$. Sie gilt auch waehrend $p := p - x$.
Dein Ausdruck $p = y - i [mm] \cdot [/mm] x$ haengt jedoch sehr davon ab, wo du dich gerade in der Schleife befindest ($i$ ist ja waehrend eines Schleifendurchlaufs konstant, $p$ aendert sich aber).
LG Felix
|
|
|
| |
|
> Dein Ausdruck [mm]p = y - i \cdot x[/mm] haengt jedoch sehr davon
> ab, wo du dich gerade in der Schleife befindest ([mm]i[/mm] ist ja
> waehrend eines Schleifendurchlaufs konstant, [mm]p[/mm] aendert sich
> aber).
>
> LG Felix
Also das hat mich nicht wirklich weiter gebracht.
Ich wollte darauf hinaus das wir uns gleich y vornehmen könnten in dem Programm, ohne extra eine Variable p zu initialisieren. Rein vom Programmiertechnischenanteil her.
Ja ist fix. Allerdings unbekannt. Ich meine vom logischen Sinne her könnte ich schnell auf i kommen. Aber mathematisch korrekt?
Wie könnte ich denn nun an:
r = y - x*i
einen Beweis durchführen? So ganz will mir das nicht einleuchten.
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 01:20 Mi 17.11.2010 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
