IEV Softwarehouse GmbH

 


Mathematische Beweisführung

Eine Prozedure und seine Invariante, dazu ein Beispiel aus der reinen Mathematik

f(x) := sin(1/x)
Eine Funktion f ist definiert durch den Sinus von Eins durch X.
Diese Funktion ist an allen Stellen außer bei x=0 stetig und differenzierbar. Die Differenzierbarkeit bei allen Stellen außer bei x=0 ist einfach zu beweisen.
Die Funktion ist an allen Stellen außer bei x=0 definiert. Denn der Sinus einer reellen Zahl ist immer definiert zwischen -1 und 1. Nun ist f an jeder Stelle differenzierbar wenn gilt, dass ein bestimmter Grenzwert existiert. Oder präziser gesagt:
Sei f :]a,b[ → ℜ eine Funktion. So heißt an der Stelle
ε ∈ ]a,b[ differenzbier, wenn folgender Grenzwert existiert:
lim h→0 ( (f(ε+h) - f(ε) ) /h) = lim x→0 ( (f(x)-f(ε)) / (x-ε) )
Das trifft auf jede Stelle von x außer bei x=0 zu. Bei x=0 ist die Funktion ja nicht definiert. Aus der Differenzierbarkeit folgt die Stetigkeit, also ist die Funktion auch an allen definierten Stellen stetig.
Wir definieren nun die Stelle x, mit f(0):=y1. Dabei nehmen wir y1 als diejenige Zahl, die uns die Stetigkeit bringt. Das geht aber nicht. Denn nehmen wir einmal an, es gäbe eine Folge die von links kommend immer den Wert -1 hat und eine von rechts kommend, die immer den Wert +1 hat. Dann haben wir zwei Folgen, die sich auf x=0 annähren, aber unterschiedliche Werte haben. Also fehlt hier die Stetigkeit. Analog kann man das auch mit der Differenzierbarkeit beweisen. Das Integral ∫ sin(1/x) existiert nicht als Term, Derive (TM) bringt uns erf(x), eine Fehlerfunktion, (also called the Gauss error function).
Der Sinus von Eins durch X ist eine nichttriviale Funktion aus der Analysis und ist deshalb immer wieder als Übungsaufgabe im Mathematikstudium zu sehen.

Das präzise Vorgehen eines Beweises in der Mathematik wird auch in diversen Programmtechniken angewandt.
Neben der Programmierung komplexer Algorithmen ist auch im Nachgang eine Beweisführung für die Korrektheit der Programme notwendig. Der Beweis mit der Invariante in einer Funktion wird da oft benutzt. Viele Programme unterlaufen am Ende nur Tests, diese sind zwar notwendig aber nicht hinreichend. Denn beispielsweise können 1 Mio Tests nicht beweisen, dass im Fall 1.000.001 das auch noch so ist, wenn sich die Ausgangsparameter ändern. Ein westentlicher Bestandteil einer Programmierung ist neben der Spezifikation auch die Verifikation.






 



 

Impressum    Kontakt    Datenschutz

©Softwarehouse 2020