4 0 0 0 OA Featherweight Javaのための漸進的型付け
- 著者
- 伊奈 林太郎 五十嵐 淳
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.26, no.2, pp.2_18-2_40, 2009-04-24 (Released:2009-06-24)
静的型システムと動的型システムの両者の利点を活かす枠組みとして,SiekとTahaは漸進的型付けを提唱している.漸進的型付けでは,型宣言された部分のみ静的型検査が行なわれ,残りの部分については実行時検査が行なわれる.これにより,当初型を付けずに書いたプログラムに型宣言を徐々に付加し,静的型付けされたプログラムを完成させることができる.本研究では,漸進的型付けをクラスに基づくオブジェクト指向言語で実現する理論的基盤として,Igarashi, Pierce, Wadlerらの計算体系Featherweight Java (FJ)に動的型を導入した体系FJ?を定義し,型付け規則を与える.さらにFJ?からFJにリフレクションを加えた体系への変換を定義することで意味論を与え,静的に検査した部分の安全性が保証されることを示す.
4 0 0 0 IR 現代ヨガが心疾患・肥満・乳がんサバイバーに与える効果─文献レビュー─
- 著者
- 久木元 由紀子 藤重 仁子 外村 晴美 五十嵐 淳介 前田 薫
- 出版者
- 森ノ宮医療大学 紀要編集部会
- 雑誌
- 森ノ宮医療大学紀要 = Bulletin of Morinomiya University of Medical Sciences
- 巻号頁・発行日
- no.13, pp.1-14, 2019-03-20
現在欧米で一般的に実践されている現代ヨガは、アーサナと呼ばれる身体的ポーズに力点をおいたもので、それに体の姿勢、呼吸法、そして瞑想を組み合わせた健康やフィットネスを目的とするエクササイズであり、また補完代替医療(Complementary and Alternative Medicine:CAM)の一療法とも位置づけされるのが一般的になっている。その医学的有効性についての期待も高まっていることから、本研究では、現代ヨガと補完医療における位置付けについて、心疾患・肥満・乳がんの医学的有効性について、エビデンスをレビューしたので紹介する。結果として、ヨガによって生活習慣を改善すると心疾患のリスク因子を低減できる可能性が高いこと、過体重者ではヨガの定期的な実施と体重増加の緩和が関連していること、乳がんサバイバーにおいて不安・うつ・QOLにおいて効果があることなどが示唆された。しかし、それらの効果が運動そのものによる効果なのかヨガに特異的な効果なのかについては明らかにされていないため、今後のさらなる検証を期待したい。
4 0 0 0 Featherweight Java のための漸進的型付け
- 著者
- 伊奈 林太郎 五十嵐 淳
- 出版者
- Japan Society for Software Science and Technology
- 雑誌
- コンピュータソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.26, no.2, pp.18-40, 2009-04-24
静的型システムと動的型システムの両者の利点を活かす枠組みとして,SiekとTahaは漸進的型付けを提唱している.漸進的型付けでは,型宣言された部分のみ静的型検査が行なわれ,残りの部分については実行時検査が行なわれる.これにより,当初型を付けずに書いたプログラムに型宣言を徐々に付加し,静的型付けされたプログラムを完成させることができる.本研究では,漸進的型付けをクラスに基づくオブジェクト指向言語で実現する理論的基盤として,Igarashi, Pierce, Wadlerらの計算体系Featherweight Java (FJ)に動的型を導入した体系FJ<SUP>?</SUP>を定義し,型付け規則を与える.さらにFJ<SUP>?</SUP>からFJにリフレクションを加えた体系への変換を定義することで意味論を与え,静的に検査した部分の安全性が保証されることを示す.
2 0 0 0 疑似線形型システムに基づくメモリ管理とプログラム最適化
本研究の目的は,本研究代表者が提唱した疑似線形型システムに基づく新しいメモリ管理方式の実現により,プログラミング言語処理系のメモリ管理の信頼性および効率を改善することであった.主要な成果は以下のとおり.・擬似線形型システムに基づく型推論によるメモリの獲得・解放命令の挿入…擬似線形型システムに基づき,プログラム中で用いられる各データが最後に使用される箇所を特定し,その部分にメモリの解放命令を挿入するための方法を確立し,関数型言語MLを対象としてプロトタイプシステムを構築した.・擬似線形型システムに基づくメモリ管理のためのバイトコード言語の設計と実装…上で述べたメモリの獲得・解放命令を挿入したプログラムを実際に実行するためのバイトコード言語を設計し,実装を行った.・通常のメモリ管理の改良と本メモリ管理方式との融合…擬似線形型システムのみでは自動的に管理できないメモリが存在するため,既存のメモリ管理方式であるGCを改良して融合する方法について研究した.主な課題はGC自体の性能,特に並列計算機上のGCの性能をあげること,および疑似線形型に基づくメモリ管理によるダングリングポインタの問題の解決であった.後者については型情報を実行時まで保存し,GC時にこれを用いることによってこの問題を解決した.・線形型解析の資源使用解析への一般化…疑似線形型を拡張し,ファイルやネットワークなど一般の計算資源の使用方法の解析を行うための型システムを構築した.これにより(i)割り当てられたメモリはいずれ解放され,解放後はアクセスされない,(ii)オープンされたファイルはいずれクローズされ,クローズ後は読み書きされない,といった性質が満たされているかを統一的に検証することができる.
1 0 0 0 OA AI時代を見据えたプログラム検証技術
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものである。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、(1)代表者らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、(2)プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに(3)機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指す。
Java 1.5ではJava言語の導入以来初めての大きな言語仕様の変更が行われる。そのうちの主要なものとして総称クラス(generic class)・ワイルドカード型の導入が挙げられる。総称クラスとは、C++言語のテンプレートのような、型パラメータにより抽象化されたクラス定義のことであり、ベクトル・木・リストなどの汎用データ構造のプログラミングにおいて有用である。総称クラスはML、Haskellなどの型付き関数型言語でみられる多相的型付けを応用した機構であるが、最近の筆者らによる研究において、(型付き)オブジェクト指向言語において伝統的である、部分型多相との新しい融合手法が考案されている。ワイルドカード型は、この手法に基づき導入された機構である。本稿では、型システムの改良が、いかに言語の柔軟性を損なうことなく、プログラムの安全性の向上に貢献できるかという例として、これらの機構を概観する。"
1 0 0 0 OA 高階モデル検査の深化と発展
本課題では、高階モデル検査の(1)理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、(2)プログラム検証への応用、(3)高階モデル検査の拡張とそのプログラム検証への応用、(4)データ圧縮への応用、の4つを柱に研究を進めている。以下、それぞれの項目について、平成28年度(およびその繰越として遂行した平成29年度の一部の結果)について述べる。(1)理論的基盤の強化:HORSモデル検査とHFLモデル検査という2種類の高階モデル検査の間に相互変換が存在することを示すとともに、HFLモデル検査問題を型推論問題に帰着できることを示した。後者の結果に基づき、HFLモデル検査器のプロトタイプを作成した。また、高階文法の性質について調べ、語を生成するオーダーnの文法と木文法を生成するオーダーn-1の文法と間の対応関係を示した。さらに、高階モデル検査アルゴリズムの改良を行い、値呼びプログラムに対して直接的に高階モデル検査を適用する手法を考案、実装した。(2)プログラム検証への応用:プログラム検証で扱える対象プログラムや性質の拡充を行い、関数型プログラムの公平非停止性の検証、コード生成プログラムの検証、動的なスレッド生成を伴う高階並列プログラムの検証、などを可能にした。(3)拡張高階モデル検査:HORSに再帰型を加えて拡張したμHORSに対するモデル検査アルゴリズムの改良を行い、その有効性をJavaプログラムの検証を通して示した。(4)データ圧縮への応用:データをそれを生成する関数型プログラムの形に圧縮する方式(高階圧縮)について、圧縮後のプログラムをビット列に変換する部分の改良を行った。また、高階圧縮のための様々な要素技術について研究を進めた。
- 著者
- 岩間 太 五十嵐 淳 小林 直樹
- 出版者
- 一般社団法人情報処理学会
- 雑誌
- 情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
- 巻号頁・発行日
- vol.48, no.4, pp.48-61, 2007-03-15
ファイルやメモリなどの計算資源がプログラム中でどのように使用されるかを型を用いて推論するための手法が五十嵐,小林らにより提案されている.彼らの手法では,各計算資源に対して起こりうるアクセス列の集合を使用法表現と呼ばれる式として推論する.しかしながら,推論された使用法表現が表すアクセス列の集合が,仕様として許されるアクセス列からなる言語に包含されているかどうかを判定するアルゴリズムが考案されておらず, 計算資源使用法検証の完全な自動化は達成できていなかった.本論文では,ある特定の言語クラスに属する仕様に対し,そのような包含判定を行うための健全かつ完全なアルゴリズムを提案する.仕様として任意の正則言語を許す場合には,包含判定問題は決定不能なので,我々のアルゴリズムが扱う仕様のクラスは,1つの入力記号について,遷移元および遷移先の状態がたかだか1つしか存在しない有限オートマトンが受理する言語のクラスとして与えられ,正則言語のクラスより小さい.しかしながら,ファイルなど現実の計算資源の仕様の多くは,我々のアルゴリズムで扱える言語のクラスに属する.したがって,本論文のアルゴリズムを五十嵐と小林らによる従来の研究と組み合わせることにより,ファイルなど多くの計算資源の使用法検証を自動化できる.In our previous work, we have developed a type-based method for inferring how resources such as files and memory are accessed in a program. Due to the lack of an algorithm for deciding whether the inferred resource usage conforms to the specification, however, it was not possible to verify automatically that resources are accessed according to the specification. In this paper, we propose a sound and complete algorithm for deciding the conformance of the inferred resource usage to the specification. Since the language denoted by the inferred resource usage belongs to a class larger than the class of the context-free languages, the class of specifications that our algorithm can deal with is smaller than the class of regular languages. Fortunately, however, that language class contains many of the typical resource usage specifications used in practice. Thus, by combining our algorithm with our previous method for resource usage inference, we can automatically check whether each resource is accessed according to the specification in many cases.