changeset 56:c361708587eb

Update slides
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 04 Aug 2016 18:53:59 +0900
parents 3d80db3be1b6
children 728bbe91b6a2
files presentation/slide.md
diffstat 1 files changed, 7 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.md	Thu Aug 04 18:46:58 2016 +0900
+++ b/presentation/slide.md	Thu Aug 04 18:53:59 2016 +0900
@@ -101,14 +101,13 @@
 ```
 
 # CbC のメタ計算の実際
-* Meta Code Segment では Data Segment は struct Data という形で一様に処理される
+* Meta Code Segment では Data Segment は struct Data という形で一様に処理
 * メタ計算と通常の計算は stub と meta によって接続される
 
 ```
 __code addTen_stub(struct Context* context) {
     goto addTen(context, context->data[Count]);
 }
-
 __code addTen(struct Context* context, struct Count c) {
     struct Port p;
     p.port = c.x+10;
@@ -118,7 +117,6 @@
 __code twice_stub(struct Context* context) {
     goto twice(context, countext->data[Port]);
 }
-
 __code twice(struct Context* countext, struct Port p) {
     p.x = p.x*2;
     goto meta(context, ShowValue);
@@ -127,7 +125,8 @@
 
 # CbC のメタ計算の実際
 * デフォルトの meta
-    * meta を変更することで平行計算や例外処理やソフトウェア検証を行なう
+    * Code Segment の接続先名から次に実行される Code Segment を決定する
+* meta を変更することで平行計算や例外処理やソフトウェア検証を行なう
 
 ```
 __code meta(struct Context* context, enum Code next) {
@@ -137,7 +136,7 @@
 
 
 
-# Meta Code Segment を使った実際の検証
+# Meta Code Segment を使った検証
 * goto する時に必ず通る Meta Code Segment `meta` を作る
 * `meta` を切り替えることでノーマルレベルの計算を拡張する
 
@@ -146,22 +145,12 @@
 struct Context {
     union Data *data;       // Data Segment
     unsigned int gotoCount; // メタ計算に必要なデータ
-    unsigned int stepOfAddTen;
 };
 
 // Meta Code Segment
 __code meta(struct Context* context, enum Code next) {
     countext.gotoCount++;
-
-    /* 接続時に行なうメタ計算を記述 */
-    switch (next) {
-        case AddTen:
-            // 特定のCode Segmentへのメタ計算
-            context.stepOfAddTen++;
-            goto addTen_stub(context);
-        case Twice:
-            goto twice_stub(context);
-    }
+    goto (context->code[next])(context);
 }
 ```
 
@@ -226,7 +215,7 @@
 * 挿入だけでなく削除を含む赤黒木の仕様検証
 * 状態の抽象化による探索の効率化
 * ポインタへの不正アクセス検出などの機能
-* CbC コンパイラに検証を行ないやすくする機構の導入
+* 検証用APIを CbC コンパイラに導入
 
 # CBMC Informations
 * CBMC 5.4
@@ -248,7 +237,7 @@
     * reflection in Java
 * 副作用などの言語処理系に依存した処理を表現する
     * Monad in Haskell
-* CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易になっている
+* CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易
 
 
 <!-- vim: set filetype=markdown.slide: -->