Vollständige Induktion bei iterativen Algorithmen?

Hallo,

ich habe bisher ein paar Beweise zur partiellen Korrektheit gesehen, die auf vollständiger Induktion basierten. Allerdings waren dies stets rekursive Algorithmen. Kann man den Ansatz auch bei iterativen Algorithmen verwenden?

Ich versuche mich gerade am Beweis einer simplen, linearen Suche.
Ich habe dazu ein PDF angefangen: http://tinyurl.com/cs9zdch

Wichtig zur algorithmischen Notation: Eine Zuweisung an x bedeutet Ausstieg aus dem Algorithmus. Also im Prinzip ein return.

Nach dem Algorithmus stehen in geschweiften Klammern die Nachbedingungen. Ich möchte -1 erhalten, wenn das gesuchte Element nicht in der Sequenz enthalten ist und den kleinsten Index zum Element, wenn das Element enthalten ist.

Darunter notiere ich den Induktionsanfang, probehalber für 0-elementige UND 1-elementige Sequenzen, was ja eigentlich nicht nötig wäre. Meine Argumentation erscheint mir dort recht wasserfest.
Danach nehme ich an, die partielle Korrektheit sei für eine (n-1)-elementige Sequenz bereits bewiesen.

Mein Problem ist nun, dass ich nicht weiß, wie ich den Induktionsschritt aufhängen soll. Meine hauptsächliche Frage ist, ob ich o.B.d.A. annehmen kann, dass das neue Element am Ende hinzugefügt wird.

Dies sollte m.E. so sein, denn wird aus der Sequenz M := { m1, m2, m3 } im Induktionsschritt M := { m1, a, m2, m3 } so könnte ich doch m3 und a die Rollen tauschen lassen, da in der Induktionsanahme ja mit abstrakten Bezeichnern, also mit beliebigen Sequenzelementen gearbeitet wurde, oder?

Danke

Da das Forum tollerweise meine tinyurl-URL zensiert hat, warum auch immer, hier nochmal ohne tinyurl:

http://46.163.65.134/beweis.pdf

knivil

Meine hauptsächliche Frage ist, ob ich o.B.d.A. annehmen kann, dass das neue Element am Ende hinzugefügt wird.

Das spielt keine Rolle.

Super, danke der Rest ist m.E. recht einfach.

Nach näherer Überlegung stoße ich auf ein weiteres Problem beim Schritt von (n-1) auf n:

Wenn man nun M := < m_0,...,m_n > betrachtet und als Induktionsannahme davon ausgeht, dass die Nachbedingungen für M' := <m_0,...m_(n-1)> bewiesen sind, so geht man ja davon aus, dass der Algorithmus bereits beendet wurde.

Denn die erfüllten Nachbedingungen für M' lauten dann:
Algorithmus terminiert mit -1 wenn k nicht in M'
Algorithmus terminiert mit kleinstem Index j für den gilt M[j] = k, wenn k in M'.

Also behaupte ich ja mit der Induktionsvoraussetzung, dass der Algorithmus bereits terminiert ist.

So wie ich das momentan sehe, ist dies ein generelles Problem, auf das man stößt, wenn man induktiv iterative Algorithmen analysiert. Wie umgeht man das formal geschickt?