スコーレム標準形を用いたZ仕様の代数仕様への変換
スポンサーリンク
概要
- 論文の詳細を見る
形式仕様言語Zは高い表現力を持っているが,それによって記述された仕様を検証するためには,人間が地道に演繹規則に従って計算しなければならない.ソフトウェアの規模が増大化し,構造が複雑化すると,もはや人手で処理することは困難である.この問題を解決するために,Zで記述された仕様(以降,Z仕様と呼ぶ)を実行可能な処理系で動作可能な記述に変換し,コンピュータ支援による検証を行なうというアプローチがいくつか提案されている.我々はZ仕様を実行可能な処理系を持つ代数仕様への変換規則と,その規則に基づいて構築した仕様の変換システムを提案してきた.従来のシステムでは,ごく限られた記述しか扱えなかった.本稿では,従来では対応できなかった,限量記号を含む論理式をスコーレム標準形を利用して等式で記述する方法を提案する.変換によって生成された代数仕様は手動による修正が必要であるが,この枠組が体系化されると,Z仕様から代数仕様への変換作業効率の向上が見込まれる.そしてZ仕様の検証がコンピュータ支援により代数仕様によって自動化されることになり,検証作業の効率化も期待できる.
- 社団法人電子情報通信学会の論文
- 2002-05-10
著者
関連論文
- Gastrointestinal stromal tumor(GIST)の終末期の特徴とターミナルケア (特集 臓器別 消化器癌終末期の特徴とターミナルケア)
- 肝細胞癌に対する経皮的ラジオ波焼灼療法による遅発性横隔膜ヘルニア嵌頓の1例
- RS-146 胃上部早期癌に対する噴門側胃切除・空腸間置術の長期QOLの検討(要望演題7 胃機能温存術,第63回日本消化器外科学会総会)
- WS-7-6 イマチニブ治療におけるGIST二次耐性腫瘍 : KIT遺伝子解析からみた集学的治療の必要性(第107回日本外科学会定期学術集会)
- O-2-368 食道切除・胃管再建術後における慢性貧血(食道 サルベージ,一般演題(口演),第63回日本消化器外科学会総会)
- 胃癌に対する腹腔内三部位洗浄細胞診(体腔洗浄細胞診と予後, 第44回日本臨床細胞学会秋期大会)
- RS-248 胃癌ESD後手術症例の臨床病理学的検討(要望演題13-1 早期胃癌の治療1,第63回日本消化器外科学会総会)
- WS-8-10 再発性GISTにおけるイマチニブ治療 : 分子標的薬をもちいた集学的治療のモデル疾患として(ワークショップ8 再発腫瘍の外科治療法および集学的治療方針-食道・胃-,第63回日本消化器外科学会総会)
- 23 腹腔細胞診陽性胃癌に対するTS-1/CDDP術前化学療法の検討(I.一般演題,第67回新潟癌治療研究会)
- 20 当院における腹腔鏡下大腸手術の現況(一般演題,第264回新潟外科集談会)
- A-4-6 多次元畳み込み信号の分解法(A-4. ディジタル信号処理)
- 多項式の因数分解を利用した劣化画像の復元法
- 制約付き悪条件連立1次方程式の解法
- GISTの診療におけるPET検査の応用 (特集 外科医に必要なPET検査の知識--その有用性と問題点)
- 交通工学と制御工学の統合による交通流制御システムの設計
- 交通ネットワークの交通流制御に関するシステム理論的考察(モバイルユビキタス時代のネットワークとサービス(キーワード: ユビキタス, センサーNWネットワークアーキテクチャ, Ad-Hoc, 及び, そのアプリケーションなど))
- 都市道路網の信号制御に関するシステム理論的考察
- 交通ネットワークの渋滞長制御(ITS)
- 交通ネットワークにおけるOD旅行時間の解析と算定
- 都市道路網における交通流円滑化システムの一設計(モバイルコンピューティングとユビキタス通信高度交通システム合同研究報告)
- 都市道路網における交通流円滑化システムの一設計
- 信号交差点における交通流ダイナミクスの解析(ITS情報処理・一般)
- WS-5-8 残胃癌切除症例の臨床病理学的特徴と遠隔成績(ワークショップ5 残胃癌に対する治療戦略,第64回日本消化器外科学会総会)
- WS-4-5 転移・再発性GISTに対するイマチニブ治療 : 二次耐性出現と耐性腫瘍切除の治療成績(第108回日本外科学会定期学術集会)
- P-3-69 胃上部臨床的早期癌における噴門側胃切除術適応の妥当性(胃・十二指腸 早期癌2,一般演題(ポスター),第64回日本消化器外科学会総会)
- RS-24-5 イマチニブ耐性GISTに対する動脈化学塞栓療法(要望演題24-1 消化管GISTに対する診断と治療1,第64回日本消化器外科学会総会)
- 13 高齢者食道癌に対し根治的化学放射線療法後にSalvage手術を施行した3例の検討(一般演題,第82回新潟消化器病研究会)
- P-2-29 食道癌術後患者における肺炎発生率および危険因子についての検討(食道 術後合併症および再発,一般演題(ポスター),第64回日本消化器外科学会総会)
- 30 転移・再発性GISTに対する分子標的治療 : イマチニブ耐性腫瘍の遺伝子学的特徴(一般演題,第261回新潟外科集談合)
- リファクタリングによるソフトウェアの品質向上に関する考察
- UMLによる折り紙シミュレーションシステムの設計
- 交通ネットワークの交通流制御に関するシステム理論的考察(モバイルユビキタス時代のネットワークとサービス(キーワード: ユビキタス, センサーNWネットワークアーキテクチャ, Ad-Hoc, 及び, そのアプリケーションなど))
- 形式仕様記述に基づく検証の自動化
- 都市道路網における交通流円滑化システムの一設計(モバイルコンピューティングとユビキタス通信高度交通システム合同研究報告)
- 階層型ニューラルネットワーク間の競合による画像の領域分割
- 信号交差点における交通流ダイナミクスの解析(ITS情報処理・一般)
- 多項式の因数分解を利用した畳み込み画像の分解法
- PCクラスタにおける並列計算の動的負荷分散
- 都市道路網の渋滞制御システム
- アコヤガイの人工授精における媒精時間の違いが受精率および幼生の成長に及ぼす影響
- 消化管間質腫瘍(GIST) (特集 悪性腫瘍の術中病理診断を効果的に活用する--どこを検索すべきか,どう対応すべきか)
- 抑制飼育期間におけるアコヤガイの閉殻力および軟体部諸形質の変動
- 交通ネットワークにおけるOD旅行時間の解析と算定
- 交通量収支に基づく交通流円滑性の解析
- 低塩分海水養生によるキズ・シミの無い真珠の生産率向上効果
- 上部消化管穿孔に対する外科治療 (特集 急性腹症の手術)
- 複数の階層型ニューラルネットワークを用いた画像の領域分割
- スコーレム標準形を用いたZ仕様の代数仕様への変換
- 交通ネットワークの渋滞長制御(ITS情報処理・一般)
- 交通ネットワークの渋滞長制御
- 判別分析法を用いた劣化画像からのエッジ領域の自動抽出法
- 形式仕様言語Z
- GUIを用いたZ仕様検証支援環境の提案
- 有機的プログラミング言語GAEAの代数仕様記述
- 有機的プログラミング言語GAEAの単一化の代数仕様記述
- 有機的プログラミング言語GAEAの単一化について
- 書き換え理論に基づく有機的プログラミング言語GAEAの意味
- PD-4-1 新規抗癌剤著効例に対するサルベージ胃切除の意義 : 多施設共同研究より(PD4 パネルディスカッション(4)StageIV胃癌に対する外科治療の現状と方向性,第111回日本外科学会定期学術集会)
- PS-121-2 虚血性心疾患併存胃癌に対する胃切除例の実態と予後について(PS-121 ポスターセッション(121)胃:周術期管理-1,第111回日本外科学会定期学術集会)
- PS-011-4 噴門側胃切除術,空腸間置再建の適応と長期成績(PS-011 ポスターセッション(11)胃:手術-2,第111回日本外科学会定期学術集会)
- SF-028-2 T4食道癌に対する外科治療(SF-028 サージカルフォーラム(28)食道:手術-3,第111回日本外科学会定期学術集会)
- 水温一定の水槽を用いた養生によるアコヤガイの脱核低減法
- 日本産アコヤガイ Pinctada fucata martensii における閉殻力の遺伝
- 近赤外分光法による閉殻力の強いアコヤガイの簡易選別
- 携帯型近赤外分光計によるアコヤガイの栄養状態の非破壊評価
- マイクロプレートを用いたアコヤガイの人工授精方法
- GISTに対する化学療法後の手術 (特集 「切除困難例」への化学療法後の手術 : 根治切除はとこまで可能か)
- PS-072-3 臨床的SM胃癌に対するD2郭清の意義と成績(PS-072 胃 リンパ節郭清,第112回日本外科学会定期学術集会)
- PS-125-7 慢性透析患者の胃癌に対する胃切除術の実態と予後について(PS-125 胃 周術期-1,ポスターセッション,第112回日本外科学会定期学術集会)
- PS-064-2 食道癌術後の胸腔ドレーン管理(PS-064 食道 周術期管理・内視鏡,第112回日本外科学会定期学術集会)
- 抑制飼育期間におけるアコヤガイの閉殻力および軟体部諸形質の変動