\def\ldef{≜}

\def\globally{□}

\def\eventually{◇}

\def\openleftarrowplus{\overset{+}{⇾}}

\def\equalv{⫤}

PlusCal: データ構造と演算子

2021年3月8日 TLC2 #PlusCal #TLA+

概要

概要
データ構造
演算子
参考文献

データ構造

ブール値

数値

文字列

文字列は \o (または \circ) で連結することができる。文字列への変換は ToString() を使用する。

タプル: << $e_1$ , $e_2$ , $e_3$ >>

TLA+ のタプル (tuple) も一般的なプログラミング言語でのタプルと同じ。順序付けられた固定個数の値を持つことのできるデータ構造で、それぞれの値の位置に対して値の型と値の意味が決まっている。TLA+ では << >> で囲んで表現する。

構造体

集合: $e_1$ .. $e_n$ または { $e_1$ , $e_2$ , $e_3$ }

集合は要素の重複を許可しない複合データ型である。variables や with で使用することで状態変数による挙動の検証ケースを増やす。

TLA+ や PlusCal での集合リテラルは 1..10 や {"A", "B", "C"} のように記述する。

多重集合型

関数

TLA+ / PlusCal で関数 (function) と呼ばれるものは他のプログラミング言語でマップ (写像) や連想配列と呼ばれている構造である。

演算子	呼び名	表記例	数式表記	意味
`f[e]`	関数の適用	`y := f[x]`	$y = f(x)$	関数 $f$ に $x$ を適用
`DOMAIN f`	関数の定義域	`x := DOMAIN f`	-	関数 $f$ の定義域
`[x \in S \|-> y]`	関数定義	`f = [x \in 0..9 \|-> x * x]`	$f:x \in \{1,\ldots,9\} \to x^2$	$x \in S$ に対して $f(x)=y$ となる関数
`[S -> T]`	関数の集合	`f = [x \in 0..9 \|-> x * x]`	$x \in S: f(x) \in T$	$x \in S$ に対して $f(x) \in T$ となる関数の集合

演算子

PlusCal の演算子 (operator) は define ～ end define の間で定義する、

TLA+ における関数 (function) とは写像のことを意味しており、一般的なプログラミング言語で関数やプロシジャと呼ばれるものは演算子やマクロと呼んで区別している。

関係演算子

演算子	呼び名	表記例	数式表記	意味
`=`	同じ値	`A = B`	$A = B$	$A$ と $B$ が等しいとき真。
`/=`	異なる値	`A /= B`	$A \ne B$	$A$ と $B$ が異なるとき真。`#` も同じ。
`<`	小なり	`A < B`	$A \lt B$	値 $A$ が値 $B$ より小さいとき真。
`>`	大なり	`A > B`	$A \gt B$	値 $A$ が値 $B$ より大きいとき真。
`<=`	以下	`A <= B`	$A \le B$	値 $A$ が値 $B$ と等しいか小さいとき真。`\leq`, `=<` も同じ。
`>=`	以上	`A >= B`	$A \ge B$	値 $A$ が値 $B$ と等しいか大きいとき真。`\geq` も同じ。
`\in`	包含	`x \in S`	$x \in S$	$S$ に要素 $x$ が含まれるとき真。
`\notin`	包含否定	`x \notin S`	$x \not\in S$	$S$ に要素 $x$ が含まれないとき真。

論理演算子

演算子	呼び名	表記例	数式表記	意味
`/\`	論理積	`P /\ Q`	$P \land Q$	$P$ と $Q$ がともに真のときのみ真。`\land` も同じ。
`\/`	論理和	`P \/ Q`	$P \lor Q$	$P$ と $Q$ のどちらかが真のとき真。`\lor` も同じ。
`~`	否定	`~P`	$\lnot P$	$P$ が偽のとき真、真のとき偽。`\lnot`, `\neg` も同じ。
`\A`	すべての	`\A x \in S: P(x)`	$\forall x \in S: P(x)$	集合 $S$ のすべての要素で $P(x)$ が真のとき真。
`\E`	存在する	`\E x \in S: P(x)`	$\exists x \in S: P(x)$	集合 $S$ に $P(x)$ が真となるような要素 $x$ が存在するとき真。
`=>`	論理包含	`P => Q`	$P \Rightarrow Q$	前提命題 $P$ のもと $Q$ が真であれば真。 $\lnot P \lor Q$ と等価。前提命題 $P$ が偽のとき真となる vacuous truth に注意。
`<=>`	同値関係	`P <=> Q`	$P \Leftrightarrow Q$	$P$ と $Q$ が同値であれば真。`\equiv` も同じ。

集合演算子

演算子	呼び名	表記例	数式表記	意味
`CHOOSE`	単一選択	`CHOOSE x \in S: P(x)`	$P \Leftrightarrow Q$	集合 $S$ の要素で $P(x)$ が真となるような $x$ を選択。一つ以上の要素が一致する場合は任意の一つが選択される (実装依存だが概ね最初に見つかった要素となる)。一致する要素が存在しない場合はエラー。

Summary of TLA+ 参照

参考文献

Leslie Lamport (1997) The Operators of TLA+