区間遷移システム:複数の環境におけるプログラムの意味の集約

Přispěvatelé: 山田, 俊行
Jazyk: japonština
Rok vydání: 2023
Popis: 様々な計算機やプログラミング言語が日々開発されている．そのため古くなった計算機を新調して移植したりプログラミング言語を変えてこれまでのプログラムを作り変えたりすることがある．そこで，プログラムが正しく動作することやプログラムの最適化，プログラム間の等価性を評価する必要がある．したがって，プログラムを解析することは重要である.遷移システムは各ブロックにおける変数の値を状態とし，変数の値の変化を遷移とする状態遷移を用いて表現することでプログラムを解析する手法であり，トランスパイラの等価性の保証などに用いられる．プログラム解析ではプログラムの流れを解析する制御フロー解析や各ブロックにおける変数の取り得る値の集合を解析するデータフロー解析等があり，プログラムの最適化に用いられる．これらは一つの決まった実行環境に基づいて，プログラ ムやプログラム変換に対して検証することは可能である．しかし，実行環境が増えるほどプログラム解析のための検証器の数は急増し，更に複数の実行環境やプログラミング言語の仕様を必要とするトランスパイラの検証器やプログラム間の検証器は膨大な数が必要となる．これはそれぞれ開発者にとっては開発すべき数が増えてしまうという点で，使用者にとっては使用している計算機やプログラミング言語の仕様の組み合わせに適した検証器を選択が必要な点で負担になる．そこで，複数の仕様を満たしながらプログラムを解析できればこれらの問題は解決できる．数値解析では計算機で実装された値や関数に対し，閉区間とその上の演算を与えることで関数の結果がどの程度の大きさの区間であるか調べることで関数の精度を考察する区間解析がある.本研究では，区間解析の対象を関数からプログラムに拡張し遷移システムの各状態における変数の解釈として閉区間を取ることでプログラム実行後における変数の精度を調べるために，区間論理とその上の区間遷移システムを提案する．先行研究で用いられた論理を用いて各変数の値を閉区間として解釈して遷移システムを構成するだけでは複数の条件分岐を扱えず，各条件分岐においてその条件を満たすような仕様のみを表現する遷移システムを前提としてしまうため不十分である．これはプログラム中に現れる論理代数と遷移システムを構成するために必要な論理に現れる論理代数を同じものとして扱うことに起因する．そのため，それらの論理代数を分けた新たな論理である区間論理を定義し，その上に区間遷移システムの定義を与えることでこの問題を解決する．区間論理は計算機やアーキテクチャやプログラミング言語などの仕様の組みあわせの定式化であり，区間遷移システムはその上のソースコードの定式化である.
三重大学大学院 工学研究科 博士前期課程 情報工学専攻 コンピュータソフトウェア研究室
27p
Databáze: OpenAIRE
Externí odkaz: