PlusCal: 制御構造

概要

このページではいくつかの例を使って PlusCal の基本的な制御構造を説明する。実行環境のセットアップは PlusCal を参照。

Table of Contents

1. 概要
2. 制御構文
   1. 条件分岐: if \(c_1\) then \(p_1\) elsif \(c_2\) then \(p_2\) else \(p_3\) end if
      1. TLA+ の IF-ELSE との違い
      2. TLA+ の CASE-OTHER との違い
   2. 繰り返し: while \(c\) do \(p\) end while
      1. 無限ループの挙動
   3. ジャンプ: goto \(L\)
3. 非決定性挙動
   1. 経路分岐: either \(p_1\) or \(p_2\) or ... end either
      1. パスワード入力例の either
   2. 経路分岐: with \(x \in S\) do \(p(x)\) end with

制御構文

PlusCal で制御を記述するための構文は if-else, while, goto の 3 つに加えて、TLA+ の IF-ELSE, CASE-OTHER を使用できる。これらはすべて一般的なプログラミング言語の機能として思い浮かべるものと同じである。

条件分岐: if \(c_1\) then \(p_1\) elsif \(c_2\) then \(p_2\) else \(p_3\) end if

PlusCal の if-else 構文は条件分岐を記述する。以下の Example 1 は if 構文で記述した FizzBuzz である。

---- MODULE FizzBuzz ----
EXTENDS Integers, Sequences, TLC
(* --algorithm FizzBuzz
variables
  number \in 1..20;
  answer = "";
begin
  FizzBuzz:
    if number % 3 = 0 /\ number % 5 = 0 then
      answer := "Fizz Buzz";
    elsif number % 3 = 0 then
      answer := "Fizz";
    elsif number % 5 = 0 then
      answer := "Buzz";
    else
      answer := ToString(number);
    end if;
  Finally:
    assert
      \/ /\ answer = "Fizz" /\ number % 3 = 0 /\ number % 5 /= 0
      \/ /\ answer = "Buzz" /\ number % 3 /= 0 /\ number % 5 = 0
      \/ /\ answer = "Fizz Buzz" /\ number % 3 = 0 /\ number % 5 = 0
      \/ /\ answer /= "Fizz" /\ answer /= "Buzz" /\ answer /= "Fizz Buzz"
         /\ number % 3 /= 0 /\ number % 5 /= 0;
    print answer;
end algorithm; *)
==== 

TLA+ や PlusCal は変数宣言で定義した初期状態の組み合わせに対して全数テストを試みる。つまりこの仕様に対して PlusCal は \(n \in \{1,\ldots,20\}\) の 20 通りの検証を実行している。

TLA+ の IF-ELSE との違い

PlusCal では TLA+ の IF-ELSE 構文を使うこともできるが、両者の大きな違いは PlusCal の if-else 構文が値を返さない文 (statement) であるのに対して、TLA+ の IF-ELSE 構文は評価結果を返すことのできる式 (expression) であるという点である。したがって C や Java の三項演算子 c? a: b のような記述が行いたいときは TLA+ の IF-ELSE 構文を使用したほうが便利である。

制御機能の違いとして TLA+ の IF-ELSE には elsif に相当する構文が存在しない点がある。TLA+ でも ELSE IF という記述は見かけるが、これはネストされた IF-ELSE 構文である。

TLA+ の CASE-OTHER との違い

TLA+ の CASE-OTHER 構文は、一般的なプログラミング言語の switch-case 構文と同様に多数の分岐があるケースを簡潔に可視性よく記述することができる。また IF-ELSE 構文と同様に評価結果を返すことのできる式であることから、例 Example 1 の if-else を以下のように書き換えることができる。

    answer := CASE number % 3 = 0 /\ number % 5 = 0 -> "Fizz Buzz"
      [] number % 3 = 0 -> "Fizz"
      [] number % 5 = 0 -> "Buzz"
      [] OTHER -> ToString(number);

繰り返し: while \(c\) do \(p\) end while

PlusCal の while 構文は繰り返しを記述する。以下の例 Example 2 は正しいパスワードを入力するまで最大 3 回の試行を繰り返す処理を行っている。

---- MODULE ReadPassword ----
EXTENDS Integers, TLC
(* --algorithm ReadWhile
variables
  max_retry = 3;
  correct_password = "success!";
  retry = 0;
  input = "";
begin
  ReadPassword:
    while input /= correct_password /\ retry < max_retry do
      either input := "success!";
      or     input := "failure?";
      end either;
      retry := retry + 1;
    end while;
  Finally:
    assert input = correct_password \/ retry = max_retry;
    print << retry, input >>
end algorithm; *)
==== 

for に相当する構文は PlusCal には存在せず、while とループカウンターを組み合わせて実装しなければならない。例中の either については後ほど説明する。

制約: while 構文の先頭にはラベルを付けなければならない。

無限ループの挙動

PlusCal はラベルで区別されるステップごとに状態変数を記録し、状態変数が過去に実行したときと完全に同一であればそれ以上の実行を省略することは既に述べた。ラベル付けが必須の while 構文では 1 回のループごとに状態変数を確認し、過去の実行と同一の状態変数であることを検出したときに無限ループとみなしてその経路の検証を停止する。

以下に示す例 Example 3 は停止条件がないため一見して無限に hello, world を出力し続けるように見えるが、1 回目のループとそれ以降のループで状態変数に変化がないことから、結果的に InfiniteGreeting ステップは 1 回しか実行されず、また次の Finally ステップは一度も実行されていないことが結果から分かる。

---- MODULE HelloWorld ----
EXTENDS TLC
(* --algorithm HelloWorld
variable
  greeting = "hello, world";
begin
  InfiniteGreeting:
    while TRUE do
      print greeting;
    end while;
  Finally:
    print "finish";
end algorithm; *)
==== 

非同期処理の設計ではメッセージループのように意図して無限ループ (停止条件がない処理) を使うこともあるが、では意図しない無限ループが発生していることを設計者はどうやって知れば良いのだろうか? PlusCal では --- MODULE ... ---- の前、または === の後、あるいはコメント部分に PlusCal options (-termination) と指定することでプログラムが停止しない経路を持つときにエラーとする TLA+ コードに変換することができる (ハイフンは省略可能)。

PlusCal options (-termination)
---- MODULE NonTermHelloWorld ----
EXTENDS TLC
(* --algorithm NonTermHelloWorld
variable
  greeting = "hello, world";
begin
  InfiniteGreeting:
    while TRUE do
      print greeting;
    end while;
  Finally:
    print "finish";
end algorithm; *)
==== 

SPECIFICATION Spec
PROPERTY Termination
\* Add statements after this line. 

もし vscode ではなく PlusCal コマンドを使って TLA+ に変換している場合は -termination オプションを使用しても非停止経路の検出をエラーとするようになる。

ジャンプ: goto \(L\)

TLA+ も PlusCal も 199x 年代のパラダイムで作られた言語で制御の記述に関しては非力と感じる部分が多い。そしてその非力さを補うために他の言語でしばしば禁忌とされている goto 命令が用意されている。goto 命令は Java の例外処理や C の longjmp() のように込み入った処理のからの大域脱出でしばしば有用である。

以下はデータをロックして読み込み、更新して書き込む、という手続きを失敗ケースも含めて記述し、どのようなケースであっても最後にロックを解除していることを確認している。

全て表示

---- MODULE Goto ----
EXTENDS TLC
(* --algorithm Goto
variables
  lock = FALSE;
  case \in {"ReadFailure", "DataCannotUpdate",
    "WriteFailure", "Success"}
begin
  BeginTransaction:
    lock := TRUE;
    \* read user data...
    if case = "ReadFailure" then
      print "failed to read user data.";
      goto EndTransaction;
    else
      \* update and validate user data...
      if case = "DataCannotUpdate" then
        print "data couldn't update.";
        goto EndTransaction;
      else
        \* write user data...
        if case = "WriteFailure" then
          print "failed to write user data.";
          goto EndTransaction;
        end if;
        Success:
          print "The data has been updated.";
      end if;
    end if;
  EndTransaction:
    lock := FALSE;
  Finally:
    assert ~lock;
end algorithm; *)
====

制約: goto の後にはラベルを配置しなければならない。

非決定性挙動

PlusCal では either または with を用いて非決定性 (nondeterminism) の挙動を記述することができる。これらの記述は制御構文と似ているが、制御構文がある状態に対して必ず 1 つの経路が決まるのに対して、非決定性挙動はシステムの状態によらず任意の経路を取りうるという点で異なる。非決定性挙動の代表的な例はユーザ入力やサーバ応答のようなシステムの外部で決定する事象である。

状態変数の定義域が組み合わせでテストされていたのと同様に、処理中に either や with と遭遇すると PlusCal は自動でその組み合わせ数の検証経路を増加させる。

経路分岐: either \(p_1\) or \(p_2\) or ... end either

PlusCal の either はシステムが取りうる非決定性挙動の分岐を記述する。Example 6 に示す自動販売機の例では、コインを入れた利用者がタバコかスナックかまたは返却を選択する動作を either を使って表現している。

---- MODULE VendingMachine ----
EXTENDS Integers, TLC
(* --algorithm VendingMachine
variables
  revenue = 0;
  deposite = 0;
  dispensing_slot = "";
begin
  PutCoin:
    deposite := 1;
  ChooseProduct:
    either
      Ciggerette:
        dispensing_slot := "Cigerette";
        revenue := revenue + deposite;
        deposite := 0;
    or
      Snack:
        dispensing_slot := "Mixed Nuts";
        revenue := revenue + deposite;
        deposite := 0;
    or
      ToReturnCoin:
        dispensing_slot := "Coin";
        deposite := 0;
    end either;
  Finally:
    assert deposite = 0;
    assert (dispensing_slot = "Coin" /\ revenue = 0) \/ revenue = 1;
    print dispensing_slot;
end algorithm; *)
====

ここで Example 6 に示す実行結果に注目すると、最初の PutCoin ステップは 1 回しか実行されていないにも拘らず either を内包する ChooseProduct ステップは 3 回実行されていることが分かる。これは PlusCal が非決定性挙動を認識して自動的に 1) タバコを購入するケース、2) スナックを購入するケース、3) コインを返却するという 3 つの経路を検証するためである。この流れを図にすると Fig 7 のようになる。

この例で 3 経路を検証するだけであれば、状態変数 action \in {"Cigarette", "Snack", "ToReturnCoin"} を追加し ChooseProduct で if-else 分岐することでも目的を満たすことはできる。しかしこの場合、最初の PutCoin ステップから 3 個の挙動を検証することになるため非効率的である (実際に修正して結果を見よ)。TLA+ では状態変数の組み合わせ数は検証全体のパフォーマンスに大きく影響するため、非決定性の分岐で十分なケースでは非決定性の分岐を使用すべきである。

either-or の本体が await を含む場合、有効化されていない選択肢に制御が移ることはない。これはしばしばマルチプロセス環境で複数の await 待機から有効化された処理のみを実行する目的で使用される (golang の select に似ている)。

パスワード入力例の either

either は while などの構文と併用することでさらに複雑な経路の組み合わせを検証できる。先の while 構文で例示した Example 2 では「最大 3 回のパスワード入力」と「ユーザは正しいパスワードか間違ったパスワードを入力する」を組み合わせることで Fig 8 のように 10 個のアクションと 4 つの経路を検証している。

経路分岐: with \(x \in S\) do \(p(x)\) end with

with は either と同様に非決定性の挙動を記述する。either がケースごとに異なる処理を記述していたのに対して、with はどのケースでも同じ処理記述となる (処理が値に依存しない) 場合に便利である。

Example 9 の例はメンデルの法則に基づいて親の血液型から生まれる子供の血液型を求めている。この例では父親と母親の血液型の組み合わせに with を用いている。

---- MODULE BloodType ----
EXTENDS TLC
(* --algorithm BloodType
variables
  blood_type = EmptyBag;
define
  ABOGene == {"A", "B", "O"}
  BloodType == {{a, b}: a \in ABOGene, b \in ABOGene}
end define;
begin
  Inherit:
    with father \in BloodType, mother \in BloodType do
      with gene1 \in father, gene2 \in mother do
        blood_type := {gene1, gene2};
      end with;
    end with;
  Born:
    assert \E b \in BloodType: b = blood_type;
    print blood_type;
end algorithm; *)
====

TLA+ では Bags モジュールで多重集合 (multiset) 型を使用できるが、\in の右辺値は列挙可能なタプルや集合のみであるため集合 (set) 型を使用している (つまり AA, BB, OO 型は実際には {"A"} のように扱われている)。

経路数について考えてみよう。BloodType は A, B, O の 3 遺伝子の重複組合せとなるため \({}_3H_2 = 6\) 通りの組み合わせとなる。6 通りの血液型を ABO 遺伝子に平坦化すると 9 通りの並びとなり、父親遺伝子と母親遺伝子の組み合わせで \(9 \times 9 = 81\) 通りの経路が発生している。ただし、この ABO 遺伝子の合成によって作られる血液型のカーディナリティは依然として 6 である。

制約: with ステートメントの中はラベルを設置することができない。この制約から派生して、ラベルを必須とする while などのいくつかの機能は with 内では使用することができない。