担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Atlantis Press  

Computational systems that deal with discrete time, such as stream computations and synchronous data flow languages, can be modeled using lists. However, most list operations are on finite lists, and it is not easy to define them for infinite lists to express persistent behavior. In particular, when using theorem provers, intuitive definitions are unacceptable due to restrictions on the handling of infinities. When integrating computational failures into the system, existing research either directly expresses failures or utilizes a mechanism that continues to send invalid values indefinitely. Still, the latter cannot determine failures in terms of computation. In this study, we formalize a model of a reversible synchronous dataflow language using finite and infinite lists and show that the semantics of each correspond to each other using the Coq theorem prover. For infinite lists, the inconsistency that arises as a result of incorporating failures into the list is resolved using finite lookahead.

DOI： 10.2991/978-94-6463-684-0_2

researchmap

担当区分：最終著者,　責任著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

小規模組込みシステム向けFRP言語XStorm では，状態遷移モデルに基づいて時変値間の関係を動的に変更でき，状態依存動作を簡潔に記述できる． しかし，例えば消費電力削減のため，状態に応じて使用する周辺装置を切替えるといった際に，C言語で書かれた周辺装置のドライバコード内で切替え処理を書く必要があった． その結果，XStormプログラムとドライバコードの間のロジックの不整合が検出できない． 本研究では，XStormの状態遷移モデルを発展させ，状態ごとに周辺装置の電源等の状態(モード)を宣言できるようにすることで，FRP言語内での周辺装置のモードの切替えも含めたロジックの記述を可能にした． これにより前述の問題を解決したほか，ランタイムによるモードの自動管理を行えるようになった．

DOI： 10.11309/jssst.42.1_40

researchmap

担当区分：最終著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Information Processing Society of Japan  

Emfrp is a functional reactive programming (FRP) language for resource-constrained systems such as microcontrollers. The language enables the concise description of reactive behavior specific to embedded systems. The current Emfrp compiler runs on a development host PC. Therefore, the program development, testing, and modification cycle is time-consuming. We have implemented an interpreter, Emfrp-REPL, which runs on the target device and enables interactive and rapid development using the REPL interface. The interpreter is designed to minimize I/O latency and employs snapshot GC to suppress latency fluctuations. However, the execution speed could be faster because the evaluation of expressions is based on AST traversal. In this study, we design and implement Emfrp-VM, a byte code VM for Emfrp, to solve this problem.

researchmap

担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

As IoT devices advance, their microcontroller systems-on-a-chip (SoCs) demand higher speeds, more memory, and advanced peripherals, leading to increased power consumption. Integrating low-power (LP) coprocessors in SoCs can reduce power usage while maintaining responsiveness. However, switching application execution to and from the coprocessors generally involves complex and platform-specific procedures. We propose a JIT compilation method for managed programming languages to streamline LP coprocessor use. Our prototype for the programming language mruby includes a JIT compiler and a seamless processor-switching mechanism, enabling rapid development of IoT applications leveraging LP coprocessors. This work-in-progress paper describes the design and implementation of the extended mruby interpreter and presents preliminary evaluations of its power consumption and latency on ESP32-S3 and ESP32-C6.

DOI： 10.1145/3679007.3685064

researchmap

担当区分：最終著者   記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

関数リアクティブプログラミング（FRP）は，時間と共に変化する値である時変値を宣言的に組み合わせることによってリアクティブシステムを記述するプログラミングパラダイムである． 組込みシステム向けFRP言語であるEvEmfrpは，時変値に対しその更新タイミングを型情報として持たせることで周期的・非周期的なタスク処理を記述することができる． しかし，それぞれの時変値の更新がいつ完了するかといった実時間性に関する保証がなく，リアルタイムシステム向けの言語としては十分ではない． 本研究では，EvEmfrpをもとに，リアルタイムシステムを記述するための構文を備えたFRP言語を提案する． 本言語では，明示的にタスクとそのデッドラインを記述することができ，各タスクでどの時変値が更新されるかを時変値が持つタイミングから静的に決定することができる． また，本言語におけるタスク処理に適したスケジューリング機構を提案する．

researchmap

担当区分：最終著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

プログラムの出力から入力を求めることを逆計算という.本論文では同期的データフロープログラミングにおける逆計算を扱い，特に，順計算と逆計算の両方を逐次的に行えるという性質を保証しながらプログラムを構成する手法について議論する.同期的データフロープログラムは，全ての入力を読み込んで出力を返して停止するのではなく，時間的な列として順に与えられる入力に対して出力を返し続けなければならない.したがってその逆計算の手法は一般的なパラダイムのものと異なる.本論文では同期的データフロープログラミングのパラダイムを列の変換としてモデル化し，それに対する逐次的な逆計算の概念を定義する.さらに，逐次的な逆計算が可能なシステムを単射部分関数を用いて構成する方法を定義することで，逐次的な逆計算のための制約を部分関数の単射性に帰着する.この議論は逐次的な逆計算を保証する同期的データフロー言語の設計の指針になりうる.

DOI： 10.11309/jssst.41.3_34

researchmap

担当区分：最終著者   記述言語：日本語   出版者・発行元：情報処理学会  

Emfrpはマイクロコントローラなどの小規模組込みシステム向けに設計された関数リアクティブプログラミング(FRP)言語であり，組込みシステム特有のリアクティブな動作の簡潔な記述を可能にする． その処理系は開発用のホストマシン上で動作するクロスコンパイラであり，プログラムの修正・テストのサイクルに時間がかかる． そこで我々はターゲットデバイス上で動作し，REPLによる対話的かつ迅速な開発を可能にするインタプリタEmfrp-REPLを実装した． Emfrp-REPLではI/Oレイテンシを低く抑える工夫がなされており，スナップショットGCによってレイテンシの変動を抑制しているが，式の評価がASTの走査によるため実行速度にやや難がある． 本研究ではEmfrpのためのバイトコードVMにもとづく処理系Emfrp-VMを設計・実装し，この問題の解決を図る．

researchmap

担当区分：最終著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

Emfrp, a functional reactive programming (FRP) language for small-scale embedded systems, is a DSL designed for execution in resource-constrained environments.
The execution model of Emfrp provides a reactive behavior of the system through repeated actions such as waiting for inputs from sensors, updating all time-varying values, and outputting them to the actuators.
Such polling-based execution consumes unnecessary energy due to frequent update processing.
For this reason, the extended language EvEmfrp was proposed to reduce unnecessary update processing and improve energy consumption.
EvEmfrp statically determines and schedules the update period of the whole system by annotating the timing of the time-varying value updates and the input interrupts.
Since time-varying value updates are performed at periodic timing, the system is put into sleep mode when no update processing is required, thereby saving energy.
However, because the timing annotations and the update intervals are set statically, executing a program that updates a specified time-varying value after a fixed time starting from an interrupt signal without unnecessary updates is impossible.
This causes frequent wake-up from sleep mode and prevents power saving.
We propose a mechanism for extending timing annotations and dynamically changing the update intervals to solve this problem.
We also show the usefulness of the proposed mechanism through an example of debouncing for button presses.

DOI： 10.1145/3651781.3651789

researchmap

担当区分：最終著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.2991/978-94-6463-388-7_10

researchmap

担当区分：最終著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

For distributed systems in Functional Reactive Programming (FRP), we have been interested in glitch avoidance.
FRP describes systems by dataflow of time-varying values which are abstractions of values that change over time.
A glitch is a kind of inconsistencies between time-varying values due to update timing.
There are several researches for glitch avoidance and/or consistency of the values.
Since distributed systems often assume no global clocks nor locks, the existing methods send many messages to ensure one of these properties.
We propose a multi-party FRP language, named MPFRP.
In MPFRP, we describe some parties of time-varying values for the distributed system.
A party is a dataflow network whose time-varying values are updated consistently each other, but independently with those in other parties.
The concept of parties gives us a flexible scope for ensuring consistency and minimizing messages.

DOI： 10.1145/3631991.3632000

researchmap

担当区分：最終著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：IPSJ  

A low power coprocessor in the microcontroller helps to save total power consumption. While the main processor is in a sleep state, the low power coprocessor can process the inputs and maintain responsiveness. However, inter-processor communication and processor power state management make development more complicated. In this paper, we address this problem by introducing a mechanism to switch a running processor to the functional reactive programming (FRP) language XStorm, which has an abstraction mechanism for modeling stateful behaviors. The proposed mechanism allows us to choose which processor to run in each state. Therefore, the switching of a running processor can be represented as a state transition. Our compiler can absorb differences in processor architectures and automatically generate programs for inter-processor communication and processor state management. As a result, developers can more easily describe system with coprocessors. We describe the proposed mechanism and report an evaluation on the power consumption and time of state transitions.

researchmap

担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

This paper presents mechanisms for describing real-time tasks in functional reactive programming (FRP) languages for small-scale embedded systems. We have designed and implemented Emfrp, an FRP language for resource-constrained systems, and demonstrated its usefulness with several applications. However, the language requires using external clocks as time-varying values when describing time-dependent behaviors. In this work, we extend the types of time-varying values that express their update timings to describe periodic and aperiodic tasks. The extensions enable concise and precise descriptions of various timed behaviors. We evaluate prototype implementations of the extended languages concerning program size, execution time, and power consumption.

DOI： 10.1145/3623506.3623578

researchmap

担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

This paper reports the implementation of Emfrp-REPL, an interactive interpreter (REPL) of a functional reactive programming language for resource-constrained embedded systems. Its goal is to accelerate the prototyping and development of microcontroller-based embedded systems. The interpreter runs on small-scale embedded devices based on 32-bit microcontrollers, such as ESP32 with 520KiB size data RAM. The evaluation shows that the memory usage of Emfrp-REPL is comparable to MicroPython, and the range of its latency is narrower than MicroPython, according to microbenchmarks.

DOI： 10.1145/3594671.3594674

researchmap

担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

Emfrp is a functional reactive programming language designed for small embedded systems. By imposing certain restrictions on the language mechanism, the language guarantees the termination of the update process for each time-varying value and enables static determination of the amount of memory required for execution. This allows Emfrp programs to run safely even in resource-constrained execution environments. However, the abovementioned restrictions make it difficult to write time-consuming operations (heavy tasks) such as graph structure construction and exploration based on external data. Moreover, since Emfrp updates time-varying values synchronously, a naive implementation of such heavy tasks using external function calls will result in a slow response time to input. Some existing programming languages provide asynchronous processing mechanisms to ensure descriptiveness and responsiveness for heavy tasks. In this study, we propose a method to introduce heavy tasks into reactive programs naturally by introducing language mechanisms equivalent to asynchronous processing mechanisms, such as future and promise, into Emfrp. In this paper, we first discuss the problems with a naive implementation of heavy tasks in Emfrp, then explain the proposed method based on an example, and discuss the language runtime implementation.

DOI： 10.1145/3563837.3568338

researchmap

担当区分：最終著者,　責任著者   記述言語：英語  

researchmap

担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Information Processing Sociey of Japan  

We introduce a new type system to Emfrp, a functional reactive programming (FRP) language designed for resource-constrained embedded systems. Functional reactive programming is a programming paradigm that allows concise descriptions of reactive systems such as GUIs by combining time-varying values that express values changing over time. Emfrp is a domain-specific language based on FRP, designed and developed for small-scale embedded systems. Because the language can statically determine the amount of runtime memory and guarantee the termination of reactive actions, a program written in Emfrp can safely continue reactive behaviors in resource-constrained environments. To ensure these properties, Emfrp disallows the use of recursive data types and functions. However, such restrictions often impose unnatural representations of data structures like lists or trees. The declarative characteristic of FRP and these restrictions impel us to write poorly maintainable redundant codes or deter us from writing certain types of programs. In this paper, we propose EmfrpBCT, an extended Emfrp with size-annotated recursive data types, to overcome this problem. The proposed system is more expressive than Emfrp, yet, it retains the aforementioned static properties. After explaining that through examples, we describe the features of EmfrpBCT, formalize the language, present an algorithm for statically computing the runtime memory bounds, and prove its soundness. Moreover, we implemented a compiler from EmfrpBCT to C, measured the translation time, and evaluated runtime overhead.

DOI： 10.2197/ipsjjip.29.685

researchmap

担当区分：責任著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

無線センサーアクターネットワーク(WSAN)は，物理環境に配備された複数個の計算機が相互に通信することで，物理環境の観測や環境への働きかけを行う分散システムである．その実現には，センサーノードに加えて環境への働きかけなどを行うアクターノードを含む複雑なノード間協調が必要である．ノード間協調が不十分な場合，センサーやアクターへのメッセージの到達順序が入れ替わり，実行順序が意図しないものになるハザードと呼ばれる問題が発生することがある．アクターノードを含まない無線センサーネットワーク(WSN)については，マクロプログラミングと呼ばれる，WSN全体を1つの計算システムとみなしてその動作を記述する手法がある．マクロプログラミングでは処理に用いるノード間協調を全体の動作から導出する．本研究では，ハザード回避を行う協調動作を導出する機構を取り入れたWSAN向けのマクロプログラミング言語を提案する．

researchmap

担当区分：筆頭著者,　責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：IPSJ  

Functional reactive programming (FRP) is a programming paradigm where a system is described using declarative abstractions of the change propagation of discrete events and continuous signals. This paper presents a purely functional reactive programming model that facilitates a uniform description of distributed coordination and per-node computation. A case study of a wireless sensor-actor network (WSAN) shows that both inter-node coordination and intra-node computation can uniformly be written as reactive behaviors. The paper also describes an implementation method of the model using Distributed XFRP, a pure FRP language for distributed systems.

researchmap

担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

We propose new functionality for FRP language to support computations on GPUs. Some embedded systems equip GPUs, which enable us to process large amounts of data such as camera images. We have developed an FRP language for embedded systems, named Emfrp. However, Emfrp lacks two kinds of concepts for computations on GPUs; one is the representation for large amounts of data, and the other is the declaration of the calculational resources of computations. In this paper, we introduce node arrays and GPU nodes, which are time-varying values computed on GPUs. We also show a prototype language of these features and evaluation through some examples on it.

DOI： 10.1145/3457784.3457795

researchmap

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

researchmap

担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

researchmap

担当区分：最終著者,　責任著者   記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）   出版者・発行元：情報処理学会  

関数リアクティブプログラミング (FRP) は，時間とともに変化する値（時変値）間の依存関係を副作用のない式で表すことで，リアクティブな動作の宣言的な記述を支援するプログラミングパラダイムである．本研究では，組込みシステム向けに設計されたFRP言語LRFRPを提案する．LRFRPはプログラミング言語Rust上の内部DSLであり，Rustのマクロ機能を用いて実装されている．Rustプログラム中に埋め込まれたLRFRPのプログラムは，コンパイル時にRustのモジュールに変換される．このモジュールは極めて限られたライブラリにのみ依存し，またRustの機能を制限しない．そのため，組込みシステムをターゲットとする場合など，利用できるライブラリが限定された状況でも動作可能である．本稿ではLRFRPの概要と実装方式について述べ，例を通してその有効性について議論する．

CiNii Research

researchmap

担当区分：最終著者,　責任著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：情報処理学会  

組込みシステムは，外部からの入力に対して自身の状態を更新しながら応答を続けるリアクティブシステムの典型例である．組込みシステムの多くは状態遷移を含み，状態に応じて振舞いを変化させる必要があるためプログラムが複雑になる．本研究では，小規模組込みシステムを対象とした関数リアクティブプログラミング（FRP）言語であるEmfrpに対し，システムの状態に応じて計算の動的な切替えを行うための抽象化機構を導入するswitch拡張を提案する．本拡張は状態ごとに時変値と次に遷移する状態の計算を記述するための機構を提供し，FRPの枠組みの中で状態遷移を扱うことを可能にする．これによって状態遷移を含むリアクティブシステムを宣言的に記述することができる．小規模組込みシステムの開発はマイクロコントローラなどの計算資源が限られた環境を対象としている．このような環境ではリソースの不足による実行時エラーを防ぐため静的にメモリ消費量を見積もる必要がある．提案する手法では遷移する状態の集合を静的に限定し，動的なメモリの確保を行うことなく実行時の計算の切替えを実現させている．switch拡張の処理系は純粋なEmfrpへの変換器として実装されている．提案する拡張によって，状態に応じて振舞いが動的に変化するコンポーネントの記述が容易になることを例を通して示す．

researchmap

その他リンク： https://www.psg.c.titech.ac.jp/posts/2020-04-27-IPSJPRO.html

担当区分：最終著者,　責任著者   記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

関数リアクティブプログラミング(FRP)言語Emfrpに対する再帰的なデータ型の導入手法を提案する． Emfrpはマイクロコントローラのような小規模システム向けに設計された純粋FRP言語である． この言語では，関数やデータ型の再帰的な定義を禁止する等の言語的制約を課すことで， 時変値の更新処理が停止することや実行時に必要なメモリサイズを静的に決定できることが保証される． 本研究では型に対してサイズの情報を含めることで，Emfrpの性質を維持しつつこの制約を緩和する手法を提案する．

researchmap

担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：論文集(書籍)内論文   出版者・発行元：Springer International Publishing  

This paper presents a functional reactive embedded domain-specific language (EDSL) for resource-constrained embedded systems and its efficient execution method. In the language, time-varying values changes at discrete points of time rather than continuously. Combined with a mechanism to let users designate the update interval of values, it is possible to derive the minimal value-updates required to produce the user-desired output. Also, the event-driven backend asynchronously updates an input value when its value is required. In this way, we can greatly reduce the number of updates.

DOI： 10.1007/978-3-030-26428-4_12

researchmap

担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM Press  

This paper presents an automatic parallelization method for a pure FRP language designed for embedded systems. Recent advances in microprocessor technology make it possible to use multicore processors even in resource-constrained embedded systems. To fully utilize such processors with a pure FRP language, we propose a method for parallelizing signal graph updates. The method is based on a static scheduling algorithm because it should run with a simple RTOS or without the help of operating systems. To evaluate the proposed method, we implemented a parallelizing compiler for XFRP, a pure FRP language for embedded systems. In this paper, we describe the parallelizing method and show some preliminary evaluation results using Linux-based systems that demonstrate the effectiveness of the method.

DOI： 10.1145/3358503.3361276

researchmap

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

This paper introduces a reflective extension of a functional reactive programming language designed for resource-constrained embedded systems. Using the extension, a program module can observe or modify its execution process via time-varying values that are connected to the internal of the metalevel of the module. Thus reflective operations are also reactive and described in a declarative manner. An example shows how the mechanism can realize an adaptive runtime that reduces the power consumption of small robots.

researchmap

記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

小規模組み込みシステム向けに設計された関数リアクティブプログラミング(FRP)言語Emfrpのための文脈指向プログラミング機構を提案する．提案方式では時変値の値にもとづく層の活性化機構を導入し，実行時文脈の変化に伴う振る舞いの動的な変更をFRPの枠組み内で宣言的に記述できるようにしている．これにより，小規模組込みシステムにおける適応動作のモジュール化が可能になる．

researchmap

担当区分：筆頭著者,　責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

This paper presents the design of a simple context-oriented programming extension to Emfrp, a purely functional reactive programming language for resource-constrained embedded systems. The language provides declarative and straightforward ways to describe various reactive behaviors in embedded systems. However, because of the static nature of the language, Emfrp lacks suitable capabilities to modularize adaptive behaviors. The proposed extension introduces a simple layer mechanism with implicit layer activation. It also provides a feature to describe responses to events that correspond to the moments of layer activations and deactivations. The extension can improve the modularity of Emfrp programs by separating the descriptions of context-dependent behaviors, and hence eliminating various cross-cutting code fragments.

DOI： 10.1145/3242921.3242925

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

OMetaで記述された言語処理系に対する，対象言語に依存しない衛生的マクロ機構の導入方式を提案する．OMetaは強力なパターンマッチ機構を備えたオブジェクト指向プログラミング言語であり，構文解析器などを作成するのに適している．提案方式は，Racketのマクロ機構で用いられているScope Setモデルに基づき，OMetaで記述されたプログラミング言語の構文解析器に衛生的マクロの定義構文および定義機構を導入するものである．本方式をJavascriptのサブセットおよびMinCamlの構文解析器に適用し，その有効性を確認した．

DOI： 10.11309/jssst.35.2_33

researchmap

記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

アクターモデルの考え方を取り入れた関数リアクティブプログラミング (FRP) 言語の利用が，計算資源の限られた組込みシステムにおいて柔軟な実行方式を可能にすることを示す．提案方式の特色は，小規模組込みシステム向け FRP 言語の実行時システムを並行計算モデルのひとつであるアクターモデルを用いて構成することで，FRP の特徴である宣言的記述にもとづく高い抽象性を保ちつつ，適応性の向上を可能にすることにある．これにより，適応的動作を含む組込みシステムの動作を宣言的に記述することが可能になることを例題を通して示す．

researchmap

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Institute of Electrical and Electronics Engineers Inc.  

DOI： 10.1109/SNPD.2017.8022750

Scopus

researchmap

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

DOI： 10.1145/3079368.3079387

Scopus

researchmap

出版者・発行元：ACM  

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/agere/agere2017.html#conf/agere/ShibanaiW17

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1145/2892664.2892670

Web of Science

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/aosd/modularity2016c.html#conf/aosd/SawadaW16

記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

本研究で我々は並行文脈指向プログラミングの概念とその実現手法を提案する．アクターモデルのような非同期通信に基づくシステムで文脈指向プログラミングを実現する際，文脈の変化と他の計算の間の同期に注意する必要がある．提案する手法は，文脈をまたがるメッセージに関する問題を自己反映計算を用いることで解決するものである．本論文ではErlangを用いた実装とその予備評価について述べ，提案手法の有効性を示す．

DOI： 10.11309/jssst.33.1_167

J-GLOBAL

researchmap

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Association for Computing Machinery, Inc  

DOI： 10.1145/2834965.2834972

Scopus

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/middleware/arm2015.html#conf/middleware/TakenoW15

記述言語：日本語  

J-GLOBAL

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：University of Cincinnati  

Scopus

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Association for Computing Machinery  

DOI： 10.1145/2637066.2637069

Scopus

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/ecoop/cop2014.html#conf/ecoop/WatanabeT14

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer Verlag  

DOI： 10.1007/978-3-319-08222-6

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1007/978-3-662-44471-9_3

Web of Science

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：電子情報通信学会  

作業手順がヒューマンエラーに対して耐性があるかどうか検査するためにモデル検証の手法を利用する.作業手順には,ヒューマンエラーによる誤り検出や復旧のためのタスクが埋め込まれているであろう.作業手順の信頼性を保持するためにそれらのタスクの有用性を検査する必要がある.本稿では,いくつかのヒューマンエラーの意味を定義し,それを作業手順のモデルに埋め込む方法を提案する.有用であることを示すために,ヒューマンエラーが埋め込まれたモデルに対して作業手順の目的としてのゴールに至るかどうかをモデル検証の手法をもちいて検査する.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

本研究の目的は適応的実時間システムのためのドメイン固有言語 (DSL) の提案である.組込みシステム等に要求される性質である適応性と実時間性はいずれも横断的関心事であり,プログラムを複雑化する要因となる.適応的な振舞は実行時の環境を表す情報 (文脈) に依存する動作として記述できる.そしてそのような記述のモジュール化を促進する手法として文脈指向プログラミング (COP) が提案されている.我々は,時刻および時区間を文脈とみなすことで,COP の考え方が適応的実時間システムに有効であることを示している.従来,COP を支援する機構は言語処理系を拡張して導入されることが一般的であったが,本研究ではプログラミング言語 Scala の諸機能を用いて COP のための内部 DSL を実現することで,言語処理系を拡張することなく適応的実時間システムのモジュラーな記述が可能になることを示す.

CiNii Books

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

DOI： 10.1145/2480362.2480594

Scopus

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/sac/sac2013.html#conf/sac/MoriguchiW13

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Association for Computing Machinery  

DOI： 10.1145/2541329.2541341

Scopus

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/agere/agere2013.html#conf/agere/Watanabe13

記述言語：日本語   出版者・発行元：情報処理学会  

定理証明支援系Coqに対する，対話的にプログラムの変更・修正を行うための手法を提案し，その手法をCoqに組み込んだECoqを実装する．定理証明支援系によるプログラムの検証は，プログラムがある性質を満たすという証明により行われる．この証明はプログラムの構造や記述と非常に強く結び付いているため，プログラムを変更した場合，証明もまたその変更に依存した変更を行わなければならない．しかし，プログラムと証明の一貫性を保つために必要な変更箇所は，たとえばコンストラクタの追加という簡単な変更に限った場合であっても，既存の証明支援系では見つけにくい場合がある．このような問題に対処するため，我々はCoqで検証を行ったプログラムと証明に対して，その一貫性を保ちつつ変更するための手法を提案する．本論文で提案する手法では，コンストラクタの追加を行い，変更が必要な箇所を利用者に提示する．このとき，コンストラクタを追加する型だけではなく，宣言時の状態やその型を利用する他の型などの情報を用いるため，本手法はCoqの内部に組み込むことを前提としている．この機能は，変更が必要な箇所を対話的に修正するものであるため，我々はこれを対話的修正機構と呼ぶ．本論文で紹介するECoqは，コンストラクタの追加を行うコマンドをCoqに追加したものである．ECoqを用いることで，利用者はソースコードに直接コンストラクタを追加して得られるエラーメッセージより細かい粒度での情報が得られる．特にECoqは，通常決してエラーが起こらないが，修正する可能性のある箇所を指摘することで，利用者が修正箇所を見つける補助を行う．本論文では，例題を通じてエラーメッセージが出ない箇所をECoqが提示できることを確認する．It is generally difficult to extend or modify an already-verified program while maintaining the consistency of the program itself and its accompanying proofs of certain desirable properties. In this paper, we propose a novel method to support the process of modifying verified programs by interactively correcting the program definitions and proofs developed with Coq proof assistant. For this method, we introduce ECoq, our extended version of Coq equipped with a component called interactive correction mechanism. The mechanism described in this paper deals with the addition of new constructors to existing inductive types and then tries to locate prospective correction points within the modified program and its proofs. Thanks to this mechanism, our method enables us to find such correction candidates more accurately than usual process guided by error messages of Coq. In particular, ECoq can point out some correction candidates that do not originate any errors.

researchmap

記述言語：日本語   出版者・発行元：情報処理学会  

定理証明支援系Coqに対する，対話的にプログラムの変更・修正を行うための手法を提案し，その手法をCoqに組み込んだECoqを実装する．定理証明支援系によるプログラムの検証は，プログラムがある性質を満たすという証明により行われる．この証明はプログラムの構造や記述と非常に強く結び付いているため，プログラムを変更した場合，証明もまたその変更に依存した変更を行わなければならない．しかし，プログラムと証明の一貫性を保つために必要な変更箇所は，たとえばコンストラクタの追加という簡単な変更に限った場合であっても，既存の証明支援系では見つけにくい場合がある．このような問題に対処するため，我々はCoqで検証を行ったプログラムと証明に対して，その一貫性を保ちつつ変更するための手法を提案する．本論文で提案する手法では，コンストラクタの追加を行い，変更が必要な箇所を利用者に提示する．このとき，コンストラクタを追加する型だけではなく，宣言時の状態やその型を利用する他の型などの情報を用いるため，本手法はCoqの内部に組み込むことを前提としている．この機能は，変更が必要な箇所を対話的に修正するものであるため，我々はこれを対話的修正機構と呼ぶ．本論文で紹介するECoqは，コンストラクタの追加を行うコマンドをCoqに追加したものである．ECoqを用いることで，利用者はソースコードに直接コンストラクタを追加して得られるエラーメッセージより細かい粒度での情報が得られる．特にECoqは，通常決してエラーが起こらないが，修正する可能性のある箇所を指摘することで，利用者が修正箇所を見つける補助を行う．本論文では，例題を通じてエラーメッセージが出ない箇所をECoqが提示できることを確認する．It is generally difficult to extend or modify an already-verified program while maintaining the consistency of the program itself and its accompanying proofs of certain desirable properties. In this paper, we propose a novel method to support the process of modifying verified programs by interactively correcting the program definitions and proofs developed with Coq proof assistant. For this method, we introduce ECoq, our extended version of Coq equipped with a component called interactive correction mechanism. The mechanism described in this paper deals with the addition of new constructors to existing inductive types and then tries to locate prospective correction points within the modified program and its proofs. Thanks to this mechanism, our method enables us to find such correction candidates more accurately than usual process guided by error messages of Coq. In particular, ECoq can point out some correction candidates that do not originate any errors.

CiNii Books

researchmap

その他リンク： http://id.nii.ac.jp/1001/00083703/

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：IEEE Computer Society  

DOI： 10.1109/SNPD.2012.115

Scopus

J-GLOBAL

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/snpd/snpd2012.html#conf/snpd/SenthooranW12

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1016/j.entcs.2006.07.002

Scopus

J-GLOBAL

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1109/ARES.2006.114

Web of Science

J-GLOBAL

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/IEEEares/ares2006.html#conf/IEEEares/NagatouW06

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：社団法人情報処理学会  

我々は, 契約による設計(Design by Contract, DbC)に基づく, アスペクト指向振舞インタフェース仕様記述言語Moxaの設計・開発を行っている.DbCは, サービスの提供者と利用者の間で, 利用者が満たすべき条件(事前条件)と提供者がもたらす結果(事後条件)を契約として取り決め, 責任の切り分けやサービスの利用方法と得られる結果を明確にすることで, ソフトウェアの品質を向上させる.JavaのためのDbCに基づく振舞インタフェース仕様記述言語の1つであるJML(Java Modeling Language)は, メソッドごとに事前条件・事後条件の記述を可能にするが, メソッド数の増加や提供するサービスの高機能化がこれらの条件を複雑なものにし, 表明の整合性・表明とプログラムの一貫性を維持しつつ, これらを修正・拡張することを難しくする.Moxaは, 複雑なオブジェクトの振舞いをいくつかの独立した側面の合成としてとらえることができる場合に, それらを表明アスペクトと呼ばれる独立したモジュールに分割して記述す

researchmap

出版者・発行元：Fakultat fur Informatik, Universitat Magdeburg  

researchmap

出版者・発行元：IASTED/ACTA Press  

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1109/WSTFES.2003.1201363

Web of Science

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/wstfeus/wstfeus2003.html#conf/wstfeus/WatanabeYN03

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1007/3-540-36532-X_13

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

DOI： 10.11309/jssst.20.292

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

本研究の目標は，実行環境に柔軟かつ安全に適応できるモバイルコードプログラムを実現することである．このような適応性はモバイルコードプログラムの発展に重要なメカニズムと見なすことができる．この目標のため，本研究ではSAMcodeというソフトウェアモデルを新たに提案した．SAMCodeにもとづくモバイルコードプログラムは，誤動作，ランタイムエラー，システム障害などを発生させることなく，実行環境に柔軟に適応することができる．

DOI： 10.1145/512035.512050

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

本研究では，コンポーネントベースのソフトウェアにおける動的適応性の安全性について検討し，そのためのソフトウェアモデルSafe DASを提案した．本研究における安全性とは，適応可能な動作がそのソフトウェアの一貫性を損なわないことを意味する．このような安全な動的適応性を実現するため，Safe DASモデルは適応動作のアトミック化とシリアル化をもたらし，実行環境の動的な状態変化に応じて変化するアサーションなどを支援する．

DOI： 10.1145/602461.602504

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Web of Science

researchmap

出版者・発行元：Springer  

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/reflection/reflection99.html#conf/reflection/AmanoW99

出版者・発行元：IEEE Computer Society  

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/tools/tools31-1999.html#conf/tools/AmanoW99

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

開放型分散システム環境や移動計算機環境の普及にともない, さまざまな実行環境やその動的な状態変化に適応できるソフトウェアの必要性が高まっている.本稿では, そうした動的適応可能なソフトウェアのモデルおよびそれを構成するための言語LEADについて述べる.鍵となるアイディアは, 1)手続き呼び出し時に, 手続きの実行コードを実行環境の状態に応じて動的に切り替える機構を導入する, 2)動的適応可能なソフトウェアをメタレベルアーキテクチャとして構成し, 適応動作の記述と問題領域の記述を分離・独立させる, といった点にある.言語LEADは, このような動的に変化する手続きの定義, および制御の機構を言語機能として提供し, LEADによる動的適応可能なソフトウェアはメタレベルアーキテクチャを形成する.LEADを用いることで, 1)拡張性の高い動的適応可能なソフトウェアの実現, 2)既存ソフトウェアへの動的適応能力の導入, などが可能となる.

researchmap

記述言語：日本語   出版者・発行元：一般社団法人日本ソフトウェア科学会  

CiNii Books

researchmap

掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：World Scientific, Singapore  

researchmap

出版者・発行元：Chapman & Hall  

researchmap

出版者・発行元：Japan Advanced Institute of Science and Technology.  

This paper reports a language-based approach to constructing adaptable applications --- application level software systems which dynamically adapt themselves to their changing runtime environments. Adaptable applications are especially indispensable to mobile distributed computing. However, such flexible applications remain more expensive to develop, maintain and port compared to their 'fixed' counterparts. Our approach is based on a language mechanism called generic procedure which enhances the modular development of adaptable applications. Using this mechanism, an application programmer c...

researchmap

担当区分：最終著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

並行オブジェクトの間で共有される計算資源の概念をとり入れた自己反映計算モデルであるHybrid Group Architectureと,その記述言語ABCL/R2を提案した.ABCL/R2では,オブジェクト単位の自己反映計算と,オブジェクトグループ単位での自己反映計算の両方が可能なため,スケジューリングのような,並列・分散システムにおける共有計算資源に関する制御を,本来の計算から隠蔽された形をとりつつ,言語の枠内から柔軟に記述できる.また,自己反映システムの効率的な処理系は,作成が困難とされていたが,部分コンパイル・段階的なメタレベル生成・軽量オブジェクトなどの技法による効率的な処理系の作成方法を示した.実際に共有記憶型並列計算機上に作成したABCL/R2処理系では,自己反映計算を行うことによる速度低下を,行わない場合の10倍以下に抑えられ,非自己反映計算の実行速度は,非自己反映処理系とほぼ同等であるというベンチマーク結果を得た.

DOI： 10.11309/jssst.11.3_175

CiNii Books

researchmap

その他リンク： https://projects.repo.nii.ac.jp/?action=repository_uri&item_id=287616

担当区分：筆頭著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：一般社団法人日本ソフトウェア科学会  

DOI： 10.11309/jssst.11.3_165

CiNii Books

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1145/141937.141948

Web of Science

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/oopsla/oopsla92.html#conf/oopsla/MasuharaMWY92

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1007/3-540-55613-3_11

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1007/BFb0057025

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1007/BFb0019450

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1145/67387.67399

Web of Science

researchmap

その他リンク： http://dblp.uni-trier.de/db/journals/sigplan/sigplan24.html#journals/sigplan/YonezawaW89

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1145/62084.62111

Web of Science

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/oopsla/oopsla88.html#conf/oopsla/WatanabeY88

担当区分：筆頭著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：人工知能学会  

DOI： 10.11517/jjsai.2.2_206

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

文脈指向プログラミング(COP)とは,プログラムの実行文脈に応じて振る舞いが変化するようなプログラムのモジュール性を高める技術である.本研究で我々は,言語の拡張を導入せずにCOPをObjective-Cで実現するための手法を提案する.Objective-Cは実行時にメソッドの書き換えを行うことができる動的なオブジェクトシステムを備えている.我々はこの機構を用いてCOPを実現した.本論文では提案手法によるCOPの実現方式について述べ,実行時オーバーヘッドについての評価結果を示す.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語  

証明支援系 Coq のプログラムに対する対話的修正機構を提案する．証明支援系はプログラムなどの正しさを証明するために利用されている．しかし，Coq による証明は対象となる体系の定義に密接に関連しているため，定義のわずかな修正に対して多くの不整合が発生する．このような不整合に対し，場所の確認を Coq からのエラーによって発見するという，退屈で，かつ誤りを組み込みやすい作業で行うことが一般的になっている．提案する機構を組み込んだ証明支援系を用いることにより，この作業を簡易化することができる．対話的修正機構は修正箇所の記述を受け取ることで，その修正によって不整合が生じた箇所を提示することができる．また，この提示された箇所をもとに修正を対話的に行うことを可能にしている．本発表で提案している Coq における対話的修正機構では，帰納型に新たなコンストラクタを追加することと，そのコンストラクタに対応するデストラクタの拡張を行う機能を持っている．このように機能としては非常に制限されているが，それにより非常に高い再利用性を得ることができる．本発表では，不整合のある箇所の検出方法と，制限の詳細について述べる．We propose an interactive refinement mechanism for Coq proof assistant, which aims to improve the reusability of proof scripts. Suppose that we have some proof scripts about a computer program. We call the program the proof target of the proof scripts. The problem is that it is generally difficult to reuse the scripts for a modified proof target. Even some small changes, such as just adding new constructors to some inductive types, could cause a large number of inconsistencies in the scripts. Usually we should manually find and fix them by examining error messages issued by the proof assistant, which is hard and error-prone process. Using the proof assistant modified to incorporate the proposed mechanism can ease the process. By providing the modified part of the target definition, our interactive refinement mechanism finds all the inconsistent parts in the definition and the proof scripts. After finding them, we can easily gain the proofs for the new target by issuing correction commands to the modified proof assistant. The interactive refinement mechanism for Coq described in this presentation covers the extension of inductive data types with new constructors and the destructors correspond to them. Our current refinement mechanism is limited, but provides us with practical means to reuse machine-assisted proofs. In this presentation, we discuss the methods to detect inconsistent parts and details of limitations for extensions.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

証明支援系 Coq のプログラムに対する対話的修正機構を提案する.証明支援系はプログラムなどの正しさを証明するために利用されている.しかし,Coq による証明は対象となる体系の定義に密接に関連しているため,定義のわずかな修正に対して多くの不整合が発生する.このような不整合に対し,場所の確認を Coq からのエラーによって発見するという,退屈で,かつ誤りを組み込みやすい作業で行うことが一般的になっている.提案する機構を組み込んだ証明支援系を用いることにより,この作業を簡易化することができる.対話的修正機構は修正箇所の記述を受け取ることで,その修正によって不整合が生じた箇所を提示することができる.また,この提示された箇所をもとに修正を対話的に行うことを可能にしている.本発表で提案している Coq における対話的修正機構では,帰納型に新たなコンストラクタを追加することと,そのコンストラクタに対応するデストラクタの拡張を行う機能を持っている.こ

researchmap

記述言語：英語   出版者・発行元：一般社団法人電子情報通信学会  

検証済みのモデルから実時間プログラムを生成する手法を提案する.本手法では,時間制約を実行時に検査するために,それに伴うオーバーヘッドをあらかじめモデルの性質の一部に取り入れる.これにより,実時間スケジューラのないOSやランタイム上でのソフト実時間システムの実現を容易にすることを目指す.本稿では,時間オートマトンで記述され,モデル検査器UPPAALで検証されたモデルから,JavaおよびCのコードを生成する手法について述べる.簡単なロボットの制御プログラムの記述例を通して,提案手法の有効性を示す.

CiNii Books

researchmap

記述言語：英語   出版者・発行元：一般社団法人電子情報通信学会  

検証済みのモデルから実時間プログラムを生成する手法を提案する.本手法では,時間制約を実行時に検査するために,それに伴うオーバーヘッドをあらかじめモデルの性質の一部に取り入れる.これにより,実時間スケジューラのないOSやランタイム上でのソフト実時間システムの実現を容易にすることを目指す.本稿では,時間オートマトンで記述され,モデル検査器UPPAALで検証されたモデルから,JavaおよびCのコードを生成する手法について述べる.簡単なロボットの制御プログラムの記述例を通して,提案手法の有効性を示す.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

我々はMorrisのアルゴリズムのCによる実装の検証を試みた.このアルゴリズムは再帰やスタックを用いずに二分木の走査を行うものであり,節点内部に余分なタグも不要であるという特徴がある.本研究はポインタ操作を伴うCプログラムへの検証支援ツール適用のケーススタディであり,今回は検証支援系CaduceusおよびWhy,自動証明系Simplifyおよび対話的証明支援系Coqを使用した.本稿では,これらによる検証手法とその結果の概要を述べる.

researchmap

記述言語：日本語  

我々は，Morrisの2分木走査アルゴリズムのCによる実装を対象として，証明支援系を用いた正当性の検証を試みた．本論文はその手法と結果に関する報告である．Morrisのアルゴリズムは，ポインタの書き換えを行うことで再帰やスタックを用いずに2分木走査を行う方法のひとつである．また他のポインタ反転法と異なり節点に印を付けるためのビットを設ける必要もないのが特徴である．我々は，入力および走査結果についての仕様を事前・事後条件として与え，C用の検証支援ツールであるCaduceusによって検証条件を生成した．ループ不変条件は必要に応じて適宜与えた．生成された検証条件を自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した．

CiNii Books

researchmap

記述言語：日本語  

本研究では、オブジェクト計算で形式的に表現できる事象を増やすために、継続オブジェクト内に保存された評価文脈を変更可能にし、継続を呼び出す時にその変更が反映される体系を提唱する。前の継続オブジェクト計算の体系では継続オブジェクト内に保存されている評価文脈内のメソッドの変更は不可能であるため、継続を呼び出して評価文脈を再利用するとき評価文脈の一部分を変更して扱いたい場合に、継続オブジェクトを作り直さなければいけなかった。これを、直接変更できるように体系を再定義し直すことで、オブジェクト計算で表現できる幅を広げる。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

ポインタ書き換えを伴うプログラムのプログラム変換にもとづく検証のケーススタディとして,Morrisの二分木走査アルゴリズムの正当性を扱った.本稿ではその際に用いたプログラム変換手法とその具体的な適用手法について報告する.

CiNii Books

researchmap

記述言語：日本語  

アスペクト指向が提案されて十余年たち，ソフトウェア工学の広い分野で用いられている．しかしながら，アスペクトとは何であるかを議論することはほとんどなく，ただAspectJに代表されるジョインポイントモデルにおけるモジュールをアスペクトとすることが多い．このように本質を定義しないままの議論は実際の言語に強く依存したものとなり，またツールにおけるアルゴリズムとその実装もアドホックになる．アスペクト指向はモジュール化を主眼としたものであり，その特徴はアスペクトモジュールの結合方法にあるといえる．本研究では，この結合方法を抽象化および定式化し，アスペクト指向の理解や議論の基礎とすることを目標としている．本研究の特徴はアスペクト指向言語のとらえ方にある．現存するアスペクト指向言語は，既存の言語に対して拡張を施すことによって作成されている．一方，既存研究ではアスペクト指向言語を1) ラムダ計算のような既存の計算体系にアスペクト指向を加えたもの，または2) 言語全体を記述する体系で定式化している．それに対し，本研究では2) と同様に既存の計算体系に依存せずにアスペクト指向としての操作の定式化のみを行い，他の体系との組合せによって1のように言語を表現する．本発表では，アスペクト指向における操作の定式化と，ラムダ計算との組合せによる言語の定式化，および他研究における議論の表現について述べる．Aspect-orientation has gained in software development in the last decade. However, formal and/or general definitions of aspects and related concepts are not thoroughly discussed so far. The important concepts such as aspect, join point, pointcut, advice, etc. are defined on top of specific aspect-oriented languages such as AspectJ. Our goal is to formalize some'aspectual'operations commonly used in aspect-oriented languages. We designed a simple calculus that models the operations independently from other computational activities such as function application or message passing. We can easily construct a model of a specific aspect-oriented language by mixing our calculus with another model that represents the base computation. In this presentation, we give a formalization of the aspectual operations in our calculus and then discuss the formalization by comparing to other works.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

アスペクト指向が提案されて十余年たち,ソフトウェア工学の広い分野で用いられている.しかしながら,アスペクトとは何であるかを議論することはほとんどなく,ただAspectJに代表されるジョインポイントモデルにおけるモジュールをアスペクトとすることが多い.このように本質を定義しないままの議論は実際の言語に強く依存したものとなり,またツールにおけるアルゴリズムとその実装もアドホックになる.アスペクト指向はモジュール化を主眼としたものであり,その特徴はアスペクトモジュールの結合方法にあるといえる.本研究では,この結合方法を抽象化および定式化し,アスペクト指向の理解や議論の基礎とすることを目標としている.本研究の特徴はアスペクト指向言語のとらえ方にある.現存するアスペクト指向言語は,既存の言語に対して拡張を施すことによって作成されている.一方,既存研究ではアスペクト指向言語を1) ラムダ計算のような既存の計算体系にアスペクト指向を加え

researchmap

記述言語：英語   出版者・発行元：社団法人電子情報通信学会  

自己反映計算は高度に柔軟で適応的なシステムを構築するための重要な考え方である.本稿で報告する自己反映計算の振舞的側面の形式化は,計算システムを表す抽象的なモデル間の実現関係に基づいており,これによってリフレクティブタワーのような無限の構造をアプリオリに導入せずに自己反映計算についての議論を可能にする.現在までの主な貢献は,明示的なメタレベルの存在範囲を形式化に導入することで,自己反映計算機構の強さを形式的に議論するための基礎を与えたことである.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：社団法人電子情報通信学会  

アスペクト指向プログラミング(AOP)はソフトウェア開発において広く用いられており、アスペクト指向プログラミング言語のもつ性質を形式的にとらえ、理解することはプログラミング言語研究の重要な課題のひとつである。我々は、ポイントカットやアドバイスといったアスペクト指向言語拡張の性質をとらえることを目的とした計算体系LMCを提案する。LMCは特定のプログラミング言語に依存しない形で定義されており、これをアスペクト指向言語拡張の定義に用いることで、アスペクト指向プログラミング言語の形式的定義をモジュール化できる。本論文ではLMCの定義の概要を示し、アスペクト指向拡張をもつ簡単なオブジェクト指向言語をLMCを用いて形式的に定義する。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：社団法人情報処理学会  

MoxaはJavaを対象とした振る舞いインターフェース記述言語であり,表明アスペクトと呼ばれる機構の導入によって仕様記述のモジュール化を促進している.本稿ではMoxaの表明アスペクトを用いた仕様記述について概観し,さらに表明アスペクトを拡張して仕様記述のモジュール化をより促進する方法について議論する.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：社団法人情報処理学会  

モニタにより強制可能なセキュリティーポリシの特徴について議論する.ここでいうモニタとはプログラムの振舞を監視し,もしそれがポリシに違反するときにはそのプログラムを強制的に停止することによりポリシを強制する強制機構のことである.もちろん,このような強制機構ではすべてのポリシが強制可能であるわけではない.なぜなら,モニタはプログラムの有限の振舞しか観測できず,未来の情報を利用することが出来ないからである.F.B.Schneiderはこのような特徴をもつポリシはLamportの安全性の特徴を充たすことを示した.また,そのような安全性を受理するようなオートマトンが存在し,それをセキュリティーオートマトンと呼んでいる.さらに,我々はモニタは単にプログラムの振舞を観測するだけでなくもっと多くの情報を利用できると考える.そのとき,ポリシがどのような特徴を持つか明らかにすることを試みる.これまでに,観測した有限の振舞の部分的な振舞を利用することにより情

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

モニタにより強制可能なセキュリティーポリシの特徴について議論する.ここでいうモニタとはプログラムの振舞を監視し,もしそれがポリシに違反するときにはそのプログラムを強制的に停止することによりポリシを強制する強制機構のことである.もちろん,このような強制機構ではすべてのポリシが強制可能であるわけではない.なぜなら,モニタはプログラムの有限の振舞しか観測できず,未来の情報を利用することが出来ないからである.F.B.Schneiderはこのような特徴をもつポリシはLamportの安全性の特徴を充たすことを示した.また,そのような安全性を受理するようなオートマトンが存在し,それをセキュリティーオートマトンと呼んでいる.さらに,我々はモニタは単にプログラムの振舞を観測するだけでなくもっと多くの情報を利用できると考える.そのとき,ポリシがどのような特徴を持つか明らかにすることを試みる.これまでに,観測した有限の振舞の部分的な振舞を利用することにより情報流ポリシが不干渉という意味で強制可能であることを明らかにした.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：社団法人電子情報通信学会  

モニタにより強制可能なセキュリティーポリシの特徴について議論する.ここでいうモニタとはプログラムの振舞を監視し,もしそれがポリシに違反するときにはそのプログラムを強制的に停止することによりポリシを強制する強制機構のことである.もちろん,このような強制機構ではすべてのポリシが強制可能であるわけではない.なぜなら,モニタはプログラムの有限の振舞しか観測できず,未来の情報を利用することが出来ないからである.F.B.Schneiderはこのような特徴をもつポリシはLamportの安全性の特徴を充たすことを示した.また,そのような安全性を受理するようなオートマトンが存在し,それをセキュリティーオートマトンと呼んでいる.さらに,我々はモニタは単にプログラムの振舞を観測するだけでなくもっと多くの情報を利用できると考える.そのとき,ポリシがどのような特徴を持つか明らかにすることを試みる.これまでに,観測した有限の振舞の部分的な振舞を利用することにより情

researchmap

記述言語：日本語   出版者・発行元：社団法人電子情報通信学会  

モニタにより強制可能なセキュリティーポリシの特徴について議論する.ここでいうモニタとはプログラムの振舞を監視し,もしそれがポリシに違反するときにはそのプログラムを強制的に停止することによりポリシを強制する強制機構のことである.もちろん,このような強制機構ではすべてのポリシが強制可能であるわけではない.なぜなら,モニタはプログラムの有限の振舞しか観測できず,未来の情報を利用することが出来ないからである.F.B.Schneiderはこのような特徴をもつポリシはLamportの安全性の特徴を充たすことを示した.また,そのような安全性を受理するようなオートマトンが存在し,それをセキュリティーオートマトンと呼んでいる.さらに,我々はモニタは単にプログラムの振舞を観測するだけでなくもっと多くの情報を利用できると考える.そのとき,ポリシがどのような特徴を持つか明らかにすることを試みる.これまでに,観測した有限の振舞の部分的な振舞を利用することにより情

researchmap

記述言語：日本語   出版者・発行元：社団法人情報処理学会  

我々は現在までに、Javaのための振舞インターフェース仕様記述言語Moxaを開発してきた。MoxaはJava Modeling Language (JML)を拡張したものであり、表明アスペクトと呼ばれる機構を用いて表明間を横断する性質を分離することで、長大で複雑になりがちな実アプリケーションの仕様のモジュール化を可能にしている。本稿ではまずMoxaの設計について簡単に説明した後、その拡張-プロトコルにもとづくアスペクト記述-について議論する。この拡張は、メソッド呼び出し系列(プロトコル)にもとづいた仕様の記述・テスト・検証を容易にするためのものである。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

我々は，契約による設計（Design by Contract，DbC）に基づく，アスペクト指向振舞インタフェース仕様記述言語Moxa の設計・開発を行っている．DbC は，サービスの提供者と利用者の間で，利用者が満たすべき条件（事前条件）と提供者がもたらす結果（事後条件）を契約として取り決め，責任の切り分けやサービスの利用方法と得られる結果を明確にすることで，ソフトウェアの品質を向上させる．Java のためのDbC に基づく振舞インタフェース仕様記述言語の1 つであるJML（Java Modeling Language）は，メソッドごとに事前条件・事後条件の記述を可能にするが，メソッド数の増加や提供するサービスの高機能化がこれらの条件を複雑なものにし，表明の整合性・表明とプログラムの一貫性を維持しつつ，これらを修正・拡張することを難しくする．Moxa は，複雑なオブジェクトの振舞いをいくつかの独立した側面の合成としてとらえることができる場合に，それらを表明アスペクトと呼ばれる独立したモジュールに分割して記述することを可能にする．この，オブジェクトの振舞いのある側面は，JML による記述では複数のメソッドに対する表明を横断する形で存在していたものである．本論文では，Moxa が提供する表明記述のモジュール化機構と，その記述方式の説明を行う．In this paper, we report the design and implementation of Moxa ? a behavioral interface specification language that supports DbC (Design by Contract) based specifications. In DbC methodology, a contract arranges responsibilities between a user and a supplier of the service. This improves software quality because this makes clear who has responsibility, how to use, and what is the result of the service. With JML (Java Modeling Language), a DbC based behavioral interface specification language for Java, we can declare assertions as pre/post-conditions for each method. However, as the number of methods increases and the functionalities of services become complex, assertions for each method gets complicated. This makes it difficult to keep the consistency between assertions and methods while we are modifying them. Using Moxa, we can divide and describe assertions into several modules called assertion-aspects, when we can regard the behavior of the object(s) as the composition of some independent aspects. In JML style specification declaration, the aspects are crosscut over the assertions declared for difference methods. In this paper, we show the modularization mechanism for assertion declarations and description method provided by Moxa.

CiNii Books

researchmap

その他リンク： http://id.nii.ac.jp/1001/00016611/

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

契約による設計（Design by Contract，DbC）は，ある処理の実行直前・直後で満たされるべき条件を表明として明示し，それらを処理の利用者と提供者の間の契約とすることで，責任の切り分けを明確にする．DbC に基づく表明の記述では，プログラムが大規模化するとともに，表明の数が増加し個々の表明も複雑になり，表明の整合性や表明とプログラムの一貫性を維持しつつ，それらを修正・拡張することが難しくなる．この原因は，従来のDbC に基づく表明の記述方式では，表明をプログラムに埋め込む形で記述するため，表明の記述をプログラムの構造から独立にモジュール化できないことにある．そこで我々は，DbC に基づく表明の記述をアスペクト指向的にモジュール化する方式を提案する．本発表の概要は以下のとおりである．まず背景として，Java で実装された電子メールメッセージを扱うライブラリと，その実装のJML（Java Modeling Language）による検査について説明する．JML はJava を対象としたDbC のための表明記述を可能にする言語である．次に，この検査の過程で問題となった表明記述の記述量の増加について述べるとともに，この問題に対処する，我々が提案する表明の記述をアスペクト指向的にモジュール化する方式についての説明を行う．その後，JML と本方式との比較を行い本方式の優位性を述べ，さらに今後の展開として，モジュール化された表明の記述から状態遷移モデルを生成する方式について述べる．In Design by Contract (DbC) facility, we explicitly specify conditions as assertions for each procedures which must hold just before/after a procedure execution, and consider them to be a contract between procedures and it's users. This makes clean who is responsible for problems of a procedure execution. The more the scale of a program grows up, the more Description of assertions based on DbC complicated, because number of assertions increases and complexity of each assertions are increased. Hence it becomes difficult to modify and/or extend programs and assertions without lose consistency between them and coherence of assertions. The reason of this problem is that we cannot modularize description of assertions independent of program structure, because in the way to describe assertions based on DbC, assertions must be embeded in the programs. So we propose an aspect-oriented modularization technique for the description of assertions based on DbC. In this technique, we think of assertion as advice, location to check the assertion as join point, and the set of them as aspect. This technique makes modularization technique for the description of assertion flexible. In this presentation, we show the implementation of Maildir Folder Service Provider we developed, which manages E-mail messages in Java, and we describe a test of this implementation using Java Modeling Language (JML) which extends java to be able to describe assertions base on DbC. Next, we show the problems for increasing of description of assertions in the test process, and propose aspect-oriented modularization technique for description of assertions. And then, we compare this technique with JML and show this method is more preferable. And finally, we show a method to generate state transition models from a modularized description of assertions.

CiNii Books

researchmap

出版者・発行元：社団法人情報処理学会  

契約による設計(Design by Contract, DbC)は, ある処理の実行直前・直後で満たされるべき条件を表明として明示し, それらを処理の利用者と提供者の間の契約とすることで, 責任の切り分けを明確にする.DbCに基づく表明の記述では, プログラムが大規模化するとともに, 表明の数が増加し個々の表明も複雑になり, 表明の整合性や表明とプログラムの一貫性を維持しつつ, それらを修正・拡張することが難しくなる.この原因は, 従来のDbCに基づく表明の記述方式では, 表明をプログラムに埋め込む形で記述するため, 表明の記述をプログラムの構造から独立にモジュール化できないことにある.そこで我々は, DbCに基づく表明の記述をアスペクト指向的にモジュール化する方式を提案する.本発表の概要は以下のとおりである.まず背景として, Javaで実装された電子メールメッセージを扱うライブラリと, その実装のJML(Java Modeling Language)による検査について説明する.JMLはJavaを対象としたDbCのための表明記述

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

CiNii Books

researchmap

出版者・発行元：日本ソフトウェア科学会  

実行監視とは、プログラムの各実行ステッぷを観測し、それがセキュリティーポリシに違反するときにはそのプログラムを停止させるなどしてポリシに違反しないことを保障する機構の総称である。実行監視によって強制されるポリシのクラスは安全性であることが知られている。我々は、プログラムから得られる情報をもちいて強制可能なポリシのクラスについて議論する。本稿では、特に機密性と上限つき可用性について議論する。

DOI： 10.11309/jssstconference.21.0.67.0

researchmap

出版者・発行元：日本ソフトウェア科学会  

オブジェクト指向言語における契約による設計(Design by Contract)では，各メソッドに対して，事前条件，事後条件という形で契約(仕様)を与え，プログラムを開発する．このような設計では，表明数が増加し更に個々の表明も複雑になり，仕様が大規模になるため，仕様の一貫性を保ち続けることが難しくなる.これに対処するため，本研究では，大規模な仕様の部分仕様をアスペクトと見なすことで，仕様を分割記述できる，アスペクト指向的モジュール化方式を提案する．また，モジュール記述から状態遷移モデルを抽出し，モデルチェックを行う方法について述べる．

DOI： 10.11309/jssstconference.21.0.24.0

researchmap

記述言語：日本語   出版者・発行元：一般社団法人日本ソフトウェア科学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

柔軟な分散計算システムを構築するための便利な抽象化機構としてさまざまな形態の異動コードが注目されてきた．固定的なネットワークシステムから移動・遍在計算機環境へとシフトするうえで，移動コードの重要性が増している．しかし，実際の応用システムで移動コードを採用するうえで，解決しなければならないセキュリティ上の問題はまだ多い．さらに，移動コードを用いてシステムを構成するためには，コードの移動がひきおこすさまざまな変化に対処できる必要がある．そしてセキュリティモデルもそのために拡張可能（あるいは適応的）である必要があり，さらにそういったセキュリティモデルのためのポリシー記述はむずかしい．今回の発表では，まずアプリケーション依存のセキュリティポリシーについて述べ，次にそういったポリシーを強制する方法の提案について説明する．対象とする移動コードは，ここではJava クラスファイルとする．我々の方式は，主としてロード時のバイトコード変換によって監視付き実行を行うコードを挿入するものであるが，そのためのポリシーをPolaris という特別な言語によって記述する．Polaris は基本的には有限状態プロセス言語であるが，変数間のデータ依存関係を扱えるようになっている．これによって監視のコストを抑えることができる．記述の具体例として，我々が構築しつつある拡張可能メールクライアントの一部を示す．Mobile code has been regarded as a convenient abstraction mechanism to construct flexi-ble/evolvable distributed computing systems. It has now gained prominence, mainly due to the current shift from stationary to mobile/ubiquitous computing environment. Although de-signing a system using mobile code is appealing, its deployment is still a security risk. Further, a system using mobile code is inherently dynamic; we need an extensible/adaptable security model. In this talk, we first claim that application-dependent and special-purpose security policies are increasingly important especially for modern distributed computing environment. Then we present a set of techniques that may be used to enforce such policies on mobile objects (Java classes). The main technique is a load-time bytecode modification that enforces user-defined policies via monitored execution. The policies are written in a language called Polaris, which is basically a finite process language enhanced to deal with data-dependencies among variables. Use of data-dependencies reduced the cost of monitoring. As an example, we show a code portion from our extensible e-mail client system.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：社団法人情報処理学会  

柔軟な分散計算システムを構築するための便利な抽象化機構としてさまざまな形態の異動コードが注目されてきた.固定的なネットワークシステムから移動・遍在計算機環境へとシフトするうえで,移動コードの重要性が増している.しかし,実際の応用システムで移動コードを採用するうえで,解決しなければならないセキュリティ上の問題はまだ多い.さらに,移動コードを用いてシステムを構成するためには,コードの移動がひきおこすさまざまな変化に対処できる必要がある.そしてセキュリティモデルもそのために拡張可能(あるいは適応的)である必要があり,さらにそういったセキュリティモデルのためのポリシー記述はむずかしい.今回の発表では,まずアプリケーション依存のセキュリティポリシーについて述べ,次にそういったポリシーを強制する方法の提案について説明する.対象とする移動コードは,ここではJavaクラスファイルとする.我々の方式は,主としてロード時のバイトコード変換

researchmap

出版者・発行元：日本ソフトウェア科学会  

複数のクラスにまたがるコードを分離して記述できる言語として、アスペクト指向言語がある。独立して開発されたアスペクトであっても、個々のアスペクトが何らかのルールに従って設計されていれば、複数同時に組み合わせて動作させることが可能であると我々は考えている。本論文ではそのようなルールを見いだし検証するための第一歩として、安全に結合可能なmixin を提供するためのルールを検証する方法について述べる。ルールの記述および検証には、Designby Contract やbehavioral subtyping の考え方を用いる。

DOI： 10.11309/jssstconference.19.0.3E3.0

researchmap

記述言語：日本語   出版者・発行元：共立出版  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CORBAのアプリケーション開発における問題点として，クロスプラットフォームの開発時に生じるインタフェースの不一致，およびスタブとスケルトンのアプリケーションへの組み込みのために生じる開発手順の煩雑さを取り上げ，インターフェイスリポジトリとリフレクションの可能なプログラミング言語を利用して，これらを解決する手法を提案する．この手法を実現するために必要なリフレクションの能力として，プログラム自身の参照/改変および未定義名の参照時の振る舞いの変更を取り上げ，その利用方法と利点について議論する．We focus on the problems in the development of CORBA applications: interface mismatches which often take place in cross-platform development, and complicated development procedure which consists of generating stubs and skeletons and incorporating them into applications. We propose a solution of these problems using the Interface Repository and reflective programming languages. We inspect the abilities of reflective languages to realize this solution, especially generation and modification of programs and modification of the behavior of the languages in referring undefined names.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CORBAのアプリケーション開発における問題点として, クロスプラットフォームの開発時に生じるインタフェースの不一致, およびスタブとスケルトンのアプリケーションへの組み込みのために生じる開発手順の煩雑さを取り上げ, インターフェイスリポジトリとリフレクションの可能なプログラミング言語を利用して, これらを解決する手法を提案する.この手法を実現するために必要なリフレクションの能力として, プログラム自身の参照/改変および未定義名の参照時の振る舞いの変更を取り上げ, その利用方法と利点について議論する.

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

自己反映的なプログラミング言語は, 言語処理系自身を計算の対象として扱うことが可能な言語システムであり, 言語の実装レベルの記述を, メタレベルとして分離することによって, 複雑なアプリケーションの記述を簡潔に行うことができる.また, メタレベルを上手にモジュール化することによって, 拡張を再利用することができる.しかし言語拡張を再利用するためには, 複数のメタのモジュール同士の意味的な衝突を考慮する必要がある.通常, 再利用を前提として言語の拡張を記述する際には, その拡張を適用する対象の言語として純粋なものを想定することになる.そのような前提は, 拡張同士を組み合わせることで保証できなくなる.そこで本稿では言語拡張同士の意味的な衝突を回避するための枠組みを示す.本稿ではMonad Transformerを用いた言語システムのモジュール化を行い, 言語を構成するコンポーネント間の依存関係を明確にする.その枠組みに基づいて, 自己反映的なプログラミング

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

自己反映的なプログラミング言語は，言語処理系自身を計算の対象として扱うことが可能な言語システムであり，言語の実装レベルの記述を，メタレベルとして分離することによって，複雑なアプリケーションの記述を簡潔に行うことができる．また，メタレベルを上手にモジュール化することによって，拡張を再利用することができる．しかし言語拡張を再利用するためには，複数のメタのモジュール同士の意味的な衝突を考慮する必要がある．通常，再利用を前提として言語の拡張を記述する際には，その拡張を適用する対象の言語として純粋なものを想定することになる．そのような前提は，拡張同士を組み合わせることで保証できなくなる．そこで本稿では言語拡張同士の意味的な衝突を回避するための枠組みを示す．本稿ではMonad Transformerを用いた言語システムのモジュール化を行い，言語を構成するコンポーネント間の依存関係を明確にする．その枠組みに基づいて，自己反映的なプログラミング言語を実装し，ある拡張と，それ以前の拡張との間で生じる衝突について検知し，拡張者に対してその情報を提供するための具体的な方法について提案する．A reflective system can understand/compute its structure and behavior at run time. Giving the facility of reflection to OS or programming languages, it is possible to construct the advanced and complex systems, like mobile computing systems or distributed systems, with more systematic manner. Practically, the programmer might want to apply several extensions to the language simultaneously. But, there might be some semantical conflicts between these extensions. In this article, we propose a framework to avid the conflicts. We provide a modular implementation of a reflective programming language based on monad transformers, and made its internal dependency of each component clear. And then, we propose a concrete mechanism to help a user who want to extend a language know enough informations to avoid possible conflicts.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

メタレベルアーキテクチャを採用するプログラムでは，通常，メタレベルは対象とする適応領域‐ベースレベルの構造やその拡張・適応方式等?に特化された形で設計される．メタレベル自体を，アプリケーションに依存した部分とそうでない部分に分離できれば，後者を再利用することによってメタレベル設計が容易になる．そのために，本稿では拡張が容易なメタレベルの設計をアプリケーションに依存せずに行なう方法について論じる．拡張を容易とするために必要なことは，安定で見通しが良い構造を導入し，その構造に従ってモジュールを組み上げていけるようにすることである．そこで，本稿ではメタレベルアーキテクチャ一般について成り立つ構造としてベースレベル記述の構文木を考え，その構造の上にモジュールを載せるという方法を提案する．ここで，この方法では一つの構文に複数のモジュールを相互作用なしに共存させることができ，また，モジュール間のインターフェースを変数の単一代入として定義することにより見通しの良いモジュール間通信を実現する．これにより，モジュールを容易に後から導入してメタレベルを拡張することが可能となる．この方法の適用例として，簡単な言語のインタプリタ，およびLRパーザジェネレータを示す．特に後者は（インタプリタやコンパイラなどの）典型的な言語処理系とは異なる構造のソフトウェアであるが，我々の方法はこのようなものにも適用できることを示す．Usually,a metalevel is designed for a specific application domain, especially when the metalevel is dedicated for extensibility because details of the extensibility are very application specific issues. The aim of this study is to extract characteristics common to all metalevel architectures and to establish a method for structuring a metalevel using the characteristics for extensibility of the metalevel. The methodology eases metalevel designs and itsextensions because it is applicable to most application domains since they are not depending to specific domains. The metalevel should be constructed by multiple modules organized as stable and open structures. VVe propose that the methodology structuring a metalevel by baselevel syntax and sticking semantic modules to the syntactic elements. Baselevel syntax is common characteristics for all metalevels since they have a definition of the baselevel and it contains the syntax definition. Therefore the structuring method is applicable to most metalevels. The modules interact with single assignment attributes defined for each edge of baselevel syntax tress. Since the attributes can be defined as many as required, multiple semantic modules can be sticked to on syntactic element without any interference.Consequently we can introduce new modules for extensions easily. This paper explains the methodology by examples including lambda calculus and LR parser generator.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

メタレベルアーキテクチャを採用するプログラムでは, 通常, メタレベルは対象とする適応領域-ベースレベルの構造やその拡張・適応方式等-に特化された形で設計される.メタレベル自体を, アプリケーションに依存した部分とそうでない部分に分離できれば, 後者を再利用することによってメタレベル設計が容易になる.そのために, 本稿では拡張が容易なメタレベルの設計をアプリケーションに依存せずに行なう方法について論じる.拡張を容易とするために必要なことは, 安定で見通しが良い構造を導入し, その構造に従ってモジュールを組み上げていけるようにすることである.そこで, 本稿ではメタレベルアーキテクチャ一般について成り立つ構造としてベースレベル記述の構文木を考え, その構造の上にモジュールを載せるという方法を提案する.ここで, この方法では一つの構文に複数のモジュールを相互作用なしに共存させることができ, また, モジュール間のインターフェースを変数

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

自己反映的なプログラミング言語は 言語自身を計算の対象として扱うことが可能な言語システムである.言語の実装レベルに相当する記述をメタレベルとして実際の計算に関する記述と分離することによって 実行時の状況に応じた動的な言語の拡張を 再利用可能なモジュールとして提供することが可能な枠組みであり 並列計算機や 分散計算機環境におけるアプリケーションの記述を簡潔におこなうことができる.しかし 自己反映的な言語を実装する場合 言語の内部構造をユーザーにどのようにして提示するかの選択によって その言語が提供する拡張性と実行効率とのトレードオフが生じる.実際の自己反映的な言語では 並列計算などの特定の用途に限った自己反映計算を提供する言語として設計されることが多く 実験的なものを除いては汎用的な用途に適した言語といけるようなものはない.本稿では 用途を限定しない自己反映的な言語の効率的な実装方法を提案したい.そこでそのような実装方法を提供するための枠組みとして Monad-Transformerをもちいた.本稿ではまず 自己反映的な言語のいくつかの形式を 拡張可能な機能ごとに独立したモジュールの組として定義するための枠組みを示し 次にプログラマーがプログラムの各局面に応じ 必要な拡張機能と実行効率を考慮した言語の実装形態を随時選択するためのインターフェイスを提案する.最後に実際の言語システムの構築における問題点などに関する考察をおこなう.Reflective programming languages are languages which enable user programs to run at the defining language level (meta-level), and act as a part of the interpreter. So reflective languages can provide high extensibility. But in fact, in most of implementations of such a language, the given way of extension is not flexible enough. Because in the traditional methodology of defining reflective language is structuring the language as a meta-circular interpreter, so if we try to provide extensibility as possible. The performance to execute such programs are too low to build practical applications. Some reflective systems restrict extensibility of the language, and solve meta-level computations at compile-time. But, if what we can do at meta-level is limited hardly, or extensions have effect on only statically, there is less advantage of reflection about extension. In this paper, we propose a modular implementation technique of reflective languages. To provide the mechanism, we define some language building-blocks. And then we build a meta-continuation based reflective language as an interpreter and a compiler for the normal (non-reflective) language. Our goal is designing interfaces to let the programmer possible to select the implementation of the reflective language and make user to be able to specify the language for the purpose of each program-pieces. So we conclude what is the most efficient combination of language modules for some domain.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

自己反映的なプログラミング言語は 言語自身を計算の対象として扱うことが可能な言語システムである.言語の実装レベルに相当する記述をメタレベルとして実際の計算に関する記述と分離することによって 実行時の状況に応じた動的な言語の拡張を 再利用可能なモジュールとして提供することが可能な枠組みであり 並列計算機や 分散計算機環境におけるアプリケーションの記述を簡潔におこなうことができる.しかし 自己反映的な言語を実装する場合 言語の内部構造をユーザーにどのようにして提示するかの選択によって その言語が提供する拡張性と実行効率とのトレードオフが生じる.実際の自己反映的な言語では 並列計算などの特定の用途に限った自己反映計算を提供する言語として設計されることが多く 実験的なものを除いては汎用的な用途に適した言語といけるようなものはない.本稿では 用途を限定しない自己反映的な言語の効率的な実装方法を提案したい.そこでそのような実装方法を提供するための枠組みとして Monad-Transformerをもちいた.本稿ではまず 自己反映的な言語のいくつかの形式を 拡張可能な機能ごとに独立したモジュールの組として定義するための枠組みを示し 次にプログラマーがプログラムの各局面に応じ 必要な拡張機能と実行効率を考慮した言語の実装形態を随時選択するためのインターフェイスを提案する.最後に実際の言語システムの構築における問題点などに関する考察をおこなう.Reflective programming languages are languages which enable user programs to run at the defining language level (meta-level), and act as a part of the interpreter. So reflective languages can provide high extensibility. But in fact, in most of implementations of such a language, the given way of extension is not flexible enough. Because in the traditional methodology of defining reflective language is structuring the language as a meta-circular interpreter, so if we try to provide extensibility as possible. The performance to execute such programs are too low to build practical applications. Some reflective systems restrict extensibility of the language, and solve meta-level computations at compile-time. But, if what we can do at meta-level is limited hardly, or extensions have effect on only statically, there is less advantage of reflection about extension. In this paper, we propose a modular implementation technique of reflective languages. To provide the mechanism, we define some language building-blocks. And then we build a meta-continuation based reflective language as an interpreter and a compiler for the normal (non-reflective) language. Our goal is designing interfaces to let the programmer possible to select the implementation of the reflective language and make user to be able to specify the language for the purpose of each program-pieces. So we conclude what is the most efficient combination of language modules for some domain.

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

本論文では、リフレクションの可能なプログラミング言語を利用して、CORBAのアプリケーション開発手順を簡略化する手法と、利用方法の複雑なCORBAのAPIを簡略化する手法を示す。リフレクションを利用することで、必要なスタブとスケルトンをアプリケーションの実行時に生成して取り込むことが可能になり、アプリケーションの開発手順を簡略化できる。さらに、リフレクションを利用することで、CORBAの遅延同期呼び出しやDynAny APIを利用する際のプログラミングの手間を削減できる。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

並行システムの動作の詳細を把握するのは一般的には困難である.本研究では, 並行システムの例として有機的プログラミング言語GAEAをとりあげる.本言語は有機的プログラミングと呼ばれる新しいソフトウェア構築方法論に基づいておりプログラムの動的変更や並行処理が可能である.この言語はPrologを基礎としてるので並列論理型プログラミング言語と考えることができる.そこで本言語は並行システムとみなし, そのシステムの計算状態や動作の明示的な記述を試みている.その記述は状態を持つ並行システムの動的変化が表現可能な書き換え論理を用いて与えている.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

開放型分散システム環境や移動計算機環境の普及にともない，さまざまな実行環境やその動的な状態変化に適応できるソフトウェアの必要性が高まっている．本稿では，そうした動的適応可能なソフトウェアのモデルおよびそれを構成するための言語LEADについて述べる．鍵となるアイディアは，1）手続き呼び出し時に，手続きの実行コードを実行環境の状態に応じて動的に切り替える機構を導入する，2）動的適応可能なソフトウェアをメタレベルアーキテクチャとして構成し，適応動作の記述と問題領域の記述を分離・独立させる，といった点にある．言語LEADは，このような動的に変化する手続きの定義，および制御の機構を言語機能として提供し，LEADによる動的適応可能なソフトウェアはメタレベルアーキテクチャを形成する．LEADを用いることで，1）拡張性の高い動的適応可能なソフトウェアの実現，2）既存ソフトウェアへの動的適応能力の導入，などが可能となる．A system has dynamic adaptability if it can adapt itself to dynamically changing runtime environments.As open-ended distributed systems and mobile computing systems have spread widely,the need for software with dynamic adaptability increases.We propose a model of software with dynamic adaptability and,we designed and implemented the language LEAD which constructs the model.The basic idea that we introduce the mechanism which changes procedure invocations dynamically depending on the states of runtime environments.The dynamically Adaptable software based on the model is realized as a meta-level architecture,and it separets the codes of dynamic adaptability from the codes of primary subject domain in the software.LEAD provides the mechanism as a language construct and,the dynamically adaptable software in LEAD forms meta-level architecture.Using LEAD,we can realize the followings:1)the highly extensible dynamically adaptable software,and 2)the introduction of the dynamic adaptability to the existing software.

CiNii Books

researchmap

その他リンク： http://id.nii.ac.jp/1001/00012969/

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

自己反映的なシステムにおいて、ユーザの言語拡張に関する記述の再利用を容易にする際に、再利用しようとしている拡張が、その時点における拡張と衝突する可能性がある。そのためシステムの設計者は、ユーザが言語の拡張を組み合わせて利用する際の安全性を考慮する必要があるが、実際にこうした衝突をまえもって特定することは困難であり、そのための枠組みが必要になる。本稿ではmonad trnasformerを利用した言語の構成手法に基づき、特に言語拡張のための記述と、その拡張された言語の機能を利用する可能性のある拡張とのあいだの関係に注目して、実際のシステムの構築例をあげそのなかで言語拡張のインターフェイスを制限するための方法について述べる。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人日本ソフトウェア科学会  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

分散・移動計算機環境における, 移動可能プログラムを記述するための一般的な言語機構を提案する. 基本的なアイデアは, 計算状態の一部を表現する部分接続(partial continuation)をプログラム中で一級オブジェクトとして明示的に扱うことにある. 並行計算系における継続(continuation)の扱いは一般に繁雑になるが, エクステントを限定した部分継続を得る言語機能を用いることにより, 遠隔コード実行の様々なパターンを記述できる. 本機構は手続きクロージャ, あるいはそれと等価な機構を持つ様々な逐次言語に導入可能であり, ユーザ向けのモバイルエージェント記述スクリプト言語だけでなく, システムプログラム記述言語にも適用可能である. 本稿では操作的意味について延べる.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

モバイルエージェントやJavaなどのWebページ記述用言語に代表される移動可能プログラムをいつでもどこでも計算機を使用可能とするモバイルコンピューティング環境と組み合わせることによって, 計算機の可能性は飛躍的に向上する. 本稿では, 移動可能プログラムと移動可能プログラムをモバイルコンピューティング環境上で実行するために必要となる適応可能なソフトウェアアーキテクチャに関して紹介する.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：北陸先端科学技術大学院大学  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

言語処理系を再利用可能な部品から構成し、その構成を言語内部にメタレベルアーキテクチャとして見せる方式を提案する。これにより、従来は困難だったメタレベル記述の再利用性を高めることができる。具体的にはインタプリタをモジュール化し、そのモジュール間の参照関係をDAGに制限することによって各モジュールの再利用を可能としている。また、インタプリタを単純にモジュール分割すると参照関係が複雑になり、再利用が不可能となることについても述べ、それを解決するためのInterpreter Passing Style (IPS) という手法についても触れる。

CiNii Books

researchmap

記述言語：英語   出版者・発行元：一般社団法人情報処理学会  

抽象書換え系を用いて,自己反映計算に対する形式的な定義を試みる.これは自己反映計算およびそれに関連した諸概念(例えばリフレクティブ・タワー等)に対する,特定の計算モデル・言語に依存しない形式的かつクリアーな定義方法を与えることを目的としている.本論文では,抽象書換え系に対する実現(implementation)の関係を定義し,それによって自己反映計算の定義を行っている.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

オブジェクト指向プログラミングにおけるソフトウェア開発において、クラスライブラリ、およびそれを有効に利用するための開発環境の役割は大変重要である。クラスライブラリを含めた開発環境を単なるソースコードのデータベースとしてだけ捉えるのではなく、情報を整理し、資産として再利用可能な形で蓄積してゆくための一手段として捉える必要がある。しかし、その一方でクラスライブラリを構成するための標準的な方法は示されておらず、設計者それぞれ固有のモデルに委ねられている。そのため利用者は、プログラミング言語の習得のみならず、各設計者によって作成されたクラスライブラリの理解をも強いられる。加えて、クラスライブラリは肥大化するばかりで、利用者の負担は増える一方である。ここに初心者がオブジェクト指向プログラミングになじめない理由の一つがある。そのためにも、クラスライブラリが備えるべき標準的な性質を設計者、利用者ともに認

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

近年の技術革新は電子装置の小型化、高性能化をもたらし、その製造技術の進歩はそれらの安価な実現を可能にした。またネットワークはパソコン通信などを通じて急速に個人の生活空間に浸透しつつある。小型化された携帯可能な電子装置とネットワーク、この2つの技術の融合により新しいコンピューティング環境、コンピューティングスタイルが生まれようとしている。このように移動可能な小型計算機をネットワークに接続し、分散環境と融合させた計算機環境を移動計算機環境という。移動計算機環境では移動による計算機を取り巻く環境の動的変化、計算機資源の制約等がシステムレベルの透過性実現を困難にしている。本研究ではこのような環境においてシステムレベルの透過性を実現する枠組として有効なメタレベルアーキテクチャで構成される言語を提案する。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

自己反映計算とは、通常の計算対象だけでなく計算を行なっている自己をも対象として計算を行なう、という概念である。自己反映的プログラミング言語とは、自己(動作中のプログラムや処理系の状態など)をその言語自身の枠組の中で扱うことができるようなプログラミング言語のことである。自己反映的なシステムでは、自己の構成、状態を動的に変更することが可能である。従って、自己反映的プログラミング言語は問題領域に合わせて自分自身をカスタマイズでき、柔軟なソフトウェアの構築に有用であることが認識されている。また、プログラム自体を扱う部分(メタレベル)と、問題を扱う部分(ベースレベル)に分けるという意味でモジュール化の促進を可能とする。本稿では、手続き的自己反映計算(ベースレベルを何らかのプログラムとすると、メタレベルをそのプログラムを実行するインタプリタとする枠組)において、モジュール化という側面を重視し、メタレベルの再利用

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

分散計算環境における大域的ガベージコレクションの一手法を提案する.本方式はリファレンスカウント方式とマーキング方式を併用したアルゴリズムを採用し,以下のような特長を持つ:(1)循環する参照を含むすべてのゴミを回収できる.(2)アプリケーションプログラムと並行に動作する.(3)比較的オーバーヘッドの高いマーキングフェーズの稼働率を低くおさえている.(4)リファレンス,構報,マーキング,終了判定のメッセージに重みを用いて,メッセージ数を減少させている.(5)集中制御を必要としない.本方式によるGCをCM-5,nCUBE/2上に実装し,他のアルゴリズムとの比較も行った.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

移動計算機を無線ネットワークを用いて分散環境と接続した移動計算機環境におけるアプリケーションは、メモリのサイズ、バッテリの量、ネットワークのバンド幅などの制約を考慮して実行する必要がある。そのため、アプリケーションやOSの構成力環境に応じて柔軟に変化しなければならない。本稿では、移動計算機環境に適した柔軟なソフトウェアの構築法の開発をめざすParsifalプロジェクトにおける柔軟なソフトウエアの構築法に関する概要を述べる。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

並行オブジェクト指向計算の新たな実行方式を考案した。本方式では並行オブジェクト指向計算を並行項書き換え計算に変換して実行する。実際の項の書き換えはグラフ簡約機械によって実現される。考案した実行システムでは、互いに通信を行なう複数のグラフ簡約機械を用いてグラフ簡約を並行に行なう。実行システムの状態は項で表すことができ、計算の進行は項の遷移で表わされる。その項の遷移が並行オブジェクト指向計算で許されている項の遷移であることを書き換え論理を用いて示し、実行システムの正当性を示す。

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

抽象書換え系を用いて,自己反映計算に対する形式的な定義を試みる.これは自己反映計算およびそれに関連した諸概念(例えばリフレクティブ・タワー等)に対する,特定の計算モデル・言語に依存しない形式的かつクリアーな定義方法を与えることを目的としている.本論文では,抽象書換え系に対する実現(implementation)の関係を定義し,それによって自己反映計算の定義を行っている.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：北陸先端科学技術大学院大学  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：北陸先端科学技術大学院大学  

CiNii Books

researchmap

researchmap

記述言語：日本語   掲載種別：書評論文，書評，文献紹介等   出版者・発行元：社団法人人工知能学会  

DOI： 10.11517/jjsai.2.4_536

CiNii Books

researchmap

記述言語：日本語   掲載種別：書評論文，書評，文献紹介等   出版者・発行元：情報処理学会  

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap