# HG changeset patch
# User soto <soto@cr.ie.u-ryukyu.ac.jp>
# Date 1641613299 -32400
# Node ID 393c839f987b0205e66dbf8f4c46a5af90dd221c
# Parent  76c3378c61dc16620195136b8517d4f17422cbfa
DONE

diff -r 76c3378c61dc -r 393c839f987b slide/slide.md
--- 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 に渡して処理を行う。
 
diff -r 76c3378c61dc -r 393c839f987b slide/slide.pdf
Binary file slide/slide.pdf has changed