view note.txt @ 0:bcc24c3e3eb4

Add note
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 10 May 2016 20:04:09 +0900 (2016-05-10)
parents
children 10e66dfc382c
line wrap: on
line source
# 論文タイトル
和文: Verification method of programs using Continuation based C
英文: Continuation based C を用いたプログラムの検証手法

# 和文アブスト(600文字程度)
Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。
Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。
Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。
プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。
また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。
Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。
本論文では Continuatoin based C によって記述された赤黒木や Synchronized Queue といったデータ構造の性質を検証する。

# 英文アブスト(200 words) (ちょっと足りてない)
We propose a verification method for programs using Continuation based C language.
Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment.
Code segments that the calculation unit has input/output data segment that data unit.
Programs are represented by connections between code segment and code segment.
The output data segment of some code segment is converts to the input data segment of connected one.
Programming paradigm using Code segments splits main computations and complicated computations such as memory control, error handling and more to meta computations.
Meta computations represented to meta code segment and meta data segment, which saves main computations.
In this paper, We define a meta computation which connects code segments with verifications and verify properties of data structures such as Red-Black Tree and Synchironized Queue.