JMLを用いた在庫管理プログラムの設計とESC/Java2を用いた検証

尾鷲, 方志; 岡野, 浩三; 楠本, 真二

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2007, 107(176), 37-42

Number of Access:303（2025-09-04 14:41 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27419

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr107_176_037 pdf None 588 KB 123 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
JMLを用いた在庫管理プログラムの設計とESC/Java2を用いた検証
A Case study : Design of Warehouse Management Program in JML and Verification with ESC/Java2
JML　ヲ　モチイタ　ザイコ　カンリ　プログラム　ノ　セッケイ　ト　ESC　Java2　ヲ　モチイタ　ケンショウ
Creator
CreatorName
尾鷲, 方志 ; オワシ, マサユキ ; Owashi, Masayuki
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Subject
ESC/Java2
JML
在庫管理問題
設計検証
契約による設計
Warehouse Manaagement
Design and verification
Design by Contract
Abstract
近年,契約に基づく設計による開発手法が脚光を浴びている.これを実現する言語の一つとしてJMLが挙げられる.本研究では、プログラム設計の共通問題である酒屋の在庫管理問題に対してJMLを用いて仕様作成を行いプログラムを記述し,ESC/Java2を用いて実際に検証を行った.本報告では,この過程で得られた知見(作業量,現バージョンのESC/Java2の記法の問題点,解決法など)について報告する.また,ソフトウェア開発にJMLを用いる上での課題について考察する.
In the software development, the notion "Design by Contract(DbC)" has been recently obtained a lot of attentions. In the DbC, contracts are represented as assertions. JML (Java Modeling Language) is one of the languages able to represent such assertions. In this research, we designed and programmed the Warehouse management program in Java and JML as a case study. This design is verified with "ESC/Java2". The paper reports the knowledge about what we learned in this process. Discussion about the issue on using JML in software development is also presented.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
107(176)
Page
37-42
Date of Issued
2007-07-26
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27419
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2007 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article