prüfen ob eine Überführungsfunktion richtig ist

Question

Kann ich mit XWizard überprüfen, ob meine Überführungsfunktion richtig ist?
 

Gibt es eine andere Möglichkeit diese auf vollständige Korrektheit zu prüfen?
​Durch ein Testwort wird es ja noch nicht allgemein gezeigt...

Answer 1

Ich bin nicht sicher, ob ich ganz richtig verstehe, was Sie wissen möchten.

Sie haben recht, ein Testwort zeigt nur für den einen Fall, dass die Überführungsfunktion in diesem Fall korrekt ist; es kann keine Aussage über ihre Korrektheit im Allgemeinen abgeleitet werden (außer, wenn sie nicht korrekt ist - dann reicht u.U. ein einziger Testfall).

Durch Testen kann man nie vollständig sicher sein, dass die Überführungsfunktion korrekt ist.

Leider gibt es allerdings für alle Automatentypen ab det. Kellerautomaten kein automatisches Beweisverfahren, um zu zeigen, dass die Semantik der Überführungsfunktion korrekt ist (die Semantik ist "das, was das Programm tut"). Sie kennen das ja vom Programmieren in Java etc. Wenn man sicher sein will, dass ein Programm korrekt ist, muss man sich schon hinsetzen und das in jedem Einzelfall von Hand beweisen.

(Es gibt Model-Checking-Verfahren, die einen halbautomatischen Mittelweg darstellen, aber damit haben wir uns nicht beschäftigt.)

Kurz gesagt, können Sie also leider nicht mit dem XWizard überprüfen, ob eine Überführungsfunktion korrekt ist. Und auch sonst gibt es kein automatisches Werkzeug, das das kann. Für die Klausur müssen Sie trotzdem in der Lage sein, korrekte Überführungsfunktionen anzugeben - und diese Korrektheit eventuell beispielhaft an einem Testwort zu demonstrieren.

(Beweisen, dass eine Überführungsfunktion korrekt ist, müssen Sie dagegen normalerweise nicht.)