Was ist "formale Semantik"?

Question

Ich lese ein sehr albernes Papier und es spricht weiter darüber, wie Giotto eine "formale Semantik" definiert.

Giotto hat eine formale Semantik, die die Bedeutung von Modeswitches, der Intertask-Kommunikation und der Kommunikation mit der Programmumgebung spezifiziert.

Ich bin am Rande, aber kann nicht ganz begreifen, was es bedeutet "formale Semantik."

Answer 1

Formal semantics beschreiben Semantik in - nun, ein formaler Weg - mit Notation, die die Bedeutung der Dinge in einer eindeutigen Weise ausdrückt.

Es ist das Gegenteil von informelle Semantik, die im Wesentlichen nur alles in Plain Englisch beschreibt. Dies ist zwar leichter zu lesen und zu verstehen, aber es birgt das Potenzial für Fehlinterpretationen, was zu Fehlern führen könnte, weil jemand einen Absatz nicht so gelesen hat, wie Sie es vorgelesen haben.

Eine Programmiersprache kann sowohl formale als auch informelle Semantik haben - die informelle Semantik würde dann als eine "Klartext" -Erklärung der formalen Semantik dienen, und die formale Semantik wäre der richtige Ort für Sie, wenn Sie nicht sicher sind was die informelle Erklärung wirklich bedeutet.

Answer 2

Um auf Michael Madsen's Antwort etwas zu erweitern, könnte ein Beispiel das Verhalten des ++ Operators sein. Informell beschreiben wir den Operator, der einfaches Englisch verwendet. Zum Beispiel:

Wenn x ist eine Variable vom Typ int, ++x Ursachen x um eins erhöht werden.

(Ich gehe davon keine ganze Zahl überläuft, und dass ++x nicht alles zurück)

in einer formalen Semantik (und ich werde operationale Semantik verwenden), wir ein bisschen haben würden der Arbeit zu tun. Zuerst müssen wir einen Begriff von Typen definieren. In diesem Fall gehe ich davon aus, dass alle Variablen vom Typ int sind. In dieser einfachen Sprache kann der aktuelle Zustand des Programms durch einen Speicher beschrieben werden, der eine Zuordnung von Variablen zu Werten darstellt. Zum Beispiel kann an einem Punkt im Programm x gleich 42 sein, während y gleich -5351 ist. Der Speicher kann als eine Funktion verwendet werden - so zum Beispiel, wenn der Speicher s die Variable x mit dem Wert 42 hat, dann s(x) = 42.

Ebenfalls im aktuellen Zustand des Programms enthalten sind die restlichen Anweisungen des Programms, die wir ausführen müssen. Wir können dies als <C, s> bündeln, wobei C das verbleibende Programm ist und s das Geschäft ist.

Also, wenn wir den Zustand <++x, {x -> 42, y -> -5351}> haben, diese informell ein Zustand, in dem der einzige verbleibende Befehl ++x ist auszuführen, wird die Variable x hat den Wert 42, und die Variable y hat Wert -5351.

Wir können dann Übergänge von einem Zustand des Programms zu einem anderen definieren - wir beschreiben, was passiert, wenn wir den nächsten Schritt im Programm machen.Also, für ++, könnten wir die folgende Semantik definieren:

<++x, s> --> <skip, s{x -> (s(x) + 1)> 

Etwas informell, durch ++x Ausführung der nächste Befehl ist skip, die keine Wirkung hat, und die Variablen im Speicher sind unverändert, mit Ausnahme von x, welches jetzt den Wert hat, den es ursprünglich plus eins hatte. Es gibt noch etwas zu tun, wie zum Beispiel die Notation, die ich für die Aktualisierung des Ladens verwendet habe (was ich nicht getan habe, um diese Antwort noch länger zu machen!). Eine bestimmte Instanz der allgemeinen Regel könnte also lauten:

<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}> 

Hoffentlich gibt Ihnen das die Idee. Beachten Sie, dass dies nur ein Beispiel für formale Semantik ist - zusammen mit operationaler Semantik gibt es axiomatische Semantik (die oft Hoare-Logik verwendet) und denotationale Semantik und wahrscheinlich noch viel mehr, mit denen ich nicht vertraut bin.

Wie ich in einem Kommentar zu einer anderen Antwort erwähnte, ist ein Vorteil der formalen Semantik, dass Sie sie verwenden können, um bestimmte Eigenschaften Ihres Programms zu beweisen, zum Beispiel, dass es endet. Neben der Tatsache, dass Ihr Programm kein fehlerhaftes Verhalten zeigt (z. B. Nicht-Beendigung), können Sie auch beweisen, dass sich Ihr Programm wie erforderlich verhält, indem Sie beweisen, dass Ihr Programm einer bestimmten Spezifikation entspricht. Abgesehen davon habe ich die Idee, ein Programm zu spezifizieren und zu verifizieren, nie so überzeugend gefunden, da ich festgestellt habe, dass die Spezifikation in der Regel nur das in Logik umgeschriebene Programm ist und die Spezifikation daher genauso fehlerhaft ist.

Answer 3

Genau wie die Syntax einer Sprache durch eine formale Grammatik beschrieben werden kann (z.B. BNF), ist es möglich, verschiedene Arten von Formalismen zu verwenden, um diese Syntax mathematischen Objekten zuzuordnen (d. H. Die Bedeutung der Syntax).

This page von A Practical Introduction to Denotational Semantics ist eine nette Einführung in die Syntax von [denotational] Semantik. Der Anfang des Buches gibt auch eine kurze Geschichte von anderen, nicht-denotationalen Ansätzen zur formalen Semantik (obwohl der wikipedia-Link Michael gibt, geht noch detaillierter und ist wahrscheinlich aktueller).

Von the author's site:

Modelle für Semantik haben nicht gefangen-on in gleichem Maße, dass BNF und seine Nachkommen in der Syntax haben. Dies könnte daran liegen, dass die Semantik einfach einfacher zu sein scheint als die Syntax. Das erfolgreichste System ist Denotation Semantik, die beschreibt alle Funktionen in imperativ Programmiersprachen gefunden und hat einen Sound mathematische Basis. (Es gibt noch aktive Forschung in Systemen des Typs und parallele Programmierung.) Viele denotational Definitionen können als Dolmetscher ausgeführt sein oder in „Compiler“ übersetzt, aber das hat noch nicht zu Generatoren effizienter Compiler geführt, die eine andere sein kann Grund dass Denotational Semantik ist weniger populär als BNF.

Answer 4

Was im Zusammenhang mit einer Programmiersprache wie Giotto gemeint ist, ist, dass eine Sprache mit formaler Semantik, eine mathematisch strenge Interpretation der einzelnen Sprachkonstrukte hat.

Die meisten Programmiersprachen sind heute nicht streng definiert. Sie können sich an Standarddokumente halten, die ziemlich detailliert sind, aber es ist letztendlich die Verantwortung des Compilers, Code zu senden, der diese Standarddokumente irgendwie hält. Eine formal spezifizierte Sprache wird andererseits normalerweise verwendet, wenn es notwendig ist, über Programmcode nachzudenken, indem z. B. Modellprüfung oder Theoremprüfung verwendet wird. Sprachen, die sich für diese Techniken eignen, sind eher funktionale, wie ML oder Haskell, da diese durch mathematische Funktionen und Transformationen zwischen ihnen definiert sind; das heißt, die Grundlagen der Mathematik.

C oder C++ dagegen sind informell durch technische Beschreibungen definiert, obwohl es wissenschaftliche Arbeiten gibt, die Aspekte dieser Sprachen formalisieren (zB Michael Norrish: Eine formale Semantik für C++, https://publications.csiro.au/rpr/pub?pid=nicta:1203), die aber oft nicht gefunden werden ihren Weg in die offiziellen Normen (möglicherweise wegen mangelnder Praktikabilität, insbesondere Schwierigkeit der Aufrechterhaltung).