Mercurial > hg > Papers > 2023 > soto-master
changeset 8:d4f3d9d283a2
...
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 23 Jan 2023 13:18:37 +0900 |
| parents | c821e707a5ee |
| children | 0504b43c3670 |
| files | DPP/ModelChecking.agda Paper/master_paper.pdf Paper/master_paper.tex Paper/src/escape_agda.rb Paper/tex/abst.tex midterm/midterm.blg midterm/midterm.dvi midterm/midterm.fdb_latexmk midterm/midterm.log midterm/midterm.pdf midterm/midterm.synctex.gz |
| diffstat | 11 files changed, 132 insertions(+), 105 deletions(-) [+] |
line wrap: on
line diff
--- a/DPP/ModelChecking.agda Sun Jan 22 21:20:59 2023 +0900 +++ b/DPP/ModelChecking.agda Mon Jan 23 13:18:37 2023 +0900 @@ -614,7 +614,7 @@ ... | [] = exit origin ... | env1 ∷ envl with DG x ... | [] = loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit - ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x); is-step = boolor (is-step me) (is-step x) } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit ) + ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x); is-step = true } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit ) eq-env origin [] [] exit loop = exit origin -- true eq-env origin [] (x ∷ pl2) exit loop = loop false @@ -624,7 +624,7 @@ eq-pid origin pl1 pl2 p1 p2 next1 exit1 with <-cmp (pid p1) (pid p2) ... | tri< a ¬b ¬c = exit1 false ... | tri> ¬a ¬b c = exit1 false - ... | tri≈ ¬a b ¬c = eq-lhand origin pl1 pl2 p1 p2 next1 exit1 + ... | tri≈ ¬a b ¬c = eq-lhand origin pl1 pl2 p1 p2 next1 exit1 eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 with (left-hand phi1) ... | sss with (left-hand phi2) @@ -632,7 +632,7 @@ eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | false = exit1 false eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | true = exit1 false eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | false = eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 - + eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 with (right-hand phi1) ... | sss with (right-hand phi2) eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | true = eq-next-code origin pl1 pl2 phi1 phi2 next1 exit1 @@ -744,7 +744,7 @@ test-dead-lock-loop : MetaEnv2 → MetaEnv2 test-dead-lock-loop metaenv2 = branch-search-meta2 metaenv2 (λ me1 → testhoge me1 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 me2 (λ me4 → test-dead-lock-loop me4) ) (λ e → e)) ) (λ e → e) --- test-dead-lock-loop test-metaenv2 +-- test-dead-lock-loop test-metaenv3 test-step-c2 : List (List Env) test-step-c2 = init-brute-force (record {
--- a/Paper/master_paper.tex Sun Jan 22 21:20:59 2023 +0900 +++ b/Paper/master_paper.tex Mon Jan 23 13:18:37 2023 +0900 @@ -120,6 +120,7 @@ \input{tex/cbc_agda.tex} + \chapter{Gears Agda による定理証明} \input{tex/hoare.tex} \input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
--- a/Paper/src/escape_agda.rb Sun Jan 22 21:20:59 2023 +0900 +++ b/Paper/src/escape_agda.rb Mon Jan 23 13:18:37 2023 +0900 @@ -31,7 +31,7 @@ code = File.read(FileName) ReplaceTable.each do |k, v| escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar - code = code.gsub(k, escaped_str) + code = code.force_encoding("UTF-8").gsub(k, escaped_str) end File.write(FileName.sub(/.agda$/, Suffix), code)
--- a/Paper/tex/abst.tex Sun Jan 22 21:20:59 2023 +0900 +++ b/Paper/tex/abst.tex Mon Jan 23 13:18:37 2023 +0900 @@ -1,9 +1,39 @@ \chapter*{要旨} -当研究室では Continuation based C （CbC） という言語を用いて，拡張性と信頼性を両立する OS である Gears OS を開発している． -CbC とは， C 言語から通常の関数呼び出しではなく，アセンブラでいう jmp 命令により関数を遷移する継続を導入した C 言語の下位言語である． -すでに Gears OS はメタ計算によるモデル検査機構を持っている． -GearsOS の CodeGear/DataGear は Gears Agda により形式証明に向いた形に記述することができる． -モデル検査機構を Gears Agda により記述することで HoareLogic 的な逐次実行型のプログラムの証明だけでなく，並行実行を含むプログラムの証明が可能になる． +開発手法の一つとして，形式手法というものがある． +形式手法とはプログラムの仕様を形式化，つまり数学的な記述を行い， +書いたプログラムがそれを満たしているか検証を行う手法である． +代表的な形式の検証手法として，定理証明やモデル検査が挙げられる． + +形式手法で開発したプログラムは数学的に正しいことが証明されている， +そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている． +しかし、一見完璧な手法であるように思えるが欠点として，膨大なコストを要する． +シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用せずとも良いとなる． + +そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する． +Gears Agdaとは当研究室で開発している Continuation based C (CbC) の概念を +取り入れた記法で記述された Agdaのことである． +通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する． +この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了し， +メインルーチンに戻る際にスタックしていた環境に戻す流れとなる． +CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができ， +環境をスタックに保持しない． +したがって関数の実行では暗黙な環境が存在せず，関数は受け取った引数のみを使用する． +この関数の単位を Code Gear と呼び，Code Gearの引数を Data Gear と呼んでいる． + +定理証明によるプログラムの検証は一般的に難易度が高いが， +これにより検証を Code Gear 単位に分割することができ，比較的容易に検証を行えるようになっている．\cite{ryokka-sigos} + +しかし，定理証明では並行処理の検証は困難である。加えて、往々にして定理証明による検証自体が複雑である． +そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした． +CbCの継続の概念はモデル検査とも相性がよい． +CbCが末尾関数呼び出しであるため Code Gear をそのまま +モデルの edge として定義することができるためである． + +定理証明支援機である Agda でモデル検査をするのは実行時間が掛かる点が困難である． +しかし，Gears Agda で 書いたプログラムをCbCに変換する事ができれば， +高速かつ Gears Agda で証明されたモデル検査器を動作させることができる． + +これらのことから，本紙では Gears Agda の定理証明とモデル検査での検証手法について述べる \chapter*{Abstract} We are developing Gears OS, a scalable and reliable OS, using the Continuation based C (CbC) language.
--- a/midterm/midterm.blg Sun Jan 22 21:20:59 2023 +0900 +++ b/midterm/midterm.blg Mon Jan 23 13:18:37 2023 +0900 @@ -1,4 +1,4 @@ -This is pBibTeX, Version 0.99d-j0.34 (utf8.euc) (TeX Live 2022/Arch Linux) +This is pBibTeX, Version 0.99d-j0.34 (TeX Live 2022/Arch Linux) Capacity: max_strings=200000, hash_size=200000, hash_prime=170003 The top-level auxiliary file: midterm.aux The style file: jplain.bst
--- a/midterm/midterm.fdb_latexmk Sun Jan 22 21:20:59 2023 +0900 +++ b/midterm/midterm.fdb_latexmk Mon Jan 23 13:18:37 2023 +0900 @@ -1,18 +1,18 @@ # Fdb version 3 -["bibtex midterm"] 1667989476 "midterm.aux" "midterm.bbl" "midterm" 1671461095 +["bibtex midterm"] 1674181838 "midterm.aux" "midterm.bbl" "midterm" 1674182852 "jplain.bst" 0 -1 0 "" - "midterm.aux" 1671461094 9691 9dc76a5c1a7654bf02e33626f7e4e1fe "latex" - "reference.bib" 1667976328 2038 e322cf6e682730289f2dd7f920509ed3 "" + "midterm.aux" 1674182852 9691 9dc76a5c1a7654bf02e33626f7e4e1fe "latex" + "reference.bib" 1673523108 2038 e322cf6e682730289f2dd7f920509ed3 "" (generated) "midterm.bbl" "midterm.blg" -["dvipdf"] 1671461095 "midterm.dvi" "midterm.pdf" "midterm" 1671461095 - "midterm.dvi" 1671461094 121456 5e2fc4f7316db880dcc6878a55ea4fb6 "latex" +["dvipdf"] 1674182852 "midterm.dvi" "midterm.pdf" "midterm" 1674182852 + "midterm.dvi" 1674182852 121460 ca1550b819f37fdceb911b81eaef5825 "latex" (generated) "midterm.pdf" -["latex"] 1671461093 "/home/soto/lab/soto-master/midterm/midterm.tex" "midterm.dvi" "midterm" 1671461095 +["latex"] 1674182851 "/home/soto/lab/soto-master/midterm/midterm.tex" "midterm.dvi" "midterm" 1674182852 "/dev/null" 0 -1 0 "" - "/home/soto/lab/soto-master/midterm/midterm.tex" 1667989918 4443 ac7cff74ca1f1b1ceca914a34084b307 "" + "/home/soto/lab/soto-master/midterm/midterm.tex" 1674182851 4443 ac7cff74ca1f1b1ceca914a34084b307 "" "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1650183167 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm" 1650183167 3584 adb004a0c8e7c46ee66cad73671f37b4 "" "/usr/share/texmf-dist/fonts/tfm/ptex-fonts/jis/jis.tfm" 1650180894 468 53f854284f6afa6c36aaa2d1090ecc12 "" @@ -147,42 +147,42 @@ "/usr/share/texmf-dist/tex/platex/jsclasses/jsarticle.cls" 1650180894 60810 5a58feea6fbea0a330b0ddfb4da256c4 "" "/usr/share/texmf-dist/tex/platex/jsclasses/jslogo.sty" 1650180894 5585 8e4615c54073c390d14154b29cee89cb "" "/usr/share/texmf-dist/web2c/texmf.cnf" 1650183167 39911 2da6c67557ec033436fe5418a70a8a61 "" - "/var/lib/texmf/web2c/eptex/platex.fmt" 1669632381 2965514 90a21d410561c98b20c2108bfda034f1 "" - "fig/Dining.pdf" 1664121780 126415 635fdfd0d90894b78e5da1c3af0ef19f "" - "fig/cbc_codegear.pdf" 1664121780 30110 abae9d544b613e6b77036cde8327a20f "" - "fig/rbt-stack.pdf" 1664121780 35233 d7920c7c7df9157f95299a7f4e75eab1 "" - "midterm.aux" 1671461094 9691 9dc76a5c1a7654bf02e33626f7e4e1fe "latex" - "midterm.bbl" 1667989476 1313 b652851d814c7bc492886f8e261b899c "bibtex midterm" - "midterm.tex" 1667989918 4443 ac7cff74ca1f1b1ceca914a34084b307 "" - "src/agda-dpp-impl.agda.replaced" 1664121780 2824 60454fbbf20d18849d1886385e94384b "" - "src/agda-term3.agda.replaced" 1664121780 545 fdcfb18f920181460a7dba32dfc82b76 "" - "src/agda/cbc-agda.agda.replaced" 1664121780 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 "" - "src/bt_impl/bt_env.agda.replaced" 1664121780 353 1c4e0e30a709998b56db02c2f5d79780 "" - "src/bt_impl/find.agda.replaced" 1664121780 1017 120c547ff4935d56838e621ce824a258 "" - "src/bt_impl/replace.agda.replaced" 1664121780 1131 b092504fc6ac756e2fbafad089102c4d "" - "src/bt_verif/find.agda.replaced" 1664121780 1169 e618092a068341b93eff11f09d6ee8e8 "" - "src/bt_verif/invariant.agda.replaced" 1664121780 1554 1a34c6377eeb4a8d839f72f44c2220eb "" - "src/cong.agda.replaced" 1664121780 136 bf35542f9064a29abc6adfff9cfb784b "" - "src/while_loop_impl/init_cg.agda.replaced" 1664121780 199 5c5a3c6d6e6a6d4a279ada436c797296 "" - "src/while_loop_impl/while_loop.agda.replaced" 1664121780 328 7d561a310d10a8a26e729559c2f4620e "" - "src/while_loop_impl/while_loop_c.agda.replaced" 1664121780 163 c00e91bf1ef0a8966c469c12c701c460 "" - "src/while_loop_impl/while_loop_dg.agda.replaced" 1664121780 92 7e17d15edce71eaef36d5d311f68d282 "" - "src/while_loop_verif/conversion.agda.replaced" 1664121780 867 42d0ed84921bff8ffdb7809e813c1018 "" - "src/while_loop_verif/init_cg.agda.replaced" 1664121780 504 91b9fe466d573b36634dc607908393ee "" - "src/while_loop_verif/verif.agda.replaced" 1664121780 437 6c5dfc7d29b2908db012b323213a7128 "" - "src/while_loop_verif/verif_loop.agda.replaced" 1664121780 1608 5cd1297a91876bf46fe092a67fd87f14 "" - "src/while_loop_verif/verif_term.agda.replaced" 1664121780 454 1f4765e0583409582bd37aa61bb228c9 "" - "src/while_loop_verif/while_loop.agda.replaced" 1664121780 1960 d3a6e8723403b7a76ca1dc6ea908d8d4 "" - "src/zero.agda.replaced" 1664121780 129 675f0cf5ad7344a43a79ac668f3582db "" - "tex/abst.tex" 1664121780 804 dfdd078293313e443c8f6f0b3476fbe7 "" - "tex/agda.tex" 1667976379 3088 63bdb2959c70d67a936861e8b2ca6bb2 "" - "tex/cbc.tex" 1664121780 2253 b995cbd082eafbc6aa946f8e4f2d1282 "" - "tex/cbc_agda.tex" 1667976725 4716 8817f826dcbb2cfe878c4afa3e46edc2 "" - "tex/dpp_impl.tex" 1664121780 6068 394a5d01cca5dcbce71d77b68b2248ea "" - "tex/hoare.tex" 1664466103 1479 f8f833313b878158593b45caee920df6 "" - "tex/intro.tex" 1667978138 3255 d8794f354118496c4aed62d0f2fda2c9 "" - "tex/tree_desc.tex" 1664466103 5282 d716a5b3b4aec10d70acd1c891f9fe06 "" - "tex/while_loop.tex" 1664121780 5277 057f958d94215589f0e7213efe2c5d99 "" + "/var/lib/texmf/web2c/eptex/platex.fmt" 1674180554 2965511 fd0c6aaf4b945d546628d161b3afb45b "" + "fig/Dining.pdf" 1673523108 126415 635fdfd0d90894b78e5da1c3af0ef19f "" + "fig/cbc_codegear.pdf" 1673523108 30110 abae9d544b613e6b77036cde8327a20f "" + "fig/rbt-stack.pdf" 1673523108 35233 d7920c7c7df9157f95299a7f4e75eab1 "" + "midterm.aux" 1674182852 9691 9dc76a5c1a7654bf02e33626f7e4e1fe "latex" + "midterm.bbl" 1674181838 1313 b652851d814c7bc492886f8e261b899c "bibtex midterm" + "midterm.tex" 1674182851 4443 ac7cff74ca1f1b1ceca914a34084b307 "" + "src/agda-dpp-impl.agda.replaced" 1673523108 2824 60454fbbf20d18849d1886385e94384b "" + "src/agda-term3.agda.replaced" 1673523108 545 fdcfb18f920181460a7dba32dfc82b76 "" + "src/agda/cbc-agda.agda.replaced" 1673523108 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 "" + "src/bt_impl/bt_env.agda.replaced" 1673523108 353 1c4e0e30a709998b56db02c2f5d79780 "" + "src/bt_impl/find.agda.replaced" 1673523108 1017 120c547ff4935d56838e621ce824a258 "" + "src/bt_impl/replace.agda.replaced" 1673523108 1131 b092504fc6ac756e2fbafad089102c4d "" + "src/bt_verif/find.agda.replaced" 1673523108 1169 e618092a068341b93eff11f09d6ee8e8 "" + "src/bt_verif/invariant.agda.replaced" 1673523108 1554 1a34c6377eeb4a8d839f72f44c2220eb "" + "src/cong.agda.replaced" 1673523108 136 bf35542f9064a29abc6adfff9cfb784b "" + "src/while_loop_impl/init_cg.agda.replaced" 1673523108 199 5c5a3c6d6e6a6d4a279ada436c797296 "" + "src/while_loop_impl/while_loop.agda.replaced" 1673523108 328 7d561a310d10a8a26e729559c2f4620e "" + "src/while_loop_impl/while_loop_c.agda.replaced" 1673523108 163 c00e91bf1ef0a8966c469c12c701c460 "" + "src/while_loop_impl/while_loop_dg.agda.replaced" 1673523108 92 7e17d15edce71eaef36d5d311f68d282 "" + "src/while_loop_verif/conversion.agda.replaced" 1673523108 867 42d0ed84921bff8ffdb7809e813c1018 "" + "src/while_loop_verif/init_cg.agda.replaced" 1673523108 504 91b9fe466d573b36634dc607908393ee "" + "src/while_loop_verif/verif.agda.replaced" 1673523108 437 6c5dfc7d29b2908db012b323213a7128 "" + "src/while_loop_verif/verif_loop.agda.replaced" 1673523108 1608 5cd1297a91876bf46fe092a67fd87f14 "" + "src/while_loop_verif/verif_term.agda.replaced" 1673523108 454 1f4765e0583409582bd37aa61bb228c9 "" + "src/while_loop_verif/while_loop.agda.replaced" 1673523108 1960 d3a6e8723403b7a76ca1dc6ea908d8d4 "" + "src/zero.agda.replaced" 1673523108 129 675f0cf5ad7344a43a79ac668f3582db "" + "tex/abst.tex" 1673523108 804 dfdd078293313e443c8f6f0b3476fbe7 "" + "tex/agda.tex" 1673523108 3088 63bdb2959c70d67a936861e8b2ca6bb2 "" + "tex/cbc.tex" 1673523108 2253 b995cbd082eafbc6aa946f8e4f2d1282 "" + "tex/cbc_agda.tex" 1673523108 4716 8817f826dcbb2cfe878c4afa3e46edc2 "" + "tex/dpp_impl.tex" 1673523108 6068 394a5d01cca5dcbce71d77b68b2248ea "" + "tex/hoare.tex" 1673523108 1479 f8f833313b878158593b45caee920df6 "" + "tex/intro.tex" 1673523108 3255 d8794f354118496c4aed62d0f2fda2c9 "" + "tex/tree_desc.tex" 1673523108 5282 d716a5b3b4aec10d70acd1c891f9fe06 "" + "tex/while_loop.tex" 1673523108 5277 057f958d94215589f0e7213efe2c5d99 "" (generated) "midterm.aux" "midterm.dvi"
--- a/midterm/midterm.log Sun Jan 22 21:20:59 2023 +0900 +++ b/midterm/midterm.log Mon Jan 23 13:18:37 2023 +0900 @@ -1,7 +1,6 @@ -This is e-pTeX, Version 3.141592653-p4.0.0-220214-2.6 (utf8.euc) (TeX Live 2022/Arch Linux) (preloaded format=platex 2022.11.28) 19 DEC 2022 23:44 +This is e-pTeX, Version 3.141592653-p4.0.0-220214-2.6 (utf8.euc) (TeX Live 2022/Arch Linux) (preloaded format=platex 2023.1.20) 20 JAN 2023 11:47 entering extended mode \write18 enabled. - file:line:error style messages enabled. %&-line parsing enabled. **/home/soto/lab/soto-master/midterm/midterm.tex (/home/soto/lab/soto-master/midterm/midterm.tex @@ -48,12 +47,12 @@ \heisei=\count192 ) (/usr/share/texmf-dist/tex/latex/geometry/geometry.sty Package: geometry 2020/01/02 v5.9 Page Geometry - (/usr/share/texmf-dist/tex/latex/graphics/keyval.sty +(/usr/share/texmf-dist/tex/latex/graphics/keyval.sty Package: keyval 2014/10/28 v1.15 key=value parser (DPC) \KV@toks@=\toks17 ) (/usr/share/texmf-dist/tex/generic/iftex/ifvtex.sty Package: ifvtex 2019/10/25 v1.7 ifvtex legacy package. Use iftex instead. - (/usr/share/texmf-dist/tex/generic/iftex/iftex.sty +(/usr/share/texmf-dist/tex/generic/iftex/iftex.sty Package: iftex 2022/02/03 v1.0f TeX engine tests )) \Gm@cnth=\count193 @@ -124,7 +123,7 @@ \lst@newlines=\count266 \lst@lineno=\count267 \lst@maxwidth=\dimen171 - (/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty +(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty File: lstmisc.sty 2020/03/24 1.8d (Carsten Heinz) \c@lstnumber=\count268 \lst@skipnumbers=\count269 @@ -133,24 +132,24 @@ File: listings.cfg 2020/03/24 1.8d listings configuration )) Package: listings 2020/03/24 1.8d (Carsten Heinz) - (/usr/share/texmf-dist/tex/latex/graphics/graphicx.sty +(/usr/share/texmf-dist/tex/latex/graphics/graphicx.sty Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR) - (/usr/share/texmf-dist/tex/latex/graphics/graphics.sty +(/usr/share/texmf-dist/tex/latex/graphics/graphics.sty Package: graphics 2021/03/04 v1.4d Standard LaTeX Graphics (DPC,SPQR) - (/usr/share/texmf-dist/tex/latex/graphics/trig.sty +(/usr/share/texmf-dist/tex/latex/graphics/trig.sty Package: trig 2021/08/11 v1.11 sin cos tan (DPC) ) (/usr/share/texmf-dist/tex/latex/graphics-cfg/graphics.cfg File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration ) Package graphics Info: Driver file: dvipdfmx.def on input line 107. - (/usr/share/texmf-dist/tex/latex/graphics-def/dvipdfmx.def +(/usr/share/texmf-dist/tex/latex/graphics-def/dvipdfmx.def File: dvipdfmx.def 2022/04/12 v5.0k Graphics/color driver for dvipdfmx )) \Gin@req@height=\dimen172 \Gin@req@width=\dimen173 ) (/usr/share/texmf-dist/tex/latex/ascmac/ascmac.sty Package: ascmac 2020/01/15 v2.1 ascmac wrapper (community edition) - (/usr/share/texmf-dist/tex/latex/ascmac/tascmac.sty +(/usr/share/texmf-dist/tex/latex/ascmac/tascmac.sty Package: tascmac 2020/01/15 v2.1 ascmac package (community edition) \@savetbaselineshift=\dimen174 \@saveybaselineshift=\dimen175 @@ -172,11 +171,10 @@ )) (/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty Package: amsmath 2021/10/15 v2.17l AMS math features \@mathmargin=\skip50 - For additional information on amsmath, use the `?' option. (/usr/share/texmf-dist/tex/latex/amsmath/amstext.sty Package: amstext 2021/08/26 v2.01 AMS text - (/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty +(/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty File: amsgen.sty 1999/11/30 v2.0 generic functions \@emptytoks=\toks21 \ex@=\dimen180 @@ -225,7 +223,7 @@ LaTeX Info: Redefining \] on input line 2939. ) (/usr/share/texmf-dist/tex/latex/amsfonts/amssymb.sty Package: amssymb 2013/01/14 v3.01 AMS font symbols - (/usr/share/texmf-dist/tex/latex/amsfonts/amsfonts.sty +(/usr/share/texmf-dist/tex/latex/amsfonts/amsfonts.sty Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support \symAMSa=\mathgroup6 \symAMSb=\mathgroup7 @@ -248,7 +246,7 @@ (Font) JY1/gt/m/n --> JY1/hgt/m/n on input line 325. LaTeX Font Info: Overwriting math alphabet `\mathgt' in version `bold' (Font) JY1/hgt/m/n --> JY1/hgt/bx/n on input line 326. - (/usr/share/texmf-dist/tex/platex/japanese-otf/ajmacros.sty +(/usr/share/texmf-dist/tex/platex/japanese-otf/ajmacros.sty Package: ajmacros 2019/04/01 21:00 iNOUE Koich! <inoue@ma.ns.musashi-tech.ac.jp> \@tempcntc=\count283 \@tempcntd=\count284 @@ -267,20 +265,20 @@ Package: cite 2015/02/27 v 5.5 ) (/usr/share/texmf-dist/tex/latex/svg/svg.sty Package: svg 2020/11/26 v2.02k (include SVG pictures) - (/usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +(/usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty Package: scrbase 2021/11/13 v3.35 KOMA-Script package (KOMA-Script-independent basics and keyval usage) - (/usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +(/usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty Package: scrlfile 2021/11/13 v3.35 KOMA-Script package (file load hooks) - (/usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +(/usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty Package: scrlfile-hook 2021/11/13 v3.35 KOMA-Script package (using LaTeX hooks) - (/usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +(/usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty Package: scrlogo 2021/11/13 v3.35 KOMA-Script package (logo) ))) Applying: [2021/05/01] Usage of raw or classic option list on input line 252. Already applied: [0000/00/00] Usage of raw or classic option list on input line 368. ) (/usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO) - (/usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +(/usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty Package: infwarerr 2019/12/03 v1.5 Providing info/warning/error messages (HO) ) (/usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty Package: ltxcmds 2020-05-10 v1.25 LaTeX kernel commands for general use (HO) @@ -295,16 +293,16 @@ Package shellesc Info: Unrestricted shell escape enabled on input line 75. ) (/usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty Package: ifplatform 2017/10/13 v0.4a Testing for the operating system - (/usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +(/usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty Package: catchfile 2019/12/09 v1.8 Catch the contents of a file (HO) - (/usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +(/usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty Package: etexcmds 2019/12/15 v1.7 Avoid name clashes with e-TeX commands (HO) )) (/usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty Package: ifluatex 2019/10/25 v1.5 ifluatex legacy package. Use iftex instead. ) runsystem(uname -s > "midterm.w18")...executed. - (./midterm.w18) +(./midterm.w18) runsystem(rm -- "midterm.w18")...executed. ) @@ -313,11 +311,11 @@ \c@svg@param@currpage=\count288 ) (/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty Package: xcolor 2021/10/31 v2.13 LaTeX color extensions (UK) - (/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg +(/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg File: color.cfg 2016/01/02 v1.6 sample color configuration ) Package xcolor Info: Driver file: dvips.def on input line 227. - (/usr/share/texmf-dist/tex/latex/graphics-def/dvips.def +(/usr/share/texmf-dist/tex/latex/graphics-def/dvips.def File: dvips.def 2017/06/20 v3.1d Graphics/color driver for dvips ) Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1352. @@ -331,23 +329,22 @@ ) (/usr/share/texmf-dist/tex/latex/transparent/transparent.sty Package: transparent 2019/11/29 v1.4 Transparency via pdfTeX's color stack (HO) - Package transparent Warning: Loading aborted, because pdfTeX is not running in PDF mode. ) (/usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty (/usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex \pgfutil@everybye=\toks26 \pgfutil@tempdima=\dimen189 \pgfutil@tempdimb=\dimen190 - (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex)) (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def +(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex)) (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def \pgfutil@abb=\box82 ) (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex (/usr/share/texmf-dist/tex/generic/pgf/pgf.revision.tex) Package: pgfrcs 2021/05/15 v3.1.9a (3.1.9a) )) (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex Package: pgfsys 2021/05/15 v3.1.9a (3.1.9a) - (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex \pgfkeys@pathtoks=\toks27 \pgfkeys@temptoks=\toks28 - (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex +(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex \pgfkeys@tmptoks=\toks29 )) \pgf@x=\dimen191 @@ -370,13 +367,13 @@ \t@pgf@tokb=\toks31 \t@pgf@tokc=\toks32 \pgf@sys@id@count=\count293 - (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg +(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg File: pgf.cfg 2021/05/15 v3.1.9a (3.1.9a) ) Driver file for pgf: pgfsys-dvips.def - (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-dvips.def +(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-dvips.def File: pgfsys-dvips.def 2021/05/15 v3.1.9a (3.1.9a) - (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-postscript.def +(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-postscript.def File: pgfsys-common-postscript.def 2021/05/15 v3.1.9a (3.1.9a) \pgf@objectcount=\count294 ))) (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex @@ -391,7 +388,7 @@ File: lstmisc.sty 2020/03/24 1.8d (Carsten Heinz) ) (/usr/share/texmf-dist/tex/latex/caption/caption.sty Package: caption 2022/03/01 v3.6b Customizing captions (AR) - (/usr/share/texmf-dist/tex/latex/caption/caption3.sty +(/usr/share/texmf-dist/tex/latex/caption/caption3.sty Package: caption3 2022/03/17 v2.3b caption3 kernel (AR) \caption@tempdima=\dimen257 \captionmargin=\dimen258 @@ -419,7 +416,7 @@ LaTeX Font Info: Font shape `JY1/hmc/m/n' will be (Font) scaled to size 9.24683pt on input line 52. LaTeX Font Info: Trying to load font information for T1+lmr on input line 52. - (/usr/share/texmf-dist/tex/latex/lm/t1lmr.fd +(/usr/share/texmf-dist/tex/latex/lm/t1lmr.fd File: t1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) (/usr/share/texmf-dist/tex/latex/l3backend/l3backend-dvips.def File: l3backend-dvips.def 2022-04-14 L3 backend support: dvips @@ -467,7 +464,6 @@ LaTeX Font Info: ... okay on input line 52. LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 52. LaTeX Font Info: ... okay on input line 52. - *geometry* driver: auto-detecting *geometry* detected driver: dvips *geometry* verbose mode - [ preamble ] result: @@ -524,7 +520,7 @@ LaTeX Font Info: Font shape `JY1/hgt/m/n' will be (Font) scaled to size 8.32214pt on input line 1. LaTeX Font Info: Trying to load font information for T1+lmss on input line 1. - (/usr/share/texmf-dist/tex/latex/lm/t1lmss.fd +(/usr/share/texmf-dist/tex/latex/lm/t1lmss.fd File: t1lmss.fd 2015/05/01 v1.6.1 Font defs for Latin Modern )) LaTeX Font Info: Font shape `JT1/hmc/m/n' will be @@ -536,19 +532,19 @@ LaTeX Font Info: Font shape `JY1/hmc/m/n' will be (Font) scaled to size 11.09619pt on input line 56. LaTeX Font Info: Trying to load font information for OT1+lmr on input line 56. - (/usr/share/texmf-dist/tex/latex/lm/ot1lmr.fd +(/usr/share/texmf-dist/tex/latex/lm/ot1lmr.fd File: ot1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) LaTeX Font Info: Trying to load font information for OML+lmm on input line 56. - (/usr/share/texmf-dist/tex/latex/lm/omllmm.fd +(/usr/share/texmf-dist/tex/latex/lm/omllmm.fd File: omllmm.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) LaTeX Font Info: Trying to load font information for OMS+lmsy on input line 56. - (/usr/share/texmf-dist/tex/latex/lm/omslmsy.fd +(/usr/share/texmf-dist/tex/latex/lm/omslmsy.fd File: omslmsy.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) LaTeX Font Info: Trying to load font information for OMX+lmex on input line 56. - (/usr/share/texmf-dist/tex/latex/lm/omxlmex.fd +(/usr/share/texmf-dist/tex/latex/lm/omxlmex.fd File: omxlmex.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) LaTeX Font Info: External font `lmex10' loaded for size @@ -562,15 +558,15 @@ LaTeX Font Info: Font shape `JY1/hmc/m/n' will be (Font) scaled to size 5.5481pt on input line 56. LaTeX Font Info: Trying to load font information for U+lasy on input line 56. - (/usr/share/texmf-dist/tex/latex/base/ulasy.fd +(/usr/share/texmf-dist/tex/latex/base/ulasy.fd File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions ) LaTeX Font Info: Trying to load font information for U+msa on input line 56. - (/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd +(/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd File: umsa.fd 2013/01/14 v3.01 AMS symbols A ) LaTeX Font Info: Trying to load font information for U+msb on input line 56. - (/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd +(/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd File: umsb.fd 2013/01/14 v3.01 AMS symbols B ) (./tex/intro.tex LaTeX Font Info: Font shape `JT1/hgt/m/n' will be @@ -583,7 +579,7 @@ ) (./tex/cbc.tex Underfull \vbox (badness 10000) has occurred while \output is active [] - [1 +[1 ] @@ -605,19 +601,19 @@ LaTeX Font Info: Font shape `JY1/hgt/m/n' will be (Font) scaled to size 9.24683pt on input line 6. LaTeX Font Info: Trying to load font information for T1+lmtt on input line 6. - (/usr/share/texmf-dist/tex/latex/lm/t1lmtt.fd +(/usr/share/texmf-dist/tex/latex/lm/t1lmtt.fd File: t1lmtt.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) LaTeX Font Info: Font shape `JT1/hgt/m/n' will be (Font) scaled to size 7.39746pt on input line 8. LaTeX Font Info: Font shape `JY1/hgt/m/n' will be (Font) scaled to size 7.39746pt on input line 8. - (./src/zero.agda.replaced) (./src/cong.agda.replaced) (./src/agda-term3.agda.replaced)) (./tex/cbc_agda.tex (./src/agda/cbc-agda.agda.replaced +(./src/zero.agda.replaced) (./src/cong.agda.replaced) (./src/agda-term3.agda.replaced)) (./tex/cbc_agda.tex (./src/agda/cbc-agda.agda.replaced consecutive: ) LaTeX Font Info: Font shape `JT1/hmc/m/n' will be (Font) scaled to size 7.39746pt on input line 8. - [2] (./src/agda/cbc-agda.agda.replaced +[2] (./src/agda/cbc-agda.agda.replaced consecutive: ) (./src/agda/cbc-agda.agda.replaced consecutive: @@ -625,12 +621,12 @@ consecutive: ) LaTeX Font Info: Trying to load font information for TS1+lmr on input line 61. - (/usr/share/texmf-dist/tex/latex/lm/ts1lmr.fd +(/usr/share/texmf-dist/tex/latex/lm/ts1lmr.fd File: ts1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern )) (./tex/hoare.tex [3]) (./tex/while_loop.tex (./src/while_loop_impl/while_loop_dg.agda.replaced) (./src/while_loop_impl/init_cg.agda.replaced) (./src/while_loop_impl/while_loop.agda.replaced) (./src/while_loop_impl/while_loop_c.agda.replaced) (./src/while_loop_verif/init_cg.agda.replaced) (./src/while_loop_verif/conversion.agda.replaced [4]) (./src/while_loop_verif/while_loop.agda.replaced) (./src/while_loop_verif/verif_term.agda.replaced) (./src/while_loop_verif/verif_loop.agda.replaced) (./src/while_loop_verif/verif.agda.replaced)) (./tex/tree_desc.tex Underfull \vbox (badness 4981) has occurred while \output is active [] - [5] +[5] File: fig/rbt-stack.pdf Graphic file (type pdf) <fig/rbt-stack.pdf> @@ -653,7 +649,7 @@ Underfull \vbox (badness 10000) has occurred while \output is active [] - [7] (./src/agda-dpp-impl.agda.replaced) (./src/agda-dpp-impl.agda.replaced +[7] (./src/agda-dpp-impl.agda.replaced) (./src/agda-dpp-impl.agda.replaced consecutive: ) (./src/agda-dpp-impl.agda.replaced consecutive: @@ -680,11 +676,11 @@ ) Here is how much of TeX's memory you used: 13953 strings out of 478697 - 230851 string characters out of 5861191 + 230851 string characters out of 5861192 1637656 words of memory out of 5000000 32054 multiletter control sequences out of 15000+600000 531855 words of font info for 129 fonts, out of 8000000 for 9000 934 hyphenation exceptions out of 8191 94i,8n,92p,502b,1814s stack positions out of 5000i,500n,10000p,200000b,80000s -Output written on midterm.dvi (10 pages, 121456 bytes). +Output written on midterm.dvi (10 pages, 121460 bytes).