formal-semantics - 「正式なセマンティクス」とは何ですか？

Question

私は非常にばかげた論文を読んでいて、Giottoが「正式なセマンティクス」をどのように定義しているかについて話し続けています。

Giottoには、モードスイッチ、タスク間通信、およびプログラム環境との通信の意味を指定する正式なセマンティクスがあります。

私は限界に達していますが、「正式なセマンティクス」が何を意味するのかを完全に理解することはできません。

Answer 1

Michael Madsenの答えを少し拡張するために、例として++演算子の動作があります。非公式には、平易な英語を使用してオペレーターを説明します。例えば：

xがタイプの変数である場合int、++xxが1つインクリメントされます。

（整数のオーバーフローはないと仮定していますが、++x何も返されません）

正式なセマンティクスでは（そして操作的セマンティクスを使用します）、やるべきことが少しあります。まず、型の概念を定義する必要があります。この場合、すべての変数が型であると想定しますint。この単純な言語では、プログラムの現在の状態は、変数から値へのマッピングであるストアによって記述できます。たとえば、プログラムのある時点で、はx42にy等しく、-5351に等しい場合があります。ストアは関数として使用できます。たとえば、ストアに値42sの変数がある場合、 。xs(x) = 42

プログラムの現在の状態には、実行する必要のあるプログラムの残りのステートメントも含まれます。これをとしてバンドルすることができます<C, s>。ここCで、は残りのプログラムであり、sはストアです。

したがって、状態がある場合<++x, {x -> 42, y -> -5351}>、これは非公式に、実行する残りのコマンドが唯一であり++x、変数xの値が42であり、変数のy値がである状態です-5351。

次に、プログラムのある状態から別の状態への遷移を定義できます。プログラムの次のステップに進むときに何が起こるかを説明します。したがって、の場合++、次のセマンティクスを定義できます。

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

やや非公式に、を実行する++xと、次のコマンドはskip効果がなく、ストア内の変数は変更されません。ただし、x元の値に1を加えた値になります。ストアの更新に使用した表記法を定義するなど、まだやるべきことがいくつかあります（この回答がさらに長くなるのを防ぐために行ったことはありません！）。したがって、一般的なルールの特定のインスタンスは次のようになります。

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

うまくいけば、それはあなたにアイデアを与えるでしょう。これは形式的セマンティクスの一例にすぎないことに注意してください。操作的セマンティクスに加えて、公理的セマンティクス（多くの場合ホーア論理を使用）と表示的セマンティクスがあり、おそらく私がよく知らないものがたくさんあります。

別の回答へのコメントで述べたように、正式なセマンティクスの利点は、プログラムの特定のプロパティを証明するためにそれらを使用できることです。たとえば、プログラムが終了することです。プログラムが悪い動作（非終了など）を示さないことを示すだけでなく、プログラムが特定の仕様に一致することを証明することにより、プログラムが必要に応じて動作することを証明することもできます。そうは言っても、仕様は通常ロジックで書き直されたプログラムであることがわかったので、プログラムを指定して検証するというアイデアをこれほど説得力のあるものとは思っていませんでした。したがって、仕様はバグがある可能性があります。

Answer 2

正式なセマンティクスは、明確な方法で物事の意味を表現する表記法を使用して、正式な方法でセマンティクスを記述します。

これは、基本的にすべてを平易な英語で説明する非公式のセマンティクスの反対です。これは読みやすく理解しやすいかもしれませんが、誤解を招く可能性があり、誰かが意図したとおりに段落を読んでいないため、バグが発生する可能性があります。

プログラミング言語は、正式なセマンティクスと非公式なセマンティクスの両方を持つことができます。非公式なセマンティクスは、正式なセマンティクスの「プレーンテキスト」の説明として機能し、正式なセマンティクスは、非公式な説明が何であるかわからない場合に調べる場所になります。本当に意味します。

Answer 3

言語の構文が形式文法（ BNFなど）で記述できるのと同じように、さまざまな種類の形式を使用して、その構文を数学的対象（つまり、構文の意味）にマッピングすることができます。

A Practical Introduction to Denotational Semanticsのこのページは、[denotational]セマンティクスが構文にどのように関連しているかについての優れた紹介です。この本の冒頭には、正式なセマンティクスに対する他の非外延的アプローチの簡単な歴史も示されています（ただし、Michaelが提供したウィキペディアのリンクはさらに詳細になり、おそらくより最新のものです）。

著者のサイトから：

セマンティクスのモデルは、BNFとその子孫が構文で持っているのと同じ程度には理解されていません。これは、セマンティクスが構文よりも単純に難しいように見えるためである可能性があります。最も成功しているシステムは、命令型プログラミング言語に見られるすべての機能を記述し、健全な数学的基礎を持っている表示的意味論です。（型システムと並列プログラミングの研究はまだ活発です。）多くの表示的定義は、インタープリターとして実行したり、「コンパイラー」に変換したりできますが、これはまだ効率的なコンパイラーのジェネレーターにつながっていません。これは、表示的意味論があまり人気がないもう1つの理由かもしれません。 BNFより。

Answer 4

ジョットのようなプログラミング言語の文脈で意味されるのは、形式的な意味論を持つ言語は、その個々の言語構造の数学的に厳密な解釈を持っているということです。

今日のほとんどのプログラミング言語は厳密に定義されていません。それらはかなり詳細な標準ドキュメントに準拠している可能性がありますが、最終的には、それらの標準ドキュメントに何らかの形で準拠しているコードを発行するのはコンパイラの責任です。

一方、正式に指定された言語は、通常、モデル検査や定理証明などを使用してプログラムコードについて推論する必要がある場合に使用されます。これらの手法に適した言語は、MLやHaskellなどの機能的な言語である傾向があります。これは、これらが数学関数とそれらの間の変換を使用して定義されているためです。つまり、数学の基礎です。

一方、CまたはC ++は技術的な説明によって非公式に定義されていますが、これらの言語の側面を形式化する学術論文が存在します（たとえば、Michael Norrish：C ++の正式なセマンティクス、https：//publications.csiro.au/rpr/pub ？pid = nicta：1203）、しかしそれはしばしば公式の基準に彼らの道を見つけません（おそらく実用性の欠如、特に維持の難しさのために）。