プログラムプロトコルへの Form Machine の適用

NWG/RFC #80 で言及した Protocol Manager は、上記の Form Machine の性質であるいくつかの興味深い機能を必要とする。

プロトコル対話中の特定の状況では、接続 A での accept を得るか、接続 B での allocation を得るかのいずれでも許容される場合がある。つまり、順序が重要でないこともある。規則を適用するための定義された手順は、順序非依存性を可能にする。

ロガーは、通常メッセージに埋め込まれたソケット番号を我々に送信するかもしれない——そのソケット番号は、あるプログラムとの接続を確立するために使用できる連続したソケット集合の先頭となることを意図している。我々は、通常メッセージからソケット番号フィールドを抽出し、おそらく別のフォーマットに変換し、それに加算して追加のソケット名を得たいと考える。通常メッセージの結果として、我々は計算したソケット番号を含むいくつかの INIT システムコールを出力したいと考える。 Form Machine の値演算子と算術演算子はこれを可能にする。

プロトコルに適用できる Form Machine の第三の性質は、文脈依存情報を解決するための規則間束縛と規則内束縛である。一般に我々は規則が順序非依存であることを望むが、特定の場合には順序を課したいと考える。 NWG/RFC #66 のロガーを例にとると、ロガーから送られる close はその文脈に応じて二つの異なる意味をもちうる。 close がソケット番号を含む通常メッセージより前に送られる場合、それは呼び出し拒否を意味する。通常メッセージが close より先行する場合、呼び出しは受け入れられる。 close は文脈的な意味をもつため、Form Machine 言語に IF と THEN を導入することを避けるために、それを通常メッセージに束縛しなければならない。

ここでしばらく、システムコールを Form Machine 記法で表現できると仮定しよう。 (以下の記法は 例示のみ を目的としたものであり、Form Machine 言語の一部ではない。) 通常メッセージを close に束縛する方法は二つある。規則内束縛では、close の前に通常メッセージが先行することを要求する。

      Reg. Msg , Close ->

次に、遠隔側が各送信の後にエコーを必要とすると仮定しよう。通常メッセージを受信した後、close が送られる前にエコーを出力しなければならないので、規則間束縛を使用しなければならない。これはプログラミング変数によって実現できる。通常メッセージを受信したときに値が割り当てられ、close を受信したときにその値が検査される。

      Reg. Msg -> Echo , ([lambda]+1)

      Close, ([lambda]=1) ->

プログラミング変数による規則間束縛を例示するために、NWG/RFC #66 の接続プロトコルは、以下の形式を Protocol Manager に渡すことで表現できる。 (以下の記法は 例示のみ を目的としたものであり、Form Machine 言語の一部ではない)。

      1. ->INIT(parameters) , ([alpha]<-0)

INIT(RTS) を送信する。

      2.  INIT(parameters) -> ALLOCATE(parameters)

接続完了 (STR の受信) に応答して allocate を送信する。

      3.  Reg. Msg (parameters) -> ([alpha]<-1)

リンク番号を運ぶメッセージを受信したとき、内部インジケータを設定する。 (リンクの抽出は例示していない。)

      4.  CLOSE(parameters),([alpha]=1) ->
                             INIT(parameters),INIT(parameters)

通常メッセージに続いて close を受信した場合、二重接続を確立する前に通常メッセージが受信されたことを確認するために [2] が検査される。通常メッセージが先行せずに close を受信した場合 (呼び出し拒否)、形式は失敗する (満たされる規則がないため)。

このプロトコルは、四つの置換規則を含む単一の形式によって扱うことができる。我々はより複雑なプロトコル系列についても同様の表現を検討した。名前で保存されたそのようなプロトコル系列はユーザーにとっての資産であり、ユーザーは事前定義された系列を自動的に実行するよう要求できる。