\( \def\ldef{\ \ :=\ } \) \( \def\rdef{\overset{\triangle}{=}} \) \( \def\globally{□} \)

PlusCal入門1: hello, world

Takami Torao TLC2 #TLA+ #TLC
  • このエントリーをはてなブックマークに追加

概要

このページでは最初の PlusCal の例として hello, world と表示するプログラムをレビューし、その基本的な記述構造について考える。PlusCal での仕様記述や TLC 実行のための環境設定は環境設定と検証の実行を参照。

  1. 概要
  2. hello, world の実行例
  3. 参考文献

hello, world の実行例

この記事では TLA+ と同様に Visual Studio Code (vscode) を使用して PlusCal の実行を行う。環境構築は vscode に TLA+ 拡張機能をインストールするだけである (環境設定と TLC の実行参照)。

まず最初に簡単な hello, world を実行してみよう。vscode で以下のような内容の HelloWorld.tla ファイルを作成する。

---- MODULE HelloWorld ----
EXTENDS TLC
(* --algorithm HelloWorld
begin
  Greeting:
    print "hello, world";
end algorithm; *)
====

最初に知っておくべき基本的な注意点:

  1. 構文の境界: PlusCal の構文は algorithm [モジュール名] から end algorithm; までの間で、それより外は TLA+ の構文である。

  2. モジュール名の統一: ファイル名の [モジュール名].tla と TLA+ 構文の MODULE [モジュール名] でモジュール名を同じにしなければならない。ただし PlusCal 構文の algorithm [アルゴリズム名] はモジュール名とは異なる名前にしても良い。

  3. EXTENDS: PlusCal のコードから TLA+ の機能を使用するときは TLA+ 構文で EXTENDS を指定する。EXTENDS の機能的な意味は Java や Python の import と同じで識別子を解決する。この例では HelloWorld モジュール内で print という機能を使用するために TLC モジュールを EXTENDS している。標準で使用できるモジュールとその機能については StandardModules 参照。

この記事ではトランスパイラによって生成される TLA+ 構文やモデル (*.cfg ファイル) については特に説明しないが、TLC の検証エラーは TLA+ 構文上の位置が示されるため読める程度には慣れておくことを薦めておく。

参考文献

  1. Leslie Lamport (2009) The PlusCal Algorithm Language
  2. Leslie Lamport (1997) The Operators of TLA+
F