>>203
識別子の字面に引きずられるようなら、その時点で形式手法を使う意味は半減するよ。
形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して
あくまで記号操作の対象として扱う。

識別子の字面が大事になるのは、形式手法を知らない人に説明する時。
「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。
非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。