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

PlusCal入門1: hello, world

2021年2月5日 TLC2 #TLA+ #TLC

概要

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

この記事では 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; *)
====

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

構文の境界: PlusCal の構文は algorithm [モジュール名] から end algorithm; までの間で、それより外は TLA+ の構文である。
モジュール名の統一: ファイル名の [モジュール名].tla と TLA+ 構文の MODULE [モジュール名] でモジュール名を同じにしなければならない。ただし PlusCal 構文の algorithm [アルゴリズム名] はモジュール名とは異なる名前にしても良い。
EXTENDS: PlusCal のコードから TLA+ の機能を使用するときは TLA+ 構文で EXTENDS を指定する。EXTENDS の機能的な意味は Java や Python の import と同じで識別子を解決する。この例では HelloWorld モジュール内で print という機能を使用するために TLC モジュールを EXTENDS している。標準で使用できるモジュールとその機能については StandardModules 参照。