2.4.3 グローバル変数

「グローバル変数」って名前あんまりよくない気がする…
「モジュールの中で操作しようとしている変数の集合」って認識したら正しそう。

モジュールMのすべてのグローバル変数の集合は次の集合の直和である。

  • Mで宣言されたグローバル変数の集合
  • Mの手続きのひとつを呼び出すことから始まる、一連の手続き呼び出しによって読み書きできるように、他のモジュールで宣言されたすべてのグローバル変数の集合。「できる」とは、読み込み/書き込みが条件の両方の分岐の実行、whileループ本体の実行、およびwhileループの終端を想定していることを意味する。*1

モジュールMのグローバル変数を表示するには、次を実行する。

print glob M.

たとえば、次のような宣言をしたとしよう。 

module Y1 = {
  var y, z : int
  proc f() : unit = { y <- 0; }
  proc g() : unit = { }
}.

module Y2 = {
  var y : int
  proc f() : unit = { Y1.f(); }
}.

module Y3 = {
  var y : int
  proc f() : unit = { Y1.g(); }
}.



module type X = {
  proc f() : unit
}.

module Z(X: X) = {
  var y : int
  proc f() : unit = { Y1.f(); }
}.

すると、

Zの場合は、パラメータXが抽象型なので、Xからはグローバル変数が何も得られない。

訳注: ifやwhileについては何も書かれていないが、例として新たに次のY4を定義すると、Y4のグローバル変数はY1.z, Y4.y, Y1.yからなる。

module Y4 = {
  var y : int
  var x : bool 
  proc f() : unit = {
    if (true) { Y1.f(); } else { Y3.f(); }
  }
}.

同様に、次のY5を定義すると、Y5のグローバル変数はY1.yからなる。

module Y5 = {
  proc f() : unit = {
    while (true) {
      Y2.f();
    }
  }
}.

すべてのモジュールMについて、対応する型glob Mが存在し、glob M型の値はMのグローバル変数の値のタプルからなる。この型の値は等価性を比較する以外には使いみちはない。

*1:なんのこっちゃわからん…が、ifの分岐のそれぞれと、whileループの本体部分に含まれる手続き呼び出しの中でアクセスする変数もグローバル変数に含まれるよ、という意味なのだと思われる。「whileループの終端(the terminal of while loops)」というのは全く意味がわからなかった。