アンダースタンディング コンピュテーション ―単純な機械から不可能なプログラムまで

2.2

 構文

19

について検証するための形式的手法というのは存在しません。仕様書を徹底的に読んで、さまざまな

ことを検討し、あらゆる結果を想定したと期待するしかありません。

Ruby 1.8.7

には文書としての仕様書が存在しており、

ISO

標準として受理されています

（

ISO/IEC 30170

）

†

。

mruby

プロジェクト（

https://github.com/mruby/mruby

）は軽量で組み

込みに使える

Ruby

実装を作る試みですが、

MRI

との互換性よりも

ISO

標準への準拠を明確

に目指しています。それでも、

MRI

は

Ruby

言語の正統な「実装による仕様」だと見なされて

います。

第3の方法は、形式意味論の数学的テクニックを利用して、プログラミング言語の意味を正確に記

述することです。ここでのゴールは、完全にあいまいさをなくすこと、そして、きちんとした解析、さ

らには自動解析に適した形式で仕様を書くことです。そうすることで、一貫性や矛盾、見落としを完

全にチェックできます。まずは構文がどのように扱われるのかを調べて、それから意味論的仕様に対

する形式的アプローチについて見ていきましょう。

2.2

　構文

通常、コンピュータプログラムは文字の羅列です。すべてのプログラミング言語には、どんな文字

列がその言語で有効なプログラムだと見なされるかを記述した規則の集まりがあります。これらの規

則は言語の構文（syntax）を規定します。

言語の構文規則によって、

y = x + 1

のような有効であろうプログラムと、

>/