| 大会名称 |
|---|
| 2009年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2009 |
| 発行日 |
| 2009/8/20 |
| セッション番号 |
| 3B |
| セッション名 |
| モデル検査 |
| 講演日 |
| 2009/09/02 |
| 講演場所(会議室等) |
| B会場（9号館1F 912教室） |
| 講演番号 |
| B-014 |
| タイトル |
| VDM-SLの陽仕様記述からLispファミリ言語Schemeへの変換 |
| 著者名 |
| 長谷 卓容, 和崎 克己, |
| キーワード |
| 形式手法, 仕様記述, 陽仕様, コード変換, VDM-SL, Scheme |
| 抄録 |
| Floyd-Hoare論理において、あるプログラムについて、部分的正当性の表明を導出することを考えるとき、そのプログラムが満たすべき事前条件・事後条件を、それぞれそのプログラムの仕様の一種とみなす。その仕様を記述する言語として仕様記述言語VDM-SLが存在する。VDM-SLは設計上の仕様であるため、そのままの状態では実行可能ではなく、かつシミュレーションを目的としたとき、外界に相当する部分は手作業で準備する必要があった。このためVDM-SL上での記述と、それに対応する実装で仕様通り動作することの確認とを、一貫して検証する環境が必要と考えた。本稿では、VDM-SL上で記述された陽仕様をLisファミリ言語Scheme上の関数へ変換する際の、種々の方策について述べ、変換する上での問題点について明らかにする。 |
| 本文pdf |
| PDF download (120.4KB) |