「トップページ」の編集履歴（バックアップ）一覧に戻る
トップページ - (2010/12/13 (月) 17:39:32) のソース
#javascript(){{
<script type="text/javascript">
var _gaq = _gaq || [];
_gaq.push(['_setAccount', 'UA-20218017-1']);
_gaq.push(['_trackPageview']);
(function() {
var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true;
ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js';
var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s);
})();
</script>
}}
* 1. はじめに
----
このページでは、 Alloy Analyzer というツールを使って、ソフトウェアの仕様を形式的に記述/検査することにより、
バグの少ない仕様を作成する方法を説明していきたいと思います。
ここで言う仕様のバグとは、
- 記述漏れ
- 矛盾
- 曖昧さ
- 要求を満たしていない
といったバグを指します。
仕様を形式的に記述/検査することのできる言語やツールは、VDM, B, Z, Isabelle など他にも色々ありますが、
Alloy はそれらにくらべてより軽いフットワークで記述/検査することができるツールです。
それらのツールと Alloy との比較も、機会があればご紹介したいと思います。
* 2. Alloy を使った形式仕様記述の特徴
----
- 数理論理学＋集合論をベースとした Alloy の言語で仕様を記述します。
- 書いた仕様を、簡単に検査することができます。
-- 難しい論理式の証明などは必要ありません。
- 検査結果は図で表示してくれるので、結果を目視で直感的に理解することができます。
- 仕様で書いた振る舞いをシミュレーションすることができます。
* 3. このページのスコープ
----
ここでは仕様のうち、概要レベルの仕様や、重要な部分だけを抜き出した仕様といった、抽象度の高い仕様をスコープとしています。
抽象度の高い仕様の段階で Alloy を使って十分検査しておけば、その後の仕様化や設計/実装段階で、根本的な仕様バグが見つかって手戻りが発生することを減らすことができます。
最終的な仕様書に書くような詳細な仕様は、ここではスコープ外とします。
Alloy の構文的に書きづらいものもありますし、規模が大きくなると Alloy の特徴である目視の検査が生かしづらくなります。
詳細な仕様の記述/検査は、別の言語やツールにまかせます。
* 4. このページの対象者
----
形式仕様記述に興味はあるけど、やったことが無い方を主に対象としています。
Alloy は難しい数理論理学の知識は必要ありませんし、論理式の計算もする必要がないので、初めての形式仕様記述に向いていると思います。
必要な前提知識
- 日本語で何らかの仕様を書いたことがあること
- 高校でやる程度の命題論理 (and, or, not とか) と、集合についての知識
* 5. Alloy Analyzer
----
Alloy Analyzer は、条件を論理式で指定すると、その論理式を満たす例 (インスタンス) を見つけてくれるツールです。
このインスタンスを見つける機能をうまく使うと、仕様に矛盾が無いか、仕様が要求を満たしているか、といったことを検査することができます。
Alloy Analyzer は MIT で開発されたツールで、現在バージョン 4 がリリースされています。
http://alloy.mit.edu/community/
日本語が使えるAlloy Analyerを作りました。
[[Unicode対応版Alloy]]
----
連絡先(hi0.alloy@gmail.com)
Total : &counter(total)
Today : &counter(today)
----
