【作業全体の説明】

甲南大学知能情報学部のソフトウェア設計検証研究室です．
この度は私共の実験にご協力頂きまして誠にありがとうございます．

これから取り組んでいただくのは，Alloy と DTRAM と呼ばれる2つの仕様記述言語による仕様記述の読解，記述内容についての設問への解答，およびアンケートへの回答です．
全体の作業時間としては，3~5時間程度を想定しています．仕様記述言語全般についての解説，Alloy および DTRAM の説明などは実験の中で行います．
仕様記述の対象となるシステムは2つあり，それぞれのシステムについて，Alloy による仕様記述と DTRAM による仕様記述をお読みいただき課題に取り組んでいただきます．
したがって，取り組んでいただく課題は計4つになります．それぞれのシステムの仕様は小さく，そのため仕様記述の行数も多くはありません．
これらの課題は，すべてWeb上で行っていただきます．課題を終えるたびに，設問およびアンケートにお答えいただきます．
これ以降お答えいただく設問およびアンケートは，課題毎に3つ，対象システム毎に1つ，すべての課題の終了後に1つの計15個です．
設問およびアンケートの数は多いですが，1つ1つの質問項目は多くありません．課題が終わるたびに作業を中断していただいて構いません．

実験の流れ：

実験は以下の流れで行います．

実験用のWebページ(本ページ)にアクセスしていただきます．
Alloy の概要を説明します．
1つ目のシステムであるツイートシステムの仕様を説明します．
1つ目の課題に取り組んでいただきます．

ツイートシステムの Alloy による仕様記述を読んで理解していただきます．（記述内容の解説も行います．）
1つ目の設問にお答えいただきます．
2つ目の設問にお答えいただきます．
課題アンケートにお答えいただきます．

DTRAM の概要を説明します．
2つ目の課題に取り組んでいただきます．

ツイートシステムの DTRAM による仕様記述を読んで理解していただきます．（記述内容の解説も行います．）
1つ目の設問にお答えいただきます．
2つ目の設問にお答えいただきます．
課題アンケートにお答えいただきます．

ツイートシステムに関するアンケートにお答えいただきます．
2つ目のシステムである酒屋の在庫管理システムの仕様を説明します．
3つ目の課題に取り組んでいただきます．

酒屋の在庫管理システムの Alloy による仕様記述を読んで理解していただきます．（記述内容の解説も行います．）
1つ目の設問にお答えいただきます．
2つ目の設問にお答えいただきます．
課題アンケートにお答えいただきます．

4つ目の課題に取り組んでいただきます．

酒屋の在庫管理システムの DTRAM による仕様記述を読んで理解していただきます．（記述内容の解説も行います．）
1つ目の設問にお答えいただきます．
2つ目の設問にお答えいただきます．
課題アンケートにお答えいただきます．

酒屋の在庫管理システムに関するアンケートにお答えいただきます．
最後に実験全体に関するアンケートにお答えいただきます．

【Alloyの説明】へ