■

SEMANTICS WITH APPLICATIONS
A Formal Introduction

Chapter 3　Provably Correct Implementation

プログラム意味論の形式的な特質は、
プログラムを実行するにあたって役に立つ。
特に、実行の正しさについて議論するのに有用。
そのことを知らしめるために、While言語を抽象マシンのアセンブラコードに変換する方法を示すとともに、
それが正しいことを証明する。
まず最初に、抽象マシンの命令の意味を操作的意味論によって

id:Writerがファックファック言っているので、言葉が伝染してしまいそうになる。これはいけない。上品な言葉を使わねば。
Writerに『C++のからくり』を貸して、『Effective C++ 原著第3版』を借りたのだけれど、うーん、『Effective C++』は難しいな。Writerが何故こんな本を買ったのかわからない。自分が薦めたのかなあ。いやそんなバカな…