annotate user/soto/log/2021-05-18.md @ 62:0c5df5736436

backup 2021-05-19
author autobackup
date Wed, 19 May 2021 00:10:03 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
62
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
1 # 研究目的
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
2 - OSやアプリケーションの信頼性を高めることは重要な課題である。
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
3
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
4 - 研究室でCbCという言語を開発している。その信頼性を証明したい。
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
5
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
6 - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
7
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
8 - 課題として、CbC はC言語とアセンブラの中間に位置しているため、人がコーディングするのは困難となっている。
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
9
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
10 - GearsOS での実装と Gears Agda による実装の違いを極力無くすためにも Gears Agda からGearsOS の生成をしたい。
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
11
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
12 # 今週やったこと
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
13
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
14 - Agdaのreflectionについて調べた
0c5df5736436 backup 2021-05-19
autobackup
parents:
diff changeset
15