一般的には、事前条件P、受け取るメッセージ列M、状態遷移（move）m、発行されるメッセージ（イベント）列Nを使って、on P receiving M causes m emits N が仕様記述文てことになります。が、状態遷移は、遷移後の状態が満たす条件＝事後条件を書けば指定で…

条件PやQを書くには副作用のない関数（のようなメソッド）が必要です。条件の評価のときに副作用があると、話がとんでもなくややこしくなります。また、条件評価で例外が生じたりするのも望ましくないので、副作用がなくエラーしない関数的メソッドが欲しい…

ソフトウェア技術のなかで僕が一番興味を持っているのは仕様技術です。正確に適切な仕様を記述すること、そしてその仕様をもとに検証ができること、それを望んでいるのですけど、まー、難しいですね、イロイロと。で、仕様に関して最近思っていることなどを…

コンパクト閉圏を定義する : まず、対称モノイド圏に双対オペレータを導入し、そうして得られた双対付き対称モノイド圏に、180度回転する“曲がった射”であるKelly単位を加えてコンパクト閉圏を定義する。これは、従来の定義に比べ冗長だが、計算や図解は容易…