Mercurial > hg > Papers > 2021 > soto-prosym
changeset 14:393c839f987b default tip
DONE
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 08 Jan 2022 12:41:39 +0900 |
| parents | 76c3378c61dc |
| children | |
| files | slide/slide.md slide/slide.pdf |
| diffstat | 2 files changed, 1 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/slide/slide.md Sat Jan 08 09:53:19 2022 +0900 +++ b/slide/slide.md Sat Jan 08 12:41:39 2022 +0900 @@ -62,13 +62,12 @@ - 信頼性を高める手法として「モデル検査」や「定理証明」など - 当研究室でCbCという言語を開発している - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる -- 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った - 本研究では Gears Agda にて重要なアルゴリズムの一つである Red Black Tree を検証する # CbC について - CbCとは当研究室で開発しているC言語の下位言語 - - CbC とは C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入したC 言語の下位言語 - 継続呼び出しは引数付き goto 文で表現される。 + - 関数呼び出し時のスタックの操作を行わずjmp命令で次の処理に移動する - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語 - CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。