はじめに go言語には、「スレッドの生成・起動」、「スレッド間の通信」といった、いわゆる「並列処理」を意識した言語要素があります。 このような言語要素を使って書く並行処理は、多くの場合振る舞いが複雑で正しいことを保証するのが難しくなります。 本記事では、そのような複雑な振る舞いになりがちなgoで書かれた「並行処理」の振る舞い設計をCSP(Communicating Sequential Process)という形式言語を使った記述と対応させます。そうする事で、並行処理を含むgo言語のコードの振る舞い検証をするための第一歩、「記述」についての説明を試みます。 尚、本記事で「遷移図」として利用した図は、PAT(Process Analysis Toolkit)というCSPベースのモデル検査のシミュレーション機能を使って表示した絵をキャプチャしたものを使いました。 CSPモデルとして解釈できるgo

