ソフトウェア・シンポジウム 2020 (オンライン開催)

探索的仕様記述のための履歴ツールの提案と実装
小田 朋宏
株式会社 SRA
tomohiro@sra.co.jp

張 漢明
南山大学
chang@nanzan-u.ac.jp

中小路 久美代
公立はこだて未来大学
kumiyo@acm.org

山本 恭裕
公立はこだて未来大学
yxy@acm.org

荒木 啓二郎熊本高等専門学校
araki@kyudai.jp

要旨

ユーザーの振る舞いから利用シナリオを抽出し，かつ，
それら対象ドメインや利用シナリオに対してどのようなソフトウェア開発の過程を困難なものとしている一つ

ソフトウェアシステムが適合するか理解を深めていく必の要因として，複雑なものを対象にした試行錯誤が挙げ

要があることから，多くのソフトウェア開発では探索的られる．ソフトウェアシステムを作成する過程において，な試行によって理解を深めていくことが求められる．

複雑な対象ドメインやソフトウェアシステム自身への理機能仕様は開発対象の機能や特性を記述したものであ解を探索的に深め，得られた知見を整理し，ドキュメン

り，他の工程の多くで参照される．機能仕様の策定にもトとして記録することが求められる．ソフトウェア開発

探索的な試行が行われるが，試行には部分的な失敗を含における履歴の管理と整理は，ソフトウェア工学の古く

むことが多いことから，他の工程に波及するとコストがからの課題であり，多くのツールが実現されて広く利用

かかる．形式仕様はソフトウェアシステムを実装する以されている．本論文では，ソフトウェア開発における試前にその特性を分析することを可能にすることから，仕行錯誤の中でも，形式仕様記述における個人作業の中で様記述段階での探索的試行に適している．著者らは形式の探索的な作業に注目して，仕様記述の編集や表現式の仕様工程のうち探索的試行が多くおこなわれる初期段

評価実行のような細粒度の履歴の整理のための手法を提階を探索的仕様記述として，それを支援するための開発

案する．そして，実行可能な仕様記述言語 VDM-SL で

環境 ViennaTalk [1] を開発してきた．ViennaTalk は仕様の仕様記述における探索的試行を記録し，後に仕様記述

記述言語として VDM-SL [2] を採用し，その実行可能

者自身がその過程を整理し，記録するためのツールを提なサブセットによる仕様アニメーションを中心にして，案し，その実装を紹介する．

VDM-SL 仕様記述を実行可能なプロトタイプとして様々な利用シナリオへの適合性を評価し，探索的な試行を支援するための機能を提供している．

1. はじめに探索の結果として得られる知見は，最終的に記述された VDM-SL 仕様だけではない．探索の過程で試した多ソフトウェア開発を困難なものにしている要因として，

くの暫定的な仕様記述や，その上で検討した利用シナリ

複雑さがある．ソフトウェアシステム自体の複雑さに加オや，その利用シナリオでのシステムの動作を記録する

え，ソフトウェアシステムの対象ドメインの複雑さや，ことで，その仕様記述の機能項目がなぜそのように定義

ソフトウェアシステムを利用する人の振る舞いに関連しされているかを説明するドキュメンテーションとしてのた複雑さから，開発の開始時点では開発に必要な知識役割を果たすことができる．

を前もって獲得することは困難である．ソフトウェアシ

本論文では，探索的な試行の履歴を整理するためのモステムを作りながら，対象ドメインに存在する概念や，

デルと，その実装例として VDM-SL 用のウェブ IDE で

95

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)

フェーズ

ある VDMPad [1] に探索的試行の履歴を整理する機能を追加した VDMPad-EpiLog を紹介し，その利用例を示

仕様の編集

仕様の編集

す．第 2 節で探索的試行の履歴を整理するための構造と状態の設定それに対する操作を提示し，その実装として VDMPad-

操作の実行

EpiLog の機能とその利用例を第 3 節に示す．第 4 節で

状態の確認

シナリオ
状態の設定

は関連する既存のツールとして github および git を中心

仕様の編集に比較検討する．第 5 節に議論とまとめを示す．

状態の設定

2. VDM-SL 仕様記述の履歴モデル

操作の実行
状態の確認

操作の実行

フェーズ

状態の確認

仕様の編集

状態の設定
操作の実行

本節では，VDM-SL 仕様を記述する個人作業における操作の実行

探索的試行の履歴を整理するための構造を提案する．本状態の設定

研究では開発における探索的試行について，対象に関す

シナリオ
状態の設定

シナリオ
状態の設定

操作の実行

操作の実行

状態の確認

操作の実行
状態の確認

る部分的な知識に基づいて暫定的仮説的なモデルの記述
時系列に並んだ履歴を作成し分析を行うことを 1 単位の試行とした上で，1整理された履歴つの試行を通して深められた理解に基づいて次の施行を扱う，サイクルプロセスと捉える．仕様記述をおこなう
図 1. 履歴整理の例

中で，探索的に繰り返された試行を抽出することで，履歴を構造化し整理する．

ンをいくつか想定し，それぞれの利用シーンをユース

VDM-SL は，実行可能なサブセットを持つ，モデル規ケースとして，どのような操作をどのような順番でどの範型の形式仕様記述言語である．仕様記述者は対象を内ような判断を伴いながら実行するかを想定することが多部状態および内部状態に対する操作としてモデル化し，い．システムの動作を表現した記述として，ユニットテ

データ型，定数，関数，状態空間，操作の 5 種類の定義に

スト [4] がある．

よって記述する [2]．データ型を types 部で宣言し，定VDM-SL 仕様に対するユニットテストフレームワーク
は vdmUnit や viennaUnit [5] などが既に開発され利用さ数および関数をそれぞれ values 部および functions
部で定義することによって，そのシステムが扱う概念とれている．

その関係を記述する．VDM-SL では定数および関数はユニットテストでは，システムの構成部品に対して想参照透明である．state 部では，システムが持つ状態定される利用シナリオ毎に，テストケースを定義する．

空間を定義するために，静的に型付けられた変数のリス

各テストケースは，シナリオの前提となるシステム状態

ト，状態に対する不変条件，および初期状態を宣言する．

の設定，システムに対する一連の操作の実行，操作結果

システムが提供する操作を operations 部で定義する．

の確認を，テスト用の操作として記述したものである．

操作は状態に対する参照や変更を行うことができる．

VDM-SL 仕様のユニットテストは，記述対象に対する利用シナリオへの適合性の検査を自動化したものと見なす

形式仕様記述言語としての VDM-SL の大きな特徴として，そのサブセットをインタプリタで実行可能である

ことができる．

ことが挙げられる．VDMTools や Overture Tool [3] を始

本研究では，ユニットテストを参考にして，探索的試

めとする VDM-SL 開発環境の多くが，REPL (Read-Eval-

行のモデルを定義した．探索的試行の中では，仕様記述

Print Loop) インタプリタを提供し，仕様記述者は編集中の仕様記述に対してインタプリタを起動して，表現式をの編集，状態の編集，操作の評価実行が行われる．仕様
記述者は，それぞれの時点での暫定的な仕様記述に対し入力して評価実行することができる．仕様記述の探索的て，利用シナリオをいくつか想定して，利用シナリオを試行において，インタプリタ実行は編集中の仕様記述の状態編集と操作列として模擬的に実行し，実行結果が利特性を把握する上で，重要な役割を果たしている．

用シナリオが想定した通りかを確認する．履歴を，仕様

VDM-SL によるモデル化の前段階として，システムの機能仕様に対する原始要求として，システムの利用シー

記述のバージョンに対応するフェーズ，利用シナリオに

96

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)

対応するシナリオ，個々の状態編集や操作実行に対応す的な仕様記述に対する一連の履歴項目を，1 つのフェー

るランの 3 つの単位にまとめることとした．

ズとする．フェーズは，履歴の時系列から，仕様記述のフェーズは，記述対象に関する理解の変化を捉えるこ編集から，次の仕様記述の編集までの区間を切り出すことを主眼にした単位である．仕様記述は，仕様記述者がとで，容易に抽出することができる．

対象をモデル化したものであり，仕様記述者による対象

フェーズの中では，いくつかの利用シナリオに関するに対する理解を表現している．本節冒頭で述べた通り，適合性の確認が行われる．ここでの利用シナリオは，原

本研究では仕様記述における探索を，仕様記述者による始要求の中で明示的に示されたものもあるが，仕様記述

対象への理解を表現した暫定的仮説的な仕様記述とその者によるドメインへの理解から仮説的に想定しているも記述に対する一連の検証を 1 つの試行とする．フェーズのもある．したがって，シナリオの同定は必ずしも機械

は 1 つの仕様記述とそれに対する検証をおこなうための的にできるとは限らない．探索の履歴を整理する上で，一連の評価実行をまとめたものであり，1 単位の試行とシナリオは原始要求や仕様記述者の理解を反映する重見なすことができる．

要な単位であることから，探索の履歴を整理するためのシナリオは，仮説検証における検証の単位である．仕ツールを設計する上で重要なポイントになる．

様記述で定義されたシステムの動作が対象ドメインや原

ランはシナリオを構成する基本要素であり，シナリオ

始要求に対して妥当であるかどうかを確認するために，の内容はランの時系列として表現される．ランは多くのシステムの特定の動作を切り出したものをシナリオとす場合，開発環境が収集した時系列の履歴の各項目から抽る．1 つのフェーズの中で，複数のシナリオによる妥当

出することができる．

性の確認が行われる．シナリオには，原始要求に含まれ3. VDMPad-EpiLog

る利用シナリオや対象ドメインからくるものもあれば，仕様記述に定義された機能単位からくるものもある．
ランは，シナリオの妥当性を確認するために行う，仕本節では，探索的試行の履歴を整理するツールの実装

様記述者による操作の単位である．VDM-SL 仕様はシス

例として VDMPad-EpiLog を説明する．VDMPad-EpiLog

テムを状態空間と操作群により定義することから，VDM-

は， 探索的な仕様記述の特に初期段階の試行を想定しSL 仕様記述での探索では，状態の初期化や，操作の評価
実行を試行の基本単位として扱うことができる．具体的て設計されたウェブ IDE である VDMPad [1] に対するにどのような種類のランがあるかは，開発環境のユーザ

図 2 に VDMPad の画面例を示す．VDMPad は仕様ア

インタラクションの設計による．REPL (Read-Eval-Print

ニメーションを中心に設計されている．仕様アニメー

Loop) インタプリタの場合，インタプリタが提供するコションとは，仕様をインタプリタ等で評価実行すること

マンドのうち，アニメーション実行に影響を与えるもの

で，与えられた仕様を実装したシステムがどのように動をランとして扱うことができる．Overture Tool には，仕作するかをシミュレートする技術である．VDMPad は，様記述が定義する操作をボタンにした簡易 GUI による

VDM-SL で記述された仕様のソースと，仕様が定義する状態空間におけるシステムの現在の状態を保持し，それをプロトタイプとしてウェブページ上に表示する．仕

拡張として実装された．

アニメーション機能があるが，この場合は各ボタンの押下をランとして扱うことができる．
図 1 に，仕様の修正をともなう探索的試行の履歴につ様記述者はプロトタイプに対して，仕様記述，状態，評いて，時系列からフェーズ，シナリオ，ランの 3 つの粒度

価式を編集して与え，評価実行ボタンを押すことで評価の構造に整理した例を示す．左側には，探索の中で行わ結果を得るとともに，プロトタイプの状態を更新する．

れた仕様の編集，状態の設定，操作の実行，状態の確認が上から下の順に時系列で列挙されている．仕様記述に

VDMPad は，柔軟な探索のために，仕様 / 状態 / 評価式のいずれも常に編集可能であり，それらはいずれもプロおける探索的試行では，暫定的な仕様記述を作成し，そトタイプへの修正操作として扱われる．また，プロトタの仕様記述が利用シナリオにどのように適合するか，シイプの仕様を編集しても，プロトタイプを再起動するこ

ステムがどのように動作するかを確認する．いくつかのとなく，継続してプロトタイプに対する操作を行うこと

利用シナリオが試され，システムの動作が仕様記述者のができる．

意図と異なる場合には仕様記述を編集する．1 つの暫定

97

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)

フェーズ 1
仕様記述 1

フェーズ 2'

シナリオ 1-1
シナリオ 1-2
仕様記述編集エリア

フェーズ 2

合併

仕様記述 2

ソース整形ボタン

シナリオ 1-1
シナリオ 1-2
シナリオ 2-1

シナリオ 2-1

状態編集エリア

図 3. フェーズの合併

状態初期化ボタン
評価式編集エリア

評価値表示エリア

仕様記述 2

評価実行ボタンフェーズ 1

フェーズ 1'

仕様記述 1

仕様記述 1

シナリオ 1-1
シナリオ 1-2

シナリオ 1-2
移動

フェーズ 2
図 2. VDMPad の画面例

仕様記述 2
シナリオ 2-1

3.1. VDMPad-EpiLog の概要

フェーズ 2'
仕様記述 2
シナリオ 1-1
シナリオ 2-1

VDMPad-EpiLog は，VDMPad を拡張して，履歴を整理する機能を追加したものである．VDMPad では，プ

図 4. シナリオの移動

ロトタイプは受動的であり，仕様記述者が評価実行ボタ
ンおよび状態初期化ボタンを押すことで，プロトタイプ• 連続した実行：いずれの条件にも当てはまらないを駆動する．評価実行ボタンが押されると，VDMPad は場合には，最新シナリオの末尾にランとして追加

仕様記述のソース，現在の状態，評価式をサーバに送信する．

し，評価結果の値，評価後の状態，エラーの場合にはエこうして自動的に整理された履歴は，ユーザによる探ラーメッセージを返す．VDMPad-EpiLog はそれを捉え索的試行を実行の時系列に忠実に反映した履歴である．

て，エラーでない場合のみ，仕様記述のソース，評価前

しかし探索の結果得られた知見としてまとめる上では，の状態，評価式，評価結果の値，評価後の状態を保存し，いくつかの問題点が考えられる．

以下の手順で自動的にフェーズ，シナリオ，ランとして仕様記述を編集するごとにそれに対応するフェーズが整理する．

生成されるが，そうしたフェーズにはあまり重要ではな• 仕様の断絶：仕様記述が直前のものと異なる場合には，新しいフェーズを生成する．

いものも多い．仕様記述の修正のうち，知見として残す必要のない軽微な修正は，重要なフェーズと合併する，あるいは削除することで，重要なフェーズのみを残すこ• 状態の断絶：上の条件に当てはまらず，かつ，評価とができる．図 3 にフェーズの合併を示す．フェーズ 1

前の状態が直前の履歴での評価後の状態と異なるの仕様に軽微な問題があり，フェーズ 2 の仕様でそれが場合には，新しいシナリオを生成し，最新フェー

解決された場合，フェーズ 1 をフェーズ 2 に合併する

ズのシナリオリストに追加する．

ことで両方のシナリオを修正後であるフェーズ 2 の仕様

98

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)

シナリオ 1

シナリオ 1'

ラン 1
ラン 2
ラン 3
ラン 4

ラン 1
ラン 2

分割

仕様記述

シナリオ 2'

フェーズ

ラン 3
ラン 4

ラン
シナリオ

ラン

図 5. シナリオの分割の上でのシナリオとすることができる．ただし，フェー
ズ 1 にあった 2 つのシナリオは，試行時にはフェーズ 1の仕様で実行されたものであり，フェーズ 2 の仕様での実行結果とは異なる可能性がある．したがってフェーズ

図 6. VDMPad-EpiLog の画面例

1 から移動したシナリオに含まれるランの実行結果は無
変数名

効マークが付与される．無効とされたランは，移動先の値

フェーズの仕様で再実行することで，無効マークを取り除くことができる．また，図 4 に示すように，特定のシ

操作前の状態の状態状態

評価式

ナリオのみ次のフェーズに移動することもできる．

返り値り値値

探索的試行の中で，同一フェーズ内で連続して複数の操作後の状態の状態状態

シナリオを検討する場合，シナリオ開始時に特に状態を変更する必要がない場合がある．状態の変更を伴わずに変数名

シナリオでのランを開始すると，VDMPad-EpiLog はシ

値

ナリオの切れ目を検出できず，同一シナリオの継続として処理する．探索的試行の中で意図したシナリオに分割するために，シナリオの特定のラン以降を別のシナリオ

図 7. ランの表示例

として分割することができる．シナリオの分割操作を図5 に示す．

EpiLog 画面には，フェーズごとに仕様記述とシナリオが表示される．各フェーズでは上段に黒枠で囲まれた仕様記述の下に，背景色がついたシナリオが列挙される．

フェーズやシナリオ，ランには繰り返し同じものが現れたり，特に重要ではないため知見として残す必要のないものも多い．したがって，不要なフェーズやシナリオ

各シナリオには，左側に太い帯状の濃いグレーが 1 つなやランを削除する操作も提供される．

がりで表示され，その右側にランが上から下に並べて表示される．シナリオ中のランとランの間は，薄い横線で3.2. VDMPad-EpiLog の UI

区切られる．
各ランには，上段に実行前の状態，中段には評価実行

本節では VDMPad-EpiLog の UI を説明する．図 6 にする表現式とその返り値，下段には実行後の状態が表示

VDMPad-EpiLog の画面例を示す．VDMPad のメニューされる．図 7 にランの表示例を示す．水平に引かれた区

中の VDMPad-EpiLog ボタンを押すと，従来の VDMPad

切り線の上に変数名，下にその値が表示される．実行前の右側に構造化された履歴が表示される．ただし，ウェの状態については，当該ランの直前のランの実行後の状

ブブラウザの横幅が足りない場合には，従来の VDMPad

態からの差分が表形式で表示される．シナリオ中の多くの下部に表示される．構造化された履歴の表示部分を，のランでは，操作前の状態は直前のランの実行後の状態

本論文では EpiLog 画面と呼ぶことにする．

99

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)を引き継ぐため，差分がなく，表示は省略される．ただし，各シナリオの最初のランは，前のランがないため，実行前の状態がそのまま表示される．中段には，右方向を指差したシンボルの左側に表現式，右側にそれを評価した返り値が表示される．下段には，実行前の状態からの実行後の状態の差分が表形式で表示される．
フェーズ，シナリオ，ランに対する修正操作は，操作対象を選択して行う．操作対象を選択すると，その対象に対して実行可能な操作に対応したボタン列が表示されるので，ボタンを押すことで操作を実行することができる．フェーズの選択は，仕様記述の黒枠内をクリックして行う．シナリオの左側の帯をクリックすると，シナリ
オが選択される．帯の右側のランの上をクリックすると，ランが選択される．

3.3. VDMPad-EpiLog の使用例
本節では，VDMPad-EpiLog の典型的な使用例として，

VDMPad 上でのカウンタの仕様記述の探索的試行の例を紹介し，その履歴を整理するステップを示す．記述する
カウンタは，自然数のカウント値を 1 ずつ増加させていくものである．ただし，上限値が設定され，上限値を越えると 0 に戻るものとする．カウンタに対する操作として，カウント値を進める inc，カウント値を 0 にリセッ
トする reset，上限値を設定する setMax の 3 つを提供するが，ここでは，まずはカウント値を進める inc を定義するための記述作業を対象とする．他の 2 つの操作

reset および setMax の定義は省略し，VDM-SL 仕様
中に記述しない．
図 8 に示した画面では，2 つのフェーズが表示されている．最初のフェーズ (以後，フェーズ 1) では，暫定的な仕様記述を入力し，2 つのシナリオが検討された．最初のシナリオでは，inc を連続して 2 回実行して，カウ
図 8. 整理開始時の画面例

ント値が期待通りに 1 ずつ増加することを確認した．次に，カウント値が上限値を越える場合の動作を確認するために，カウント値 count と上限値 max にそれぞれ 9を設定し，inc 操作を行った．すると，カウント値が 0になることが期待されていたところが，10 となった．仕様記述者はこの時点での仕様記述に誤りがあることに気付いた．
仕様中の inc 操作の定義の中で，count + 1 mod(max + 1) とある式は，正しくは (count + 1) mod(max + 1) を意図していた．表現式 count + 1 mod

100

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)

図 9. 軽微な修正のフェーズを合併した画面例

図 10. シナリオを再実行した画面例(max + 1) は，演算子の結合順位により count + (1mod (max + 1)) と解釈され，1 mod (max + 1)

めに黄色を背景色にして表示されている．

は常に 1 であることから，inc 操作は上限値に関係なで，有効にすることができる．図 10 に，1 つ目のシナリ

く常にカウント値を 1 ずつ増加させる動作となっていオを再実行した結果を示す．初期状態から inc 操作を 2

無効なランは，新しい仕様記述の上で再実行することた．仕様記述者はこの誤りに気付き，修正を行い，再び回実行し，結果は元のフェーズ 1 での実行結果と同一でカウント値 count と上限値 max にそれぞれ 9 を設定あった．最初の探索的試行の段階では，誤りを含んだ仕し，inc 操作を行った．これが 2 つ目のフェーズ (以後，

様記述での実行を確認しただけであったところが，そのフェーズ 2) であり，実行結果は仕様記述者の意図通り，

履歴をまとめる作業を通して，修正後も同様に意図通り

カウント値が 0 になった．

の動作をすることを確認することができた．

フェーズ 2 はフェーズ 1 からの軽微な修正であり，こ次に，カウント値が上限値を超えた場合のシナリオのこではフェーズ 2 を中心に探索的試行をまとめることに再実行を行う．カウント値が上限値を超えた場合についする．ただし，フェーズ 1 では初期状態から inc 操作ては，仕様記述を修正する前は意図した通りの動作をしを 2 つ行うシナリオを実行しているが，フェーズ 2 でなかった．図 10 では，元の意図した通りの動作ではなは実行していない．本来はフェーズ 2 でも実行すべきでかったランが無効化された状態で表示されている．このあるが，仕様記述者は上限値を超えた時の動作の修正をランを再実行することで，この仕様記述では意図した通行っており，他のシナリオは念頭になかった．そこで，りの結果に置き換わることを確認することができる．再フェーズ 1 で検討したシナリオをフェーズ 2 にまとめる

実行の結果を図 11 に示す．元のフェーズ 2 で実行されため，フェーズ 1 をフェーズ 2 に合併する．

たシナリオと同一の結果であることが確認できる．

図 9 に合併の結果を示す．合併の結果，フェーズは 1

カウント値が上限値を超えた場合のシナリオは内容がつのみになった．このフェーズではフェーズ 2 にあった，同一であることから，冗長であり削除することにする．

誤り修正後の仕様記述が使われる．元のフェーズ 1 から削除することで，一連の探索的試行の整理が完了する．

合併で移動した 2 つのシナリオに含まれるランは，元の履歴を整理した結果を図 12 に示す．この探索で到達し誤りを含む仕様記述で実行されたため，このフェーズのた仕様記述と，その上で検討された 2 つのシナリオが並履歴としては正しくない．これら 2 つのシナリオの合わ

んで表示されている．1 つ目のシナリオは，初期状態かせて 3 つのランは無効であり，無効であることを示すた

ら inc 操作を 2 回連続で行うもので，仕様記述者の意図

101

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)

通りの動作であることが確認された．2 つ目のシナリオ
は，カウント値が上限値を越える場合の inc 操作を行う
もので，これも仕様記述者の意図通りの動作であることが確認された．これら 2 つのシナリオがこの仕様記述で想定された利用シナリオであり，それぞれユニットテス
トにおけるテストケースとして利用することができる．

4. 関連する既存ツール
ソフトウェア開発を支援するための工学研究では，開発の履歴の保存や集積，追跡性の確立は古くからの課
題の 1 つである．現在ソフトウェア開発で多く利用されている統合開発環境では操作履歴に関する機能として

undo/redo を提供するものは多いが，履歴に構造を与えて系統的にまとめることは行われていない．大きな粒度での開発の履歴の保存や集積，追跡性の確立は，コードレ
ポジトリおよびそれと統合された開発チームホスティン
グサービスが提供している．github は現在オープンソー
スをはじめ広く利用されている開発チームホスティング

図 11. 全シナリオを再実行した画面例

サービスである．ソースコードレポジトリは分散バー
ジョン管理システム git によりバージョン間の関係を有向グラフとして保存することができる．また，イシュー
管理システムおよび修正提案 (pull request) から特定のバージョンへの参照を記録することができることから，あるバージョン差分の意図がどの問題を解決するためのもので，それがどの修正提案として提案され，誰によりソースコードレポジトリに取り入れたかを追跡可能にしている．このことから，github は開発コミュニティにおける長期間での開発の記録を整理し保存し，追跡性を確保した形で集積する機能を持つサービスと言える [6]．ただし，github でのバージョン管理，イシュー管理および修正提案は，開発の中での極めて大きな粒度での試行を捉えるものであり，基本的に個人間の円滑な連携や，新規参入者が文脈を理解しやすくするための仕組みである．
本研究が扱うような，個人作業の内部でおこなう 1 つ 1つの試行的な評価実行を対象にしたものではない．
ローカルな git レポジトリにも，バージョン差分を併合する機能があることから，個人作業での試行の履歴を整理することができる．しかし git レポジトリが扱う対図 12. 重複シナリオを削除し整理を完了した画面例

象はソースコードであり，インタプリタ上あるいはコンパイルされた実行ファイルを動作させた履歴は扱わない．
ユニットテスティングでのユースケースのバージョン差分を管理することで，各試行で検討したシナリオの変遷

102

SEA

ソフトウェア・シンポジウム 2020 (オンライン開催)

6. 謝辞

を記録することが可能だが，本研究で扱う極めて短期間での試行とは，扱う試行の粒度が異なると考えられる．

本研究は，JSPS 科研費 (18K18033) および JSPS 科研

5. 議論とまとめ

費 (19K11911) の助成を受けた．有益なご指摘を頂いた
査読者の方々に感謝する．

探索的な仕様記述で行われる探索的試行の履歴から，探索全体を整理し知見として残すための枠組みとして，

参考文献

フェーズ，シナリオ，ランによる構造化と，構造化された履歴への編集操作を提案した．具体的なツールとして[1] 小田朋宏, 荒木啓二郎 “形式仕様工程の初期段階に着VDMPad-EpiLog を実装し，その利用例を示した．

目した統合仕様記述環境 ViennaTalk”, コンピュータ

VDMPad-EpiLog は VDM-SL 仕様を対象として扱うことを前提に設計されている．VDM-SL はモデル規範型の形式仕様記述言語であり，モデルが取りうる状態空間

ソフトウェア, 34 巻, 4 号, ppp. 4 129-4 143, 日本ソ
フトウェア科学会, 2017.

[2] J. Fitzgerald and P. G. Larsen “Modelling Systems –Practical Tools and Techniques in Software Develop-

を厳密に規定する．状態空間が明確に規定されていることで，試行における評価実行の文脈を容易に保存するこment”, Cambridge University Press, 1998.

とができる．
プログラミング言語でのユニットテスティングでもシ[3] P. G. Larsen, N. Battle, M. Ferreira, J. Fitzgerald, K.
Lausdahl and M. Verhoef “The Overture Initiative – In-

ナリオを再現するための状態設定を行うが，一般にプロ
グラミング言語では状態空間が明示的でなく，多くの不tegrating Tools for VDM”, SIGSOFT Softw. Eng. Notes,
Vol. 32, No. 1, pp. 1–6, 2010.

確定要素を抱える．例えば，ファイル入出力は多くの場
合にはバッファリング IO を通して，オペレーティング[4] P. Hamill “Unit Test Frameworks”, O Reilly, 2004.

システムのシステムコールが提供する共有リソースにアクセスする．他のプロセスとの相互作用も暗黙的に発生[5] 小田朋宏, 荒木啓二郎 “アジリティのある探索的形式仕様記述のためのテストフレームワーク”, ソフト

する可能性がある．これらはソースコードには明示的に記述されない部分であり，VDMPad-EpiLog が行うよう

ウェアシンポジウム 2018 論文集, 2018.

な細粒度での再実行を実現するのは容易ではない．シナリオが前提とする状態の再現の容易さと，それがもたら[6] L. Dabbish, C. Stuart, J. Tsay, and J. Herbsleb “So-すシナリオに対する編集操作は，モデル規範型の形式仕

cial coding in GitHub: transparency and collaborationin an open software repository”, in Proceedings of theACM 2012 conference on computer supported cooper-

様記述言語 VDM-SL の利点として挙げることができる．
今後の課題として，より複雑な仕様記述での探索的ative work, pp. 1277-1286, 2012.

試行の支援が挙げられる．VDMPad は比較的小規模な仕様記述を想定して設計・実装されているため，複数モジュールに分割された複雑な仕様記述を扱うのに適していない．より複雑化した VDM 仕様を扱うために，

VDMPad-EpiLog と同様な機構を ViennaTalk にも実装し，比較評価したい．
関連研究で挙げた科学研究向けノートブック環境への応用も考えられる．状態の再現性の高さ，および，操作実行の結果の検証の容易さは，再現性や検証可能性が要求されるノートブック環境の実現にも有用であることが期待できる．

103

SEA