2024-03-28T21:24:35Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001616562023-11-17T02:17:36Z06504:08672:08730
VDM++仕様からC#コードを生成するツールの開発jpnソフトウェア科学・工学http://id.nii.ac.jp/1001/00161622/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=161656&item_no=1&attribute_id=1&file_no=1Copyright (c) 2016 by the Information Processing Society of Japan仙台高等専門学校 広瀬キャンパス仙台高専千坂, 優佑岡本, 圭史形式仕様記述は、形式仕様記述言語で仕様を記述することで、仕様の誤りの自動検証を可能にする。既存ツールを用いて形式仕様記述言語VDM++で記述された仕様からプログラミング言語のコードを生成できるが、JavaとC++にしか対応しておらず、また操作の事後条件は無視される等の制約がある。本研究では、VDM++仕様からC#コードを生成するツールの開発を目指す。VDM++記述の検証後に、このツールを用いてVDM++仕様中の事前条件、事後条件および不変条件を生成コード中の契約に変換し、C#から利用できるCode Contractsによる契約情報に基づく実装コードのテストを実施することで,事前・事後・不変条件に基づく検証をシームレスに実現できる。AN00349328第78回全国大会講演論文集201613633642016-03-102016-05-18