| 講演名 | 1994/3/9 並行論理型プログラミング言語における段階的プログラム記述の検証 小田 幸弘, 村上 昌己, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では、並行論理型プログラミング言語GHCについて、プログラムを有限集合に対応づける新しい意味論を構成する。これは、ある有限集合とそれを無限集合へと展開する演算によってなされる。また本稿ではこの意味論について、プログラムの意味をプログラムの仕様、意味写像をプログラムからプログラムの仕様を抽出する手続きと捉える。そしてこの意味論をラビットプロトタイピングのような段階的プログラム記述おける形式的な検証に応用する。すなわち意味写像によって改変前のプログラムから仕様を組織的に生成し、改変後のプログラムがこれを満足するかを検証することで、プログラムの機能継承についての形式的な検証の手段とする。 |
| 抄録(英) | In this paper,we construct a new semantics for concurrent logic programming language GHG-which maps a program to a finite set.We achieve that by a finite set and an operator which extends the set to an infinite one.We regard the semantics-mapping as a procedure to extract specifications of programs.We apply the semantics to the formal verification for stepwise programming such as rapid- prototyping.We present a method to verify whether the next version of a program inherits the functions of the original version using the specification generated from the original one by the semantics- mapping. |
| キーワード(和) | GHC / 形式的意味論 / 段階的プログラミング / 形式的仕様記述 |
| キーワード(英) | GHC / formal semantics / stepwise programming / formal specification |
| 資料番号 | COMP93-81,SS93-49 |
| 発行日 |
| 研究会情報 | |
| 研究会 | COMP |
|---|---|
| 開催期間 | 1994/3/9(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Theoretical Foundations of Computing (COMP) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 並行論理型プログラミング言語における段階的プログラム記述の検証 |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification for stepwise programming in concurrent logic language |
| サブタイトル（和） | |
| キーワード(1)（和/英） | GHC / GHC |
| キーワード(2)（和/英） | 形式的意味論 / formal semantics |
| キーワード(3)（和/英） | 段階的プログラミング / stepwise programming |
| キーワード(4)（和/英） | 形式的仕様記述 / formal specification |
| 第 1 著者 氏名（和/英） | 小田 幸弘 / Yukihiro Oda |
| 第 1 著者 所属（和/英） | 岡山大学大学院工学研究科 Graduate school Information Technology,Okayama University |
| 第 2 著者 氏名（和/英） | 村上 昌己 / Masaki Murakami |
| 第 2 著者 所属（和/英） | 岡山大学工学部情報工学科 Department of Information Technology,Okayama University |
| 発表年月日 | 1994/3/9 |
| 資料番号 | COMP93-81,SS93-49 |
| 巻番号（vol） | vol.93 |
| 号番号（no） | 496 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |