はてなブックマーク

                                                                     

2014年12月5日・7日に行われるモデル発見ツールJSTMセミナーの資料置き場です． 12/6：資料・ツールの修正版をアップロードしています． 資料 スライド資料一式（pdf in zip） 演習用プロジェクトファイル（そのままImportできるzip） ツールダウンロード セミナーではツールインストール済のPCを用意しますので，自身でのインストールは不要です． 自身のマシンで試したいときのためのプラグインファイル Eclipse IDE for Java and DSL Developersを取得して下さい． Eclipseのeclipse/pluginフォルダーに，上記ファイルを解凍して出てくるjarファイルを追加して下さい． Javaはバージョン7以上のみ対応しています． ※ セミナー例題以外での挙動，Linuxでの挙動についてはまだ十分に確認していません．試用に際し何か要望や質問

青字： 不具合が埋め 込まれる場所 黒字： 不具合が発見 される場所 赤字： 不具合の除去 における コストの増加率 １． 早くバグ を見つける ２． バグ検出の コストを下げる サイト内の紹介資料 累計コストを下げる ピークコストを下げる class EventManager instance variables users : set of User := {}; rooms : set of Room := {}; events : set of Event := {}; inv (forall ev1, ev2 in set events & ev1 <> ev2 => ev1.room <> ev2.room or ev1.date <> ev2.date); reservations : set of Reservation := {}; inv … operations …

VDM自体やその言語，ツールに関するFAQです． VDMに限らない形式手法全般については，著者もかかわっているディペンダブル・システムのための形式手法の実践ポータルなどをご参照下さい． 書籍にて解説しなかった情報を中心に載せています． あくまで著者自身の試用・見解に基づくものですので，特にツールに関する情報についてはぜひ公式な情報もご確認下さい． 質問項目は随時追加予定です（最終更新2012/01/26）．リクエストも受け付けております． 目次 位置づけ どういう状況に対してどういう利用効果が期待できる？ VDM-SL/VDM++はプログラミング言語じゃないの？ VDMの欠点・限界は？ 活用 VDM-SLとVDM++の違い（言語上・ツール上）は？どちらを使えばよい？ コード生成は使える？生成されたコードが気に入らない 文法・記述 セミコロンを打つべき場所がわからない 予期せぬ場所で操作の実

近代科学社より出版されている書籍「VDM++による形式仕様記述」のWebサイトです．VDMToolsやOverture（Eclipseベースのツール）の利用法なども載せています． Amazonへのリンク（紹介文を下記に引用） 機能仕様書の曖昧さ、不正確さ、不整合などに起因する手戻りに悩まされている開発者、近年話題となっている形式手法をまずは手軽なところから学び実際に使ってみたい開発者・大学院生・研究者へ！ 一般の開発者になじみやすい形で、仕様をはじめとした開発上流の成果物を厳密に（ただし抽象的に）記述し、様々な分析を行いそれらの品質確保に取り組む形式仕様記述手法である VDM（Vienna Development Method）の具体的かつ網羅的な入門書、解説書。 更新履歴 2017/6/1： VDMToolsのWebサイト変更に伴いリンクを張り替えました． 2011/11/10： 7章の