In den Gedächtnisprotokollen stand desöfteren, daß Korrektheit und Vollständigkeit (insbesondere von axiomatischen Inferenzregeln) mit denotationaler Semantik beweisbar sind. Man soll das angeblich sogar vorrechnen/zeigen! Kann mir mal jemand sagen, wo das steht? Habe ich da was überlesen?

Da es nicht mehr sonderlich lange bis zu meiner Prüfung ist, wäre ich auch über kurze Hinweise dankbar, falls ihr schonmal für LOS gelernt haben solltet oder derzeit lernt und noch grob was darüber wisst.

Nochmal die Frage: Wo steht in den Unterlagen, daß Korrektheit und Vollständigkeit mit der denotationalen Semantik beweisbar ist? Und wenn das nirgendwo steht, warum ist das so?

Danke für eure Hilfe!!

schau dir die Korrektheitsbeweise in Skript an! Es gibt aber so weit ich das hier grad überschau, nur die zu Zuweisung und while…leztere ist für die Prüfung sicherlich zu umfangreich. Ersteren kann man aber gut lernen (s. S. 49).

Meine Prüfung ist zu lange her, als dass ich das beantworten könnte, aber steht nicht in einem der Prüfungsprotokolle was als Antwort darüber?

die Korrektheit beweisst du, indem du zeigst das alle Regeln korrekt sind (und die Axiome auch), das zeigst du mit hilfe der dent. Semantik, wie im Falle der Zuweisung (bzw. while, siehe Beitrag oben). Die Vollständigkeit ist nicht so leicht zu beweisen, sie gilt auch nur bei der simplen Im. Sprache (d.h. ohne Felder etc). Das steht aber nicht im Skript…

falls du oder jemands anderes noch Fragen hat, könnten wir das über ICQ besprechen, da ich morgen Prüfung habe, würde mir die wiederholung sehr gut tun….