最終的な成績
Aでした
課題に関するファイル
1.1 論文管理ソフト
Agda に関する論文を探して Zoteroに登録する 登録したものの Bibtex を export して、それをレポートせよ 論文に対する短いコメントをつけること
Zoteroをダウンロードする
- 公式サイトからダウンロードする
- Chromeで作業する
- Chromeのエクステンション、「Zotero Connector」をインストールする
Agda に関する論文を探して Zoteroに登録する
- Google Scholarでagdaの論文を検索して登録するための論文を探す。
- 自分はGearsOSのHoare Logicをベースにした検証手法を選んだ。
- ZoteroのExtentionで論文をZoteroを保存する
登録したものの Bibtex を export して、それをレポートする
- ファイルが追加されていることを確認したら、Add to Collection → New Collection... → automatonと入力して保存
- ファイルを副クリックして、Export Item
- Eport Itemの設定
- assignment_1_1.bibとして保存
- 中身を
$ cat assignment_1.bib | pbcopyでもメモ帳で開いてでもいいので、クリップボードに張ってメールのレポートに貼る、bibファイルも添付する
@article{_gearsoshoare_2019,
title = {{GearsOSのHoare} {Logicをベースにした検証手法}},
volume = {IEICE-118},
url = {https://ken.ieice.org/ken/paper/20190116d1Jm/},
abstract = {Gears OS は継続を主とするプログラミング言語 CbC で記述されている。OS やアプリケーションの信頼性を上げるには仕様を満たしていることを確認する必要がある。現在 GearsOS の仕様の確認には定理証明系である Agda を用いている。CbC では関数呼び出しを用いず goto 文により遷移する。これは Agda 上では継続渡しの記述を用いた関数として記述する。また、継続にはある関数を実行するための事前条件や事後条件などをもたせることが可能である。Hoare Logic では事前条件が成り立っているときにある関数を実行して、それが停止する際に事後条件を満たすことを確認する。これは継続を用いた Agda 上では事前条件を継続で関数に渡し、関数からさらに継続した先で事後条件が成り立つという形で記述できる。本発表では GearsOS の仕様確認に Hoare Logic をベースとした記述と証明を導入する。},
language = {ja},
number = {IEICE-MSS-384,IEICE-SS-385},
urldate = {2023-02-11},
journal = {IEICE Conferences Archives},
author = {政尊, 外間 and 真治, 河野},
month = jan,
year = {2019},
note = {Publisher: The Institute of Electronics, Information and Communication Engineers},
pages = {IEICE--MSS},
}
論文に対する短いコメントをつける
while文を使ったプログラムが正しく機能することをagdaで証明しているところが興味深かった。 これがきっかけで卒論ではデータベースをcbcで実装し、その機能の信頼性をagdaで証明したものを書きたいと思った。
2.2 Agdaによる関数と証明
以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
解答
module record1 where
record _∧_ (A B : Set) : Set where
field
π1 : A
π2 : B
ex0 : {A B : Set} → A ∧ B → A
ex0 = _∧_.π1
ex1 : {A B : Set} → ( A ∧ B ) → A
ex1 a∧b = _∧_.π1 a∧b
open _∧_
ex0' : {A B : Set} → A ∧ B → A
ex0' = π1
ex1' : {A B : Set} → ( A ∧ B ) → A
ex1' a∧b = π1 a∧b
ex2 : {A B : Set} → ( A ∧ B ) → B
ex2 a∧b = π2 a∧b
-- [ A ]₁ [ B ]₂
-- ─────────────────────────────────────────── λ-elim
-- A ∧ B
-- ─────────────────────────────────────────── λ-intro₂
-- B → (A ∧ B)
-- ─────────────────────────────────────────── λ-intro₁
-- A → B → (A ∧ B)
ex3 : {A B : Set} → A → B → ( A ∧ B )
ex3 a b = record { π1 = a ; π2 = b }
-- [ A ]₁ [ A ]₂
-- ─────────────────────────────────────────── λ-elim
-- (A ∧ A)
-- ─────────────────────────────────────────── λ-intro₁
-- A → (A ∧ A)
ex4 : {A B : Set} → A → ( A ∧ A )
ex4 a = record { π1 = a ; π2 = a }
-- [B]₁ [C]₂
-- ───────────────────────────── λ-elim
-- [ A ]₁ (B∧C)
-- ─────────────────────────────────────────────────────────── λ-elim
-- A B C
-- ─────────────────────────────────────────────────────────── λ-elim
-- ( A ∧ B) C
-- ─────────────────────────────────────────────────────────── λ-elim
-- A ∧ (B∧C)
-- ─────────────────────────────────────────────────────────── λ-intro₁
-- ( A ∧ B ) ∧ C → A ∧ (B ∧ C)
ex5 : {A B C : Set} → ( A ∧ B ) ∧ C → A ∧ (B ∧ C)
ex5 a∧b∧c = record { π1 = π1 (π1 a∧b∧c) ; π2 = record { π1 = π2 (π1 a∧b∧c) ; π2 = π2 a∧b∧c } }
--
-- [(A → B ) ∧ ( B → C) ]₁
-- ──────────────────────────────────── π1
-- [(A → B ) ∧ ( B → C) ]₁ (A → B ) [A]₂
-- ──────────────────────────── π2 ─────────────────────── λ-elim
-- ( B → C) B
-- ─────────────────────────────────────────── λ-elim
-- C
-- ─────────────────────────────────────────── λ-intro₂
-- A → C
-- ─────────────────────────────────────────── λ-intro₁
-- ( (A → B ) ∧ ( B → C) ) → A → C
ex6 : {A B C : Set} → ( (A → B ) ∧ ( B → C) ) → A → C
ex6 x a = π2 x (π1 x a)
-- [ A ]₁ [ B ]₂
-- ──────────────────── λ-elim
-- B C
-- ─────────────────────────────────────────── λ-elim
-- C
-- ─────────────────────────────────────────── λ-intro₃
-- A → C
-- ─────────────────────────────────────────── λ-intro₂
-- ( B → C) → A → C
-- ─────────────────────────────────────────── λ-intro₁
-- (A → B ) → ( B → C) → A → C
ex6' : {A B C : Set} → (A → B ) → ( B → C) → A → C
ex6' = λ z z₁ z₂ → z₁ (z z₂)
実行
$ agda record1.agda && echo done done
5.1 正規表現
egrep / Perl などを使って、これらのパターンに対するテストプログラムを作成せよ。C で書くとどうなるか? C の regcomp を使ってみよ。
perlで実装する
use strict;
use warnings;
my $target = "Brouhaha!";
my $regex = '(h|a)aha*';
while ($target =~ m/$regex/g) {
my $match = $&;
my $start = $-[0];
my $end = $+[0];
print "pattern match succeeded\n";
print "Match: $match\n";
}
実行結果
$ perl regex_match.perl pattern match succeeded Match: haha
Cで実装する
#include <stdio.h>
#include <regex.h>
#include <stdlib.h>
#include <string.h>
int main(int argc, char *argv[]) {
regex_t preg;
int result, i, match_count;
regmatch_t *pmatch;
char *target = "Brouhaha!";
int target_len = strlen(target);
int offset = 0;
// Compile the regular expression pattern
result = regcomp(&preg, "(h|a)aha*", REG_EXTENDED);
if (result != 0) {
printf("fail to compile regex\n");
return 1;
}
// Perform the pattern matching
pmatch = malloc(sizeof(regmatch_t));
result = regexec(&preg, target + offset, 1, pmatch, 0);
match_count = 0;
while (result == 0 && offset < target_len) {
printf("pattern match succeeded\n");
printf("Match: %.*s\n", (int)(pmatch[0].rm_eo - pmatch[0].rm_so), target + offset + pmatch[0].rm_so);
match_count++;
offset += pmatch[0].rm_eo;
pmatch = realloc(pmatch, (match_count + 1) * sizeof(regmatch_t));
result = regexec(&preg, target + offset, 1, &pmatch[match_count], REG_NOTBOL);
}
if (result != REG_NOMATCH) {
printf("fail to execute regrex\n");
return 1;
}
free(pmatch);
regfree(&preg);
return 0;
}
実行結果:
$ gcc regex_match.c -o regex_match && ./regex_match pattern match succeeded Match: haha
6.1 正規表現の決定性オートマトンへの変換
以下の正規表現をDFAに変換せよ。 (1) (a*|b*)c (2) (a|b)*c (3) (a*|b*)c(a|b)*c (4) ((a*|b*)c)|((a|b)*c)
draw.ioなどで以下の図を再現して、svgで出力して学科ページに貼ればいいじゃないかと思う、それか画像を直接メールに添付でもいいかもしれないがどうだろう...?
一応、学科ページにdraw.ioで再利用可能なxmlファイルとsvgファイルをアップロードした、ご自由に再利用してください
index.html
<!doctype html>
<html lang="ja">
<head>
<meta charset="UTF-8">
<title>automaton 6.1</title>
</head>
<body>
<h1>automaton 6.1</h1>
<hr>
<h2>(1) (a*|b*)c</h2>
<img src="images/6.1.1.svg">
<a href="download/6.1.1.xml" download>xmlファイルのダウンロード</a>
<hr>
<h2>(2) (a|b)*c</h2>
<img src="images/6.1.2.svg">
<a href="download/6.1.2.xml" download>xmlファイルのダウンロード</a>
<hr>
<h2>(3) (a*|b*)c(a|b)*c</h2>
<img src="images/6.1.3.svg">
<a href="download/6.1.3.xml" download>xmlファイルのダウンロード</a>
<hr>
<h2>(4) ((a*|b*)c)|((a|b)*c)</h2>
<img src="images/6.1.4.svg">
<a href="download/6.1.4.xml" download>xmlファイルのダウンロード</a>
</body>
</html>
ファイル構成
+amane+e205723 ls download/ images/ index.html +amane+e205723 ls download 6.1.1.xml 6.1.2.xml 6.1.3.xml 6.1.4.xml +amane+e205723 ls images 6.1.1.svg 6.1.2.svg 6.1.3.svg 6.1.4.svg +amane+e205723 pwd /home/student/e20/e205723/public_html/automaton/6-1
- (1)
(a*|b*)c - (2)
(a|b)*c - (3)
(a*|b*)c(a|b)*c - (4)
((a*|b*)c)|((a|b)*c)
