# 研究目的

• cbcについて

Continuation based C(CbC) は、C からループ制御構造とサブルーチンコールを取り除き、継続を導入した C の下位言語である。継続呼び出しは引数付き goto 文で表現される。

• Hoare Logicについて

事前条件 P を満足する時に、プログラム S を実行すると、その実行後には，事後条件 Q を満足する。プログラム S が終了すれば, プログラム実行の効果として、事前条件と事後条件との対によって表現した意図通りの結果が得られる。

• このCbCの継続の部分をHoareLogicで関数の実行を証明する、プログラムに使用されている関数一つ一つを独立して正常な実行の証明ができたなら、そのプログラムの正常な実行の証明となる

• 関数に与えられる引数を事前条件、関数実行後の戻り値を事後条件とし、CbCではこの事後条件が次の関数の引数とするので、次の関数の事前条件となる。実行を継続渡しで行うCbCのプログラム自体の検証ができる

• また、Hoare Logicの検証の中に「コマンドが停止すること」というものがある。これが外間さんの修論で説明していたもの(少し理解が足りていないのでもう少しみてみます…)

# 今週の進捗

• バイトの時間以外ずっとソフ演3のoauthをずっとやっていました。
• そしたら日曜日体調を崩しました。
• vscodeのagdaプラグインを調べました。

# sof3

node.jsでoauthを使ってユーザーの情報を管理したい。

ですが、自分のwebの理解が足りないのもあってユーザー情報(メールアドレスやトークン情報があるはず)を取得できていない。

文献が少ない感じなのでnode.js諦めてもうdjangoでやってしまおうかなという話も…

# VScodeのagdaプラグインについて

ここlanguage-agda - Visual Studio Marketplace を調べたのですがどうもシンタックスハイライトと記号のスニペットはあるらしいですが実行は対応していなさそうです。 コード

別手口でやるとしたら

• atomにプラグインをいれる方法と
• spaceemacsにvimのキーマップをいれる

などがありそうです(まだ詳しくは調べていません…)