Research on software contracts for highly interoperable software modules

高度互操作软件模块的软件契约研究

基本信息

批准号：
20H00582
负责人：
五十嵐淳
金额：
$ 28.45万
依托单位：
Kyoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (A)
财政年份：
2020
资助国家：
日本
起止时间：
2020-04-01 至 2025-03-31
项目状态：
未结题

项目摘要

【研究項目1. モジュール間のデータ変換機構とその自動化の研究】前年度から行っているレコードとハッシュテーブルが相互運用な可能な言語の研究を進め，基本的な機能をSML#コンパイラ上に実装することができ，この成果について国内研究集会で論文発表を行った．一方で，SML#に実装されているOhoriの多相レコード計算の制限から再帰的データ構造の取り扱いに当初想定していなかった問題があること，ならびにコンパイラ内での中間処理に起因する制限から，ある種類のプログラムについてはうまくコンパイルできないことが判明した．前者について，解決の方策は既に得られているが理論的な問題がないことを確認する必要がある．後者については純粋にエンジニアリング的な問題であり時間をかければ解決可能であると見込んでいる．一般的なデータ変換の自動化機構については関連研究のサーベイなどを行った．また、関連して、LLVM IR からスマートコントラクト言語Michelsonへのコンパイル方式の研究を行った。これは多言語モジュールでスマートコントラクトを記述することにも繋がる。【研究項目2. 多言語モジュールで構成されたソフトウェアシステムの検証機構】交付申請書であげた(項目2-1)については，項目1のデータ変換自動化機構とも密接に関連することもあり，関連研究のサーベイに費した．(項目2-2)の多相型を持つ言語と動的型付言語間の相互運用を行うための実行検査については，前年度までの空間効率のよい実装の不可能性の理論的結果に基づき，不可能性がパラメータ性を実行時に保証するために使われている名前生成機構のみに因ることを理論的に示した．具体的には，空間効率の指標となるサイズ関数の定義を，連続したコアーションについてはサイズを定数と見做すことにすれば，空間効率がよいと見做せることを証明した．

[研究项目1.模块之间的数据转换机制及其自动化的研究] 我们从去年开始就一直在研究一种允许记录和哈希表之间互操作的语言，并在SML#编译器上实现了基本功能。在国内的一个研究会议上就此成果做论文报告。另一方面，由于Ohori在SML#中实现的多态记录计算的局限性，在处理递归数据结构时出现了一些意想不到的问题，以及由于编译器内部的中间处理而导致的某些类型的程序的限制。编译不好。对于前者，虽然已经得到了解决方案，但还需要确认理论上不存在问题。后者是一个纯粹的工程问题，我们希望随着时间的推移它可以得到解决。我们对通用数据转换自动化机制的相关研究进行了调查。此外，我们还研究了从LLVM IR到智能合约语言Michelson的编译方法。这也导致了用多语言模块编写智能合约。 [研究项目2.由多语言模块组成的软件系统的验证机制] 关于拨款申请中提到的(项目2-1)，它也与项目1中的数据转换自动化机制密切相关，因此花费了研究调查。（第2-2项）关于多态类型语言和动态类型语言之间的互操作性的执行检查，基于前一年关于空间高效实现的不可能性的理论结果，我们从理论上证明了不可能性仅是由于用于保证运行时参数性的名称生成机制所致。具体来说，我们证明，如果通过将大小视为连续联盟的常数来定义作为空间效率指标的大小函数，则可以认为空间效率良好。