Final project for SJTU CS2612 Programming Languages and Compilers (2022 Fall)
TODO:
- 指称语义中证明证明$[F(X) = (test1(D0) ∘ D ∘ while_denote D0 D) ∪ test0(D0)]$这个函 数的单调性与连续性。为此需要证明:
- 三元关系的复合保持集合之间的包含关系,相等关系
- 果_[F]是单调连续的,那么[G(X) = Y ∘ F(X)]_也是单调连续的。
主要困难在于,三元关系比较复杂,需要看代码RelDomain,简单套用遇到了困难
-
(*)指称语义中err和inf的部分,但是这部分小步语义中用不到,可以先缓缓
-
小步语义的构造