(57)【要約】【課題】ユーザプログラムにおいて制約が守られているか否かを容易に判定できるようにする。【解決手段】情報処理装置１は、制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定する情報処理装置であって、アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせをライブラリ２から探索する探索手段３と、探索手段３が単一の関数または複数の関数の組み合わせを発見できた場合に、アプリケーションプログラムが制約を充足していると判定する充足判定手段４とを備えている。【選択図】図６
2018169693.tif 000002
【特許請求の範囲】
【請求項１】
制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定する情報処理装置であって、
前記アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせを前記ライブラリから探索する探索手段と、
前記探索手段が前記単一の関数または複数の関数の組み合わせを発見できた場合に、前記アプリケーションプログラムが制約を充足していると判定する充足判定手段と
を備えたことを特徴とする情報処理装置。
【請求項２】
ライブラリは、関数の入力に係る制約が型構造で定義され、制約を充足する値が型生成関数として定義されたライブラリプログラムを含む
請求項１記載の情報処理装置。
【請求項３】
ライブラリプログラムは、再帰的構造を有する型生成関数を用いて制約充足の条件が定められたプログラムである
請求項２記載の情報処理装置。
【請求項４】
探索手段は、使用されない変数を除去しつつ、単一の関数または複数の関数の組み合わせを探索する
請求項１から請求項３のうちのいずれか１項に記載の情報処理装置。
【請求項５】
制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定する情報処理方法であって、
前記アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせを前記ライブラリから探索し、
前記単一の関数または複数の関数の組み合わせを発見できた場合に、前記アプリケーションプログラムが制約を充足していると判定する
ことを特徴とする情報処理方法。
【請求項６】
ライブラリは、関数の入力に係る制約が型構造で定義され、制約を充足する値が型生成関数として定義されたライブラリプログラムを含む
請求項５記載の情報処理方法。
【請求項７】
ライブラリプログラムは、再帰的構造を有する型生成関数を用いて制約充足の条件が定められたプログラムである
請求項６記載の情報処理方法。
【請求項８】
使用されない変数を除去しつつ、単一の関数または複数の関数の組み合わせを探索する
請求項５から請求項７のうちのいずれか１項に記載の情報処理方法。
【請求項９】
制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定するための情報処理プログラムであって、
コンピュータに、
前記アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせを前記ライブラリから探索する処理と、
前記単一の関数または複数の関数の組み合わせを発見できた場合に、前記アプリケーションプログラムが制約を充足していると判定する処理と
を実行させるための情報処理プログラム。
【請求項１０】
ライブラリは、関数の入力に係る制約が型構造で定義され、制約を充足する値が型生成関数として定義されたライブラリプログラムを含む
請求項９記載の情報処理プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、制約を型として扱う情報処理装置、情報処理方法および情報処理プログラムに関する。
【背景技術】
【０００２】
企業等で使用される一般的な業務システムと比較すると、ＩｏＴ（Internet of Things）システムでは、より広範な知見が求められることが多くなる。例えば、物理層では、デバイスに関する制約に関する知見が求められる。無線通信が必要とされる場合には、通信方式に関する知見が求められる。さらに、収集したデータを効率よく保存するための知見、データ処理のためのシステム設計に関する知見、および、大量のデータを処理するためのビッグデータ処理に関する知見などが求められる。また、設計に必要な知見に加え、プライバシや肖像権の保護等の法規制など、運用方面での知見もシステムの開発時に要求される。
【０００３】
特許文献１に、複数人または複数組織から知識を収集して、ソフトウェアライブラリ（ライブラリ）にライブラリ化する技術が記載されている。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開平１１−１８４８７４号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
一人の開発者が広範な知見を有していることはまれである。現実には、各領域の知見を有する人材を集め、それぞれが知見を出しあうことが想定される。ある領域において深い知識を有する人材は限定されるので、同時に異なる複数のプロジェクトへの参画が求められることが多い。彼らの主な業務は、設計のレビュー、試験、会議への出席、問合せへの対応等である。プロジェクトが増加すると、システム開発者は調達可能であっても、ある領域において深い知識を有する人材を確保することが難しくなる。人材の確保の困難性は、ビジネス上のボトルネックになる可能性がある。
【０００６】
そこで、特許文献１に記載されているように、収集した知識を、再利用可能にライブラリ化することが得策である。
【０００７】
一般に、ライブラリにおいて、汎用化された処理が記述され、ライブラリを呼び出すことによって、汎用的な処理を再現することが可能である。また、必要に応じて、使用上の制約を汎用的なテストコードとしてライブラリ化されることもある。その場合、ユーザプログラム側でテストコードを呼び出すコードが記述されることによって、テストコードの呼び出し箇所において、制約を充足するか否かの試験が可能になる。
【０００８】
しかし、そのような方法では、テスト呼び出し箇所でしか検査を実施することができない。例えば、ユーザプログラムＡがライブラリプログラムＢを呼び出し、さらにライブラリプログラムＢに付随するテストを呼び出しても、検査によって保証されるのは実行コンテクスト上のライブラリプログラムＢの正しさである。すなわち、ユーザプログラムＡから適切にライブラリプログラムＢを呼び出しているという保証はできない。つまり、使用上の制約が守られているか否かの判定が実行されているわけではない。
【０００９】
本発明は、ユーザプログラムにおいて制約が守られているか否かを容易に判定できるようにすることを目的とする。
【課題を解決するための手段】
【００１０】
本発明による情報処理装置は、制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定する情報処理装置であって、アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせをライブラリから探索する探索手段と、探索手段が単一の関数または複数の関数の組み合わせを発見できた場合に、アプリケーションプログラムが制約を充足していると判定する充足判定手段とを備えたことを特徴とする。
【００１１】
本発明による情報処理方法は、制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定する情報処理方法であって、アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせをライブラリから探索し、単一の関数または複数の関数の組み合わせを発見できた場合に、アプリケーションプログラムが制約を充足していると判定することを特徴とする。
【００１２】
本発明による情報処理プログラムは、制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定するための情報処理プログラムであって、コンピュータに、アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせをライブラリから探索する処理と、単一の関数または複数の関数の組み合わせを発見できた場合に、アプリケーションプログラムが制約を充足していると判定する処理とを実行させることを特徴とする。
【発明の効果】
【００１３】
本発明によれば、ユーザのアプリケーションプログラムにおいて制約が守られているか否かを容易に判定できるようにすることができる。
【図面の簡単な説明】
【００１４】
【図１】情報処理装置の実施形態を示すブロック図である。
【図２】情報処理装置の動作を説明するためのフローチャートである。
【図３】アプリケーションソースコードの一例を示す説明図である。
【図４】ライブラリプログラムの一例を示す説明図である。
【図５】型ＧＴ１と、型Ｎａｔ、型Ｏおよび型Ｓとの関係を示す説明図である。
【図６】本発明による情報処理装置の主要部を示すブロック図である。
【発明を実施するための形態】
【００１５】
実施形態１．
以下、本発明の実施形態を図面を参照して説明する。
【００１６】
図１は、情報処理装置の実施形態を示すブロック図である。図１に示す情報処理装置１０は、ライブラリ１００、型構造抽出装置１０１、型構築関数抽出装置１０２、および型構築関数探索装置１０３を含む。アプリケーションソースコード２００は、例えば、ライブラリ１００を利用するユーザのパーソナルコンピュータ等の端末に存在する。
【００１７】
ライブラリ１００には、複数人または複数組織から収集された知識に関するデータが、ソフトウェアライブラリとして格納されている。また、ライブラリ１００には、制約が型として記述されているライブラリプログラムが含まれている。
【００１８】
型構造抽出装置１０１は、入力されたアプリケーションソースコード２００とライブラリ１００の内容を読み取り、型定義を抽出し、型構造を示す情報（型構造情報）を取得する。型構造情報は、有向グラフの構造になる。
【００１９】
型構築関数抽出装置１０２は、アプリケーションソースコード２００とライブラリ１００の内容を読み取り、関数の入出力関係を分析して、型構築関数の関係を抽出する。型構築関数も、有向グラフの構造になる。
【００２０】
型構築関数探索装置１０３は、アプリケーションソースコード２００と得られた型構造情報および型構築関数との関係を用いて、アプリケーションソースコードで記述されている関数呼び出しに必要となる型を構築する単一の関数または複数の関数の接続構造を探索する。型構築関数探索装置１０３は、探索の結果として、必要となる単一の関数または複数の関数の接続関係を出力する。
【００２１】
型構築関数探索装置１０３は、型構造抽出装置１０１によって抽出された型構造に対して、型構築関数抽出装置１０２によって得られた型構築関数の関係を用いて、アプリケーションソースコード中に含まれる関数の呼び出し対象の型を生成するのに必要な関数を探索する。制約は型としてライブラリ１００において記述されているので、型構築関数探索装置１０３は、当該型を生成する関数を発見することが可能である。
【００２２】
型構造抽出装置１０１、型構築関数抽出装置１０２、および型構築関数探索装置１０３は、プログラム記憶部に格納されたプログラムにもとづいてＣＰＵ（Central Processing Unit ）が処理を実行することによって実現可能である。
【００２３】
次に、情報処理装置１０の動作を説明する。図２は、情報処理装置１０の動作を説明するためのフローチャートである。
【００２４】
型構造抽出装置１０１は、ステップＳ２０１の型識別子抽出処理で、ユーザの端末等から入力されたアプリケーションソースコード２００およびライブラリ１００の内容のそれぞれを分析し、型識別子を抽出する。また、型構造抽出装置１０１は、ステップＳ２０２の型関係抽出処理で、型識別子抽出処理で得られた型識別子が示すそれぞれの型の親子関係およびパラメータ関係を抽出する。
【００２５】
型構築関数抽出装置１０２は、ステップＳ２１１の関数識別子抽出処理で、入力されたアプリケーションソースコード２００およびライブラリ１００の内容を対象として、関数を走査し、関数の識別子を抽出する。型構築関数抽出装置１０２は、ステップＳ２１２の関数入出力関係抽出処理で、関数識別子抽出処理で得られた識別子の関数のそれぞれについて、その入出力の対応関係（関数の入出力関係）を抽出する。
【００２６】
型構築関数探索装置１０３は、ステップＳ２２１の型探索空間生成処理で、アプリケーションソースコードおよびライブラリに加えて、ステップＳ２０２の型関係抽出処理で得られた型継承関係（親子関係およびパラメータ関係）とステップＳ２１２の関数入出力関係抽出処理で得られた関数の入出力関係とを基に、目的の型（アプリケーションソースコードで記述されている関数呼び出しに必要となる型）を特定するために探索すべき空間（探索空間）を生成する。
【００２７】
型構築関数探索装置１０３は、ステップＳ２２２の型探索処理で、ステップＳ２２１の型探索空間生成処理で生成された空間にもとづいて、目的の型を生成するために使用すべき単一の関数または関数の組合せ方を探索する。
【００２８】
単一の関数または関数の組合せ方を発見できなかったことは、型として与えられた制約を充足できる関数の組合せを発見できなかったことを意味している。よって、その場合には、すなわち、単一の関数または関数の組合せ方を発見できなかったときには、型構築関数探索装置１０３は、制約違反と判定しエラーを出力する（ステップＳ２２３；Ｎｏ）。
【００２９】
単一の関数または関数の組合せ方を発見できたことは、制約を充足する方法を発見できたことを意味している。その場合には、型構築関数探索装置１０３は、ステップＳ２３１の関数生成処理で、制約を充足する関数を生成して出力する。
【００３０】
次に、情報処理装置１０の動作を具体例について説明する。
【００３１】
図３は、アプリケーションソースコードの一例を示す説明図である。図３に例示するアプリケーションソースコード２００ａは、引数であるS[S[S[O]]]に対して、ライブラリ１００に存在するライブラリプログラムにおけるisGreaterThan1という関数により真偽値を用いて判定するコードである。
【００３２】
図４は、ライブラリの内容（ライブラリプログラム）の一例を示す説明図である。図４に示す例では、関数の定義および当該関数の入力に係る制約が型構造で定義され（１２行目）、制約を充足する値が型生成関数（９〜１０行目）として定義されている。また、後述するように、ライブラリプログラムは、再帰的構造を有する型生成関数を用いて制約充足の条件が定められたプログラムである。
【００３３】
具体的には、図４に例示するライブラリプログラム１００ａにおいて、１２行目に、関数isGreaterThan1が定義されている。そして、関数isGreaterThan1についてライブラリ１００において与えられている制約として、GT1[K]が存在する。アプリケーションソースコード２００ａには、この制約を充足することが求められる。
【００３４】
より具体的には、関数isGreaterThan1において、第１引数であるＫが１より大きいことを制約とすることが表現されている。そして、この制約が充足されない場合に、コンパイル時に確実にエラーを発行することが要請される。
【００３５】
情報処理装置１０において、型構造抽出装置１０１は、ステップＳ２０１の型識別子抽出処理で、アプリケーションソースコード２００ａおよびライブラリプログラム１００ａから、型を抽出する。アプリケーションソースコード２００ａから抽出される型はＳおよびＯである。ライブラリプログラム１００ａから抽出される型はＮａｔ，Ｏ，Ｓ，ＧＴ１の４つである。
【００３６】
型構造抽出装置１０１は、ステップＳ２０２の型関係抽出処理で、型関係を抽出する。ライブラリプログラム１００ａの２行目から、型Ｏは、型Ｎａｔの子であることを抽出できる。そして、型構造抽出装置１０１は、３行目から、型Ｓは型Ｎａｔの子をパラメータとして有する、型Ｎａｔの子であることを抽出できる。また、型構造抽出装置１０１は、５行目から、型ＧＴ１は、型ＮａｔおよびＧＴ１の子クラスである型Ｏおよび型Ｓをパラメータとして有することを抽出できる。
【００３７】
図５は、型ＧＴ１と、型Ｎａｔ、型Ｏおよび型Ｓとの関係（親子関係およびパラメータ関係）を示す説明図である。
【００３８】
型構築関数探索装置１０３は、ステップＳ２２１の型探索空間生成処理で、関数の識別子として、isGreaterThan1、GT1; apply、GT1; twoGT1 、GT1; xGT1 を抽出する。
【００３９】
また、型構造抽出装置１０１は、ステップＳ２１２の関数入出力関係抽出処理で、以下のように、関数の入出力関係を抽出する。
【００４０】
GT1; apply：  (K<:Nat) GT1[K] → GT1[K]  （ライブラリプログラム１００ａの７行目から）
GT1; twoGT1 ：  GT1[S[S[O]]]   （ライブラリプログラム１００ａの９行目から）
GT1; xGT1 ：  (K<:Nat) GT1[K] → GT1[S[K]] （ライブラリプログラム１００ａの１０行目から）
isGreaterThan1：  (K<:Nat) K → GT1[K] → Boolean （ライブラリプログラム１００ａの１２行目から）
【００４１】
型構築関数探索装置１０３は、ステップＳ２２１の型探索空間生成処理で、以上の情報を使用して、探索空間を生成する。ライブラリプログラム１００ａでは、isGreaterThan1[S[S[O]]] が目的の関数であるから、ライブラリプログラム１００ａの１２行目から抽出された関数の入出力関係の"K → GT1[K] → Boolean"のうち、GT1[S[S[O]]]を探索する必要があることが特定される。すなわち、GT1[S[S[O]]]に関する空間が、探索空間として特定される。
【００４２】
具体的には、型構築関数探索装置１０３は、ステップＳ２２２の型探索処理で、型GT1[S[S[O]]]を生成するために使用すべき単一の関数または関数の組合せ方を探索する。以下、型GT1[S[S[O]]]を生成するために使用される関数を条件に適合する関数という。
【００４３】
型構築関数探索装置１０３は、まず、Ｓ２１２の関数入出力関係抽出処理で特定された入出力の対応関係が、条件に適合するか否か判定する(初回の探索)。条件に適合するのはGT1; xGT1 のGT1[K] → GT1[S[K]] である。
【００４４】
ここで、K = S[S[O]] とおけば、xGT1が成立するので、GT1[S[S[O]]]が成立する必要があることがわかる。そのため、型構築関数探索装置１０３は、GT1[S[S[O]]]が成立するか否かを再帰的に判定する (２回目の探索)。ここで、条件に適合するのは、GT1; twoGT1 とGT1; xGT1 である。そこで、型構築関数探索装置１０３は、それぞれについて判定する。
【００４５】
xGT1が条件に適合するには、GT[S[O]]が成立する必要がある。そのために、３回目の探索では、GT[O] が成立する必要があるが、ここで成立しないことが判定される。なぜなら、S[K] = OとなるＫを発見することができないからである。
【００４６】
そのため、２回目の探索としてのGT1; twoGT1 の適合の判定に戻る。ライブラリプログラム１００ａにおいて、twoGT1の関数の入出力関係から引数を取らない、すなわち、前提条件なしにGT1[S[S[O]]が成立すると定義されている。よって、２回目の探索で、twoGT1が条件に適合することがわかる。
【００４７】
型構築関数探索装置１０３は、ステップＳ２３１の関数生成処理で、制約を充足する関数を生成して出力する。この例では、検査が必要であったのは、isGreaterThan1(S[S[S[O]]])(GT1[Ｋ])であった。
【００４８】
そして、初回の探索で条件に適合したのはxGT1である。そこで、isGreaterThan1(S[S[S[O]]])(xGT1[Ｋ'])に変形される。２回目の探索で条件に適合したのは、twoGT1である。よって、さらにisGreaterThan1(S[S[S[O]]])(xGT1[twoGT1])と変形される。
【００４９】
さらに、１２行目のisGreaterThan1の右辺の定義には引数gt（xGT1[twoGT1]に相当する。）が現れていない。よって、isGreaterThan1(S[S[S[O]]])(xGT1[Ｋ'])からxGT1[Ｋ']を除去することができる。すなわち、型構築関数探索装置１０３は、ステップＳ２３１の関数生成処理で、制約を充足する関数として、isGreaterThan1(S[S[S[O]]]) = true を出力する。
【００５０】
次に、アプリケーションソースコード２００ａで、引数が(O) である関数isGreaterThan1(O) が指定された場合を例にして情報処理装置１０の動作を説明する。ステップＳ２０１〜Ｓ２２１の処理は、上記の場合の処理と同じである。
【００５１】
この場合、型構築関数探索装置１０３は、Ｓ２２２の型探索処理で、型GT[O] を探索する。しかし、関数の入出力関係から、型GT[O] を生成するために使用すべき関数を発見することができない。なぜなら、xGT1[K] ではＫに対する減少への再帰を持つが、図４に示すライブラリプログラム１００ａにおいて、０からの減少はNat の定義上存在しないからである。
【００５２】
よって、型構築関数探索装置１０３は、isGreaterThan1(O) という関数呼び出しが含まれるソースコードに対して、制約を充足しないとしてエラーを発行する。
【００５３】
なお、本実施形態では、アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数が発見されたが、複数の関数の組み合わせが発見されることもある。
【００５４】
本実施形態では、ライブラリ１００において、制約が型として定義されている。そして、情報処理装置１０は、その型を充足する関数を探索するために（ステップＳ２２２）、必要になる型の構造を生成するとともに（ステップＳ２０１〜Ｓ２０２）、目的の型を生成するために必要とされる可能性がある関数を抽出する（ステップＳ２１１〜Ｓ２１２）。そして、情報処理装置１０は、探索空間を生成する（ステップＳ２２１）ために、関数の親子関係と関数の入出力関係とを抽出する。その結果、型として定義された制約を充足する関数の有無を検査することができる。
【００５５】
また、本実施形態では、一方の入力であるアプリケーションソースコード側で制約を記述する必要をなくすことができるので、アプリケーションプログラムの作成者に制約に対する知見が要求されなくなる。
【００５６】
また、本実施形態がアプリケーションプログラムのコンパイル時に適用されることによって、コンパイル時にアプリケーションソースコードを検査することができる。そして、制約が型としてライブラリに埋め込まれ、探索によって得られる対応関係（関数の構造の対応関係）にもとづいて、アプリケーションプログラムが制約を充足することを保証することができる。
【００５７】
また、制約は実質的にライブラリ中に隠蔽され、呼び出し側のアプリケーションプログラムでは、制約の情報が不要になる。
【００５８】
以上に説明したように、本実施形態では、アプリケーションソフトウェアに対して、呼び出しに制約が存在する関数の呼び出しにおいて、制約の判定を自動化することができる。
【００５９】
図６は、本発明による情報処理装置の主要部を示すブロック図である。図６に示す情報処理装置１は、制約が型として記述されているライブラリの関数を呼び出すアプリケーションプログラムが制約を充足するか否か判定する装置であって、アプリケーションプログラムの関数呼び出しに必要となる型を構築する単一の関数または複数の関数の組み合わせをライブラリ２から探索する探索手段３（実施形態では、型構築関数探索装置１０３で実現される。）と、探索手段３が単一の関数または複数の関数の組み合わせを発見できた場合に、アプリケーションプログラムが制約を充足していると判定する充足判定手段４（実施形態では、型構築関数探索装置１０３で実現される。）とを備えている。
【符号の説明】
【００６０】
１        情報処理装置
２        ライブラリ
３        探索手段
４        充足判定手段
１０      情報処理装置
１００    ライブラリ
１００ａ  ライブラリプログラム
１０１    型構造抽出装置
１０２    型構築関数抽出装置
１０３    型構築関数探索装置
２００，２００ａ  アプリケーションソースコード
【図１】
2018169693.tif 000003
【図２】
2018169693.tif 000004
【図３】
2018169693.tif 000005
【図４】
2018169693.tif 000006
【図５】
2018169693.tif 000007
【図６】
2018169693.tif 000008