プログラミング言語仕様

コンピュータプログラミングにおいて、プログラミング言語仕様（または標準、定義）は、ユーザーと実装者がその言語のプログラムの意味について合意できるようにプログラミング言語を定義する文書です。仕様は通常詳細かつ形式的であり、主に実装者によって使用され、ユーザーは不明な点がある場合に参照します。たとえば、 C++仕様は複雑であるため、ユーザーによって頻繁に引用されます。関連ドキュメントには、ユーザー向けのプログラミング言語リファレンスや、仕様がなぜそのように書かれているのかを説明するプログラミング言語の根拠などがありますが、これらは通常、仕様よりも非公式です。

すべての主要プログラミング言語に仕様があるわけではなく、仕様がなくても何十年も存在し、人気がある言語もあります。言語には1つ以上の実装があり、その動作が仕様に文書化されていなくても、事実上の標準として機能します。Perl（ Perl 5まで）は仕様のない言語の顕著な例ですが、PHPは20年間使用された後、2014年にようやく仕様が定められました。^[1]言語は実装されてから仕様が定められることもあれば、仕様が定められてから実装されることもあり、また、これらが一緒に開発されることもあり、これは今日の通常の慣行です。これは、実装と仕様が互いをチェックするためです。仕様を記述するには、実装の動作を正確に記述する必要があり、実装では、仕様が実現可能で、実用的で、一貫していることを確認します。実装の前に仕様を記述することは、実装が延期されると実装で予期しない困難が生じるため、 ALGOL 68（1968年）以降、ほとんど避けられています。ただし、言語は正式な仕様なしに実装され、人気を得ることもあります。実装は使用に不可欠ですが、仕様は望ましいものの必須ではありません (非公式には、「コードトーク」)。

ALGOL 68 は、実装前に完全な正式な定義が行われた最初の (そしておそらく最後の) 主要言語でした。

—  CHAコスター、^[2]

プログラミング言語の仕様には、次のようないくつかの形式があります。

• 言語の構文と意味の明示的な定義。構文は一般に形式文法を使用して指定されますが、意味の定義は自然言語(例: C 言語で採用されているアプローチ) または形式意味(例: Standard ML ^[3]およびScheme ^{[4]仕様) で記述される場合があります。注目すべき例としては C 言語が挙げられます。C 言語は正式な仕様がないまま人気を博し、代わりに}「プログラミング言語 C」 (1978 年)という書籍の一部として説明され、その後ずっと後になってANSI C (1989 年) として正式に標準化されました。
• 言語 (例: C++言語およびFortran ) のコンパイラ(「トランスレータ」と呼ばれることもあります)の動作の説明。言語の構文とセマンティクスは、この説明から推測する必要があります。この説明は、自然言語または形式言語で記述できます。
• モデルの実装。指定されている言語 (例: Prolog ) で記述されることもあります。言語の構文とセマンティクスは、モデルの実装の動作に明示的に反映されます。

プログラミング言語の構文は、許容される単語の定義、つまり、特定のコードが言語に対して有効かどうかを判断するための正式なパラメータとルールを表します。その点では、言語構文は通常、次の 3 つの構成要素の組み合わせで構成されます。

• 特定の文字セット（空でない有限の記号セット）
• 語彙素を記述する正規表現（アルファベット順のトークン化用）
• 正しいプログラムを形成するために語彙をどのように組み合わせるかを記述する文脈自由文法

構文仕様では、一般的に、適度な理解可能性を提供するために自然言語による記述が想定されています。ただし、上記で概説したコンポーネントの正式な表現は、言語とその概念の実装と承認に有利であるため、通常はセクションの一部となります。

大規模で複雑で実用的なプログラミング言語の厳密な意味論を定式化することは、経験豊富な専門家にとっても困難な作業であり、その結果得られる仕様は専門家以外には理解しにくいものとなる。以下はプログラミング言語の意味論を記述する方法の一部である。すべての言語はこれらの記述方法の少なくとも1つを使用し、いくつかの言語は複数の方法を組み合わせている^[5]。

• 自然言語: 人間の自然言語による説明。
• 形式意味論:数学による記述。
• 参照実装:コンピュータプログラムによる記述。
• テスト スイート: プログラムとその予想される動作の例による説明。この形式で始まる言語仕様はほとんどありませんが、一部の言語仕様の進化はテスト スイートのセマンティクスの影響を受けています (たとえば、過去にAdaの仕様はAda 適合性評価テスト スイートの動作に合わせて変更されました)。

最も広く使用されている言語は、その意味を自然言語で記述して定義されています。この記述は通常、言語のリファレンスマニュアルの形式をとります。これらのマニュアルは数百ページに及ぶこともあり、例えば、印刷版の『Java言語仕様第3版』は596ページあります。^[6]

プログラミング言語のセマンティクスを記述するための手段としての自然言語の不正確さは、仕様の解釈に問題を引き起こす可能性があります。たとえば、Java スレッドのセマンティクスは英語で指定されていましたが、その仕様は実装者に適切なガイダンスを提供していないことが後に判明しました。^[7]

形式意味論は数学に基づいています。そのため、自然言語で表現される意味論よりも正確で、曖昧さが少なくなります。ただし、形式定義の理解を助けるために、意味論の補足的な自然言語による説明が含まれることがよくあります。たとえば、Modula-2のISO標準には、反対のページに形式定義と自然言語定義の両方が含まれています。

セマンティクスが形式的に記述されているプログラミング言語は、多くの利点を得ることができます。例:

• 形式意味論により、プログラムの正しさを数学的に証明することが可能になります。
• 形式意味論は、型システムの設計と、それらの型システムの健全性の証明を容易にします。
• 形式意味論は、言語の実装に対して明確で統一された標準を確立することができます。

自動ツール サポートは、これらの利点の一部を実現するのに役立ちます。たとえば、自動化された定理証明器または定理チェッカーは、プログラム (または言語自体) に関する証明の正確さに対するプログラマー (または言語設計者) の信頼を高めることができます。これらのツールのパワーとスケーラビリティは大きく異なります。完全な形式検証は計算集約的で、数百行のプログラムを超えることはめったになく^{[引用が必要] 、プログラマーによる手動の支援がかなり必要になる場合があります。}モデル チェッカーなどのより軽量なツールは、必要なリソースが少なく、数万行のプログラムで使用されてきました。多くのコンパイラーは、コンパイルするすべてのプログラムに 静的型チェックを適用します。

リファレンス実装は、権威あるものとして指定されたプログラミング言語の単一の実装です。この実装の動作は、その言語で記述されたプログラムの適切な動作を定義するものと見なされます。このアプローチには、いくつかの魅力的な特性があります。まず、正確であり、人間による解釈を必要としません。プログラムの意味に関する論争は、リファレンス実装でプログラムを実行するだけで解決できます (実装がそのプログラムに対して決定論的に動作することを条件とします)。

一方、リファレンス実装を通じて言語セマンティクスを定義することには、いくつかの潜在的な欠点もあります。その主な欠点は、リファレンス実装の制限と言語の特性が混同されることです。たとえば、リファレンス実装にバグがある場合、そのバグは正式な動作とみなされる必要があります。もう 1 つの欠点は、この言語で記述されたプログラムがリファレンス実装の癖に依存し、異なる実装間での移植性が妨げられる可能性があることです。

それにもかかわらず、いくつかの言語ではリファレンス実装アプローチがうまく使用されています。たとえば、Perlインタープリタは、Perl プログラムの正式な動作を定義すると考えられています。Perl の場合、ソフトウェア配布のオープン ソース モデルにより、この言語の別の実装が作成されたことはなく、リファレンス実装を使用して言語のセマンティクスを定義することに伴う問題は議論の余地がありません。

テスト スイートの観点からプログラミング言語のセマンティクスを定義するには、その言語でいくつかのサンプル プログラムを作成し、それらのプログラムがどのように動作するかを記述する必要があります (正しい出力を書き留めるなど)。プログラムとその出力は、言語の「テスト スイート」と呼ばれます。正しい言語実装は、テスト スイート プログラムで正確に正しい出力を生成する必要があります。

セマンティック記述に対するこのアプローチの主な利点は、言語実装がテスト スイートに合格するかどうかを簡単に判断できることです。ユーザーは、テスト スイート内のすべてのプログラムを実行し、出力を目的の出力と比較するだけです。ただし、テスト スイート アプローチを単独で使用する場合、大きな欠点もあります。たとえば、ユーザーは、テスト スイートの一部ではない独自のプログラムを実行したいとします。実際、テストスイート内のプログラムしか実行できない言語実装はほとんど役に立ちません。ただし、テスト スイートだけでは、テスト スイートにないプログラムに対して言語実装がどのように動作するかを記述できません。その動作を決定するには、実装者側で何らかの推定を行う必要があり、実装者によって意見が異なる場合があります。さらに、非決定的であることが意図されている、または許可されている動作をテストするためにテスト スイートを使用することは困難です。

したがって、一般的には、テスト スイートは、自然言語記述やリファレンス実装などの他の言語仕様技術のいずれかと組み合わせてのみ使用されます。

• プログラミング言語リファレンス

公式またはドラフトの言語仕様の例をいくつか示します。

• 主に形式数学で書かれた仕様:
  • 標準 ML の定義、改訂版 –操作的セマンティクススタイルによる正式な定義。
  • Scheme R5RS –表示的意味論スタイルによる正式な定義
• 主に自然言語で書かれた仕様:
  • アルゴル60レポート
  • Ada 95 リファレンスマニュアル
  • Java言語仕様
  • C++ 標準草案
• テストスイートによる仕様:
  • Rubyの事実上のコミュニティ主導の仕様