| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2019-01-16 09:25 論理制約付き書換えにおける構造体および共用体の表現について ○金澤慶明・西田直樹・酒井正彦（名大）  MSS2018-67 SS2018-38 |
|
| 抄録 | （和） | 近年，項書換え系への変換に基づいた手続き型のプログラムの検証について研究が行われており，実行の中間状態を表現する項から制御フローをモデル化するための論理制約を分離して表現できる論理制約付き項書換え系への変換が注目されている．しかし，既存手法ではデータ型として整数とその1次元配列のみをデータとして扱うC言語プログラムを対象としており，ビット数が異なる基本データ型や構造体，共用体を扱っていない．本稿では，構造体や共用体などのサイズの異なるデータ構造を論理制約付き項書換えの枠組みで扱うための，構造体や共用体のビットベクトルを用いた表現，およびそれらのメンバへアクセスするための書換え規則の構成法を提案する． |
| （英） | Recently, several methods for verifying imperative programs by means of transformations into term rewriting systems have been investigated. In particular, constrained rewriting systems are popular as sources of such transformations, since logical constraints used for modeling control flows can be separated from terms that represent intermediate states of the execution of target programs.In the existing methods, data types that can be used in target programs are, however, restricted to the integers and their one-dimensional arrays, and hence we are not allowed to use other primitive data types, structures, or unions.In this article, we propose a bit-vector representation of basic data types that are recursively defined over size-fixed primitive data types, structure, and unions in the framework of logically constrained rewriting, and then propose a construction of rewrite rules that access members of structures and unions. | |
| キーワード | （和） | 論理制約付き書換え / プログラム変換 / ビットベクトル / 構造体 / 共用体 / / / |
| （英） | logically constrained rewriting / program transformation / bit vector / structure / union / / / | |
| 文献情報 | 信学技報, vol. 118, no. 385, SS2018-38, pp. 67-72, 2019年1月. | |
| 資料番号 | SS2018-38 | |
| 発行日 | 2019-01-08 (MSS, SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | MSS2018-67 SS2018-38 |
|
| 研究会情報 | |
| 研究会 | MSS SS |
| 開催期間 | 2019-01-15 - 2019-01-16 |
| 開催地（和） | 沖縄県青年会館 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2019-01-MSS-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 論理制約付き書換えにおける構造体および共用体の表現について |
| サブタイトル（和） | |
| タイトル（英） | On Representation of Structures and Unions in Logically Constrained Rewriting |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 論理制約付き書換え / logically constrained rewriting |
| キーワード(2)（和/英） | プログラム変換 / program transformation |
| キーワード(3)（和/英） | ビットベクトル / bit vector |
| キーワード(4)（和/英） | 構造体 / structure |
| キーワード(5)（和/英） | 共用体 / union |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 金澤 慶明 / Yoshiaki Kanazawa / カナザワ ヨシアキ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2019-01-16 09:25:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | MSS2018-67, SS2018-38 |
| 巻番号（vol） | vol.118 |
| 号番号（no） | no.384(MSS), no.385(SS) |
| ページ範囲 | pp.67-72 |
| ページ数 | 6 |
| 発行日 | 2019-01-08 (MSS, SS) |
[研究会発表申込システムのトップページに戻る]