Fakultät Algorithmus auf Korrektheit prüfen

Diese Seite verwendet Cookies. Durch die Nutzung unserer Seite erklären Sie sich damit einverstanden, dass wir Cookies setzen. Weitere Informationen

  • Fakultät Algorithmus auf Korrektheit prüfen

    Hallo,

    ich habe eine Frage und probiere schon den ganzen Tag herum, aber komme nicht wirklich weiter. Es geht um einen Algorithmus der die Fakultät näherungsweise aber effizient berechnet. Das ist auch eigentlich egal, denn ich soll nur beweisen, dass der Algorithmus korrekt ist.

    Eingabe: n, natürliche Zahlen mit 0

    Ausgabe: n!

    Pseudocode:

    Quellcode

    1. s = 0 {s element rat. Zahlen}
    2. WHILE n > 1 DO
    3. s = s + ln(n)
    4. n = n - 1
    5. END WHILE
    6. RETURN e^(s)


    Dass der Algorithmus terminiert, also dass die Schleife und das Programm in jedem Fall endet, habe ich bereits bewiesen. Jetzt fehlt mir noch die Wohldefiniertheit, am besten durch eine Schleifeninvariante, doch iwie finde ich keine. Prof. verlangt eine aussagenlogische Formel, kann mir da iwer helfen. Es muss ja gelten n! = e^(s) --> n! = e^(ln((n-1)!)). Bei beispielsweise n=4 durchläuft er ja 4-1 Schleifen und s= ln(4) + ln(3) + ln(2)