産総研：システム検証研究センター：CVS研修コース「Agdaによる仕様記述」研修コース「 Agda による仕様記述」開催のお知らせ ■コース概要 近年、体系的にシステムを開発する手段の一つとして数理的技法(形式手法)が注目を集めています。例えば形式仕様記述の枠組みを使うと、仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。結果として設計書や実装に不具合の種が入り込むことを防ぐことができます。 本コースでは、形式仕様記述の概要とその実際を講義と演習を通して実感して頂きます。演習環境として用いるツール Agda は(１)関数型プログラミング言語(２)形式仕様の処理系(３)定理証明支援系の側面を持つツールです。本コースでは(１)(２)の側面を使い、抽象的なデータの定義と関数を用いてシステムを記述すること、記述を支援する Agda の機能と操作法を扱います。演習の時間を多くとり、実例と経験から形式仕様記述を理解できるコースとなっています。 ■目標 (１
