{"created":"2021-03-01T06:16:26.869715+00:00","id":9666,"links":{},"metadata":{"_buckets":{"deposit":"b293f757-7573-461e-83b5-a17fd8da5a0d"},"_deposit":{"id":"9666","owners":[],"pid":{"revision_id":0,"type":"depid","value":"9666"},"status":"published"},"_oai":{"id":"oai:nagoya.repo.nii.ac.jp:00009666","sets":["320:606:607"]},"author_link":["29303"],"item_12_biblio_info_6":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"1989-07-05","bibliographicIssueDateType":"Issued"}}]},"item_12_date_granted_64":{"attribute_name":"学位授与年月日","attribute_value_mlt":[{"subitem_dategranted":"1989-07-05"}]},"item_12_degree_grantor_62":{"attribute_name":"学位授与機関","attribute_value_mlt":[{"subitem_degreegrantor":[{"subitem_degreegrantor_language":"ja","subitem_degreegrantor_name":"名古屋大学"},{"subitem_degreegrantor_language":"en","subitem_degreegrantor_name":"Nagoya University"}],"subitem_degreegrantor_identifier":[{"subitem_degreegrantor_identifier_name":"13901","subitem_degreegrantor_identifier_scheme":"kakenhi"}]}]},"item_12_degree_name_61":{"attribute_name":"学位名","attribute_value_mlt":[{"subitem_degreename":"工学博士","subitem_degreename_language":"ja"}]},"item_12_description_4":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"本論文は,プログラミング言語の代数的仕様記述法および代数的仕様記述法で意味論が与えられた言語のプログラム検証について述べたものである.第1章では,本研究の背景,動機について述べる.近年,ソフトウェアの生産性,信頼性の向上が切実に要求されている.プログラミング言語の形式的仕様記述法および形式的意味論の研究は,ソフトウェア基礎論の一つであり,プログラム検証,プログラム合成,プログラム変換,コンパイラの正当性検証,コンパイラ自動生成などソフトウェアの生産性,信頼性を向上させるために現在進められている研究の基礎を提供する.プログラミング言語の仕様記述法としては,操作的仕様記述法,公理的仕様記述法,表示的仕様記述法,代数的仕様記述法などがある.これらの中で代数的仕様記述法は,構文要素の領域(構文領域)と意味領域を多ソート代数(抽象データ型)として捉え,プログラムの意味をこの二つの代数間の準同型写像(意味写像)によって与える方法である.本方法の特徴は,意味領域を抽象データ型として代数約手法によって記述する点である.抽象データ型は,モジュール性,抽象化,情報隠ぺい,局所化というプログラミング方法論を実現する概念であり,その代数的仕様記述は,形式性,記述性,理解性を持ち,また,必要最小限の情報しか記述しないという特徴を持つ.また,意味論が等式論理に基づいており,他の仕様記述法に比べて理解がしやすい.本論文では,このプログラミング言語の代数的仕様記述法について考察を行う.第2章では,プログラミング言語の代数的仕様記述法を提案する.言語の仕様は,一般に,構文の仕様と意味の仕様からなる.構文の仕様は字面としてのプログラムの集合(以下では構文領域と呼ぶ)を記述するものである．意味の仕様では,意味を与える基礎となる領域(以下では,意味領域と呼ぶ)と字面のプログラムに意味を与える写像(以下では,意味写像と呼ぶ)の2つを記述する．本論文で提案する代数的仕様記述法は,構文領域および意味領域を代数(抽条データ型)として,意味写像をこの2つの代数間の写像として記述する.具体的には,構文領域は文脈自由文法で,意味領域は抽象データ型の代数的仕様記述法で,意味写像は原始帰納的な意味方程式系で記述する.本方法の特徴は,意味領域の仕様を等式のみを用いて与えたことである.これにより,意味領域を厳密に抽衆データ型として捉えることができ,意味写像を構文領域から意味領域への準同型写像で与えており,完全に代数的理論の枠組の中で言語の意味が記述されているので,目的言語ないしは機械とは独立に言語の仕様記述を可能にしている.そのために,記述性と読解性に優れているばかりでなく,十分な形式性を備えた仕様記述法になっており,これまでに抽象データ型の代数的仕様記述の理論の中で得られてきた成果を直接に利用することができるようになった.さらに,本方法による仕様記述から意味が一意に定まること,すなわち,意味写像が一意に存在することを証明する.また,意味写像の性質,すなわち,その意味写像が,構文領域から.意味領域の演算記号で構成される項集合への写像δ'とその項を意味領域上で評価する評価写像evalの合成で表されることを示す.それと同時に,理解の助けのために,簡単ではあるがループ文を含むプログラミング言語SL を例にとり,仕様記述法を具体的に説明する.第3章では,第2章において提案したプログラミング言語の代数的仕様記述法の有効性を実証することを目的として,Pascal風言語PL/O+の代数的仕様記述を与え,その説明を通して,Pascal風言語一般に対する代数的仕様記述の技法を明らかにする.なお,PL/O+は,Wirth がその著書｢アルゴリズム+データ構造=プログラム｣の中でコンパイラの作成の例に用いられた言語PL/O を拡張した言語である.すなわち,PL/O+は,PL/0 の持つ諸機能に加えて,配列,入出力,パラメタ付き手続きなどの機能を持ち,整数配列のソーティングのプログラムを自然に記述できる程度の実用性のある言語である.本章で与えるPL/O+仕様の次のような特徴を持っている.第1は,第2章で与えた代数的仕様記述法に従って,意味領域を抽象データ型として純粋に等式のみを用いて記述したことであり,プログラムの正当性検証などの問題を代数的意味論の枠組の中で取り扱うことができる.第2は,プログラムの意味を入力から出力ヘの関数として考え,それを抽象データ型を用いて記述したことである.すなわち,抽象データ型の代数的仕様記述では,関数をそのままデータとして扱えないので工夫が必要であり,本論文では,関数の表現と関数の表現を関数と解釈して引数に適用する関数によって記述を行っている.第3は,意味領域を規定する等式の集合が項書き換え系として,線形性,無あいまい性を持つように記述したことである.意味領域中の等式は左辺から右辺への書き換え規則と見ることができ,さらに,意味領域の仕様は項書き換え系と見ることができる.また,項書き換え系が線形性,無あいまい性の性質を持てば,書き換え結果が一意に定まる.このことに基づいて,項書き換え系を用いて意味領域の直接実現(記号実行)を行うことができ,さらに,その直接実現を用いて仕様記述された言語のインタプリタを自動生成できる.実際,言語処理系生成システムLass により,本章の仕様からPL/O+ の処理系を生成し, PL/O+のプログラムを実行してみて,この仕様のテストを行い,仕様の妥当性を確認している.第4章および第5章では,代数的仕様記述法を確立する目的の一つであるプログラム検証について考察する.第4章では,プログラム検証法としてよく知られているホーア流の公理的検証体系と代数的意味論との関係を明らかにする.そのために,代数的意味論に対する公理的検証体系の健全性について考察する.具体的には,WHILE プログラムを記述する簡単な言語WLに対して,代数的意味論に関する公理的検証体系の健全性を示す.これにより,代数的意味論と公理的検証体系の間に矛盾のないこと,代数的意味論の与えられたプログラミング言語で書かれたプログラムの検証に公理的検証体系を用いてよいことがわかる.また,すでに広く認められているホーア流の公理的検証体系との無矛盾性は,代数的仕様の正しさを相対的に保証する.同種の研究としては,表示的意味論と公理的検証体系の関係を明らかにしたものとして,Donahueの研究がある. Donahueは,PascalサブセットのScott 流の表示的意味論を与え,公理的検証体系の表示的意味論に対する健全性を証明し,両者の間に矛盾がないことを示している.また,ホーア流の公理的検証体系の健全性と完全性の研究については,Cookの研究がよく知られている.Cookはプログラミング言語の意味論としては,関数的意味論を用いて,公理的検証体系の健全性と完全性の証明を行なっている.これらの研究と異なり,代数的意味論に対する公理的検証体系の健全性の証明を行なったことが本論文の特徴である.第5章では,代数的意味論の枠組の中でプログラムの正当性検証を行うための基本的な考え方について述べる.即ち,プログラムの意味を入力から出力ヘの関数と考えたプログラミング言語の代数的仕様記述法,ならびに,プログラムの機能の代数的仕様記述法を与え,それに基づいてプログラムの正当性の定義を与える.言語の代数的意味論を基礎にしているため,検証の(半)自動化に項書き換え系を直接利用できる.プログラムの検証とは,直観的に言えば,プログラムPとそれが満たすべき仕様Sが与えられたとき, Pが確かにSを満たすことを証明することである.しかし,このままでは具体的に何をしたら良いのか分からない.形式的なプログラム検証のためには,『プログラムが仕様を満たす』ということの妥当でかつ厳密な定式化が必要である.この定式化は次の3項目の定義によってなされる.(1)プログラムの実行によって達成される機能(プログラムの意味)(2)プログラム仕様の表す機能(プログラムの仕様の意味)(3)プログラム仕様に対するプログラムの正当性(1)は,プログラミング言語の形式的意味論を与えることで定義される.(2)は,(1)と同様に,プログラム仕様の記述言語の形式的意味論を与えることで定められる.(3)は,プログラムの意味する機能がプログラム仕様の意味する機能を満たすことの定義である. これらの定義が定まれば,与えられたプログラムと仕様に対してプログラム検証をするには何をすれば良いのかが明確となる.ここで重要なことは,(3)の妥当な定義のためには,(1)と(2)が同じ枠組の中で定義されなければならないことである.本章では,プログラム検証を念頭においた場合の(1),(2)の代数的な定義手法,および,(3)の一つの妥当な定式化を提案し,プログラムの代数的な検証法の基礎を明確にする,代数的枠組を用いることの結果として,｢プログラムの意味ばかりでなく,意図する機能も抽象データ型として仕様記述することとなり,抽象データ型の検証手法,特に,項書き換え系を利用した技法がそのままプログラム検証に応用できる.このことは,本章のプログラム検証の形式化の最も大きな特徴である.最後に付録として,第3章で代数的仕様記述の説明に用いたプログラミング言語PL/O+の全仕様を載せる.","subitem_description_language":"ja","subitem_description_type":"Abstract"}]},"item_12_description_5":{"attribute_name":"内容記述","attribute_value_mlt":[{"subitem_description":"名古屋大学博士学位論文 学位の種類:工学博士 (課程) 学位授与年月日:平成1年7月5日","subitem_description_language":"ja","subitem_description_type":"Other"}]},"item_12_dissertation_number_65":{"attribute_name":"学位授与番号","attribute_value_mlt":[{"subitem_dissertationnumber":"甲第2235号"}]},"item_12_identifier_60":{"attribute_name":"URI","attribute_value_mlt":[{"subitem_identifier_type":"HDL","subitem_identifier_uri":"http://hdl.handle.net/2237/11464"}]},"item_12_select_15":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_select_item":"publisher"}]},"item_12_text_14":{"attribute_name":"フォーマット","attribute_value_mlt":[{"subitem_text_value":"application/pdf"},{"subitem_text_value":"application/pdf"}]},"item_12_text_63":{"attribute_name":"学位授与年度","attribute_value_mlt":[{"subitem_text_value":"1989"}]},"item_access_right":{"attribute_name":"アクセス権","attribute_value_mlt":[{"subitem_access_right":"open access","subitem_access_right_uri":"http://purl.org/coar/access_right/c_abf2"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"北, 英彦","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"29303","nameIdentifierScheme":"WEKO"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2018-02-20"}],"displaytype":"detail","filename":"ko2235-1.pdf","filesize":[{"value":"371.0 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"ko2235-1.pdf 要旨","objectType":"abstract","url":"https://nagoya.repo.nii.ac.jp/record/9666/files/ko2235-1.pdf"},"version_id":"5275b5a0-d06e-49c9-b66f-b194b61e6f6e"},{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2018-02-20"}],"displaytype":"detail","filename":"ko2235.pdf","filesize":[{"value":"4.8 MB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"ko2235.pdf 本文","objectType":"fulltext","url":"https://nagoya.repo.nii.ac.jp/record/9666/files/ko2235.pdf"},"version_id":"fc30e212-4c8f-4cbe-b75a-9657413c6953"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"doctoral thesis","resourceuri":"http://purl.org/coar/resource_type/c_db06"}]},"item_title":"代数的手法に基づくプログラミング言語の仕様記述法とプログラム検証に関する研究","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"代数的手法に基づくプログラミング言語の仕様記述法とプログラム検証に関する研究","subitem_title_language":"ja"}]},"item_type_id":"12","owner":"1","path":["607"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2009-04-15"},"publish_date":"2009-04-15","publish_status":"0","recid":"9666","relation_version_is_last":true,"title":["代数的手法に基づくプログラミング言語の仕様記述法とプログラム検証に関する研究"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-16T03:55:07.631721+00:00"}