编译步骤/代码生成/网页汇编纯调用证明。豫
yuyan · 135 行 · 7440 字节 · UTF-8
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。
「:文言:整参入而整数出,无外效方可复用;无外效非必终。汉语:输入须为已验证SSA,且调用处另外证明所有实参都是整数。本分析独立重建整数与布尔种类,不信任结果类型标签;拒绝分配、内存访问、除法与未知操作。结论是条件性的无外部副作用和整数返回,不保证终止,不允许将调用提前到原本不执行的路径。:」
「纯整查函」乃化「字符串」而化「正则模块」而(「或可有」于「正则函数」)也。
「纯整查函」者会「名」而会「诸函」而
鉴「诸函」而
有「罄」则「可无」
或有(「缀」于「函」于「余」)则
若「串相等」于「名」于(「函」中「零」)则「可有」于「函」否则「纯整查函」于「名」于「余」
也。
「验纯整函数」乃化「正则模块」而化「正则函数」而「爻」也。
「验纯整函数」者会「候选」而会「函」而
若「或者」
于(「大于」于(「函」中「四」)于「二五六」)
于(「大于」于(「长度」授以「整数」于(「函」中「二」))于「八」)则
「阴」
否则
虑「种」者「新数组引用」授以「整数」于「零」于(「函」中「四」)
而
虑「好」者「新引用」授以「爻」于「阳」而
虑「无」者
「态射」授以「整数」授以「有」
于(「函」中「二」)
于(会「号」而「写数组引用」授以「整数」于「种」于「号」于「一」)
而
虑「取」者
(化「正则原子」而「整数」也会「值」而鉴「值」而
有(「正则局部」于「号」)则
「读数组引用」授以「整数」
于「种」于「号」
或有(「正则整数」于「数」)则「一」
或有(「正则爻」于「爻值」)则「二」
或有「其他」则「零」
)
而
虑「诸整」者
(化(「列」于「正则原子」)而「爻」也会「参」而「全部符合」授以「正则原子」
于(会「值」而「等于」于(「取」于「值」)于「一」)于「参」
)
而
虑「运种」者
(化「正则操作」而化(「列」于「正则原子」)而「整数」也会「术」而会「参」而鉴「术」而
有(「正则原语」于「名」)则(
若「非」于(「且」于(「等于」于(「长度」授以「正则原子」于「参」)于「二」)于(「诸整」于「参」))则
「零」
否则
鉴「名」而
有『豫言_整数加』则「一」
或有『豫言_整数减』则「一」
或有『豫言_整数乘』则「一」
或有『豫言_整数相等』则「二」
或有『豫言_整数大于』则「二」
或有「其他」则「零」
)
或有「正则调用」则(
鉴「参」而
有(「缀」于(「正则函数引用」于「名」)于「余」)则(
鉴(「纯整查函」于「名」于「候选」)而
有(「可有」于「往」)则
若「且」
于(「等于」于(「长度」授以「正则原子」于「余」)于(「长度」授以「整数」于(「往」中「二」)))
于(「诸整」于「余」)则
「一」
否则
「零」
或有「可无」则「零」
)
或有「其他」则「零」
)
或有「其他」则「零」
)而
递归虑「察段」其化「正则区域」而「整数」者会「段」而
鉴「段」而
有(「正则段」于「令们」于「终」)则(
虑「无」者
「态射」授以「正则指令」授以「有」
于「令们」
于(会「令」而鉴「令」而
有(「正则运算」于「号」于「类」于「术」于「参」)则(
虑「果」者「运种」于「术」于「参」
而
虑「无」者
若「等于」于「果」于「零」则「写引用」于「好」于「阴」否则「元」
而
「写数组引用」授以「整数」于「种」于「号」于「果」
)
或有(「正则如果」于「号」于「类」于「条件」于「阳体」于「阴体」)则(
虑「无」者
若「等于」于(「取」于「条件」)于「二」则「元」否则「写引用」
于「好」于「阴」
而
虑「阳种」者「察段」于「阳体」
而
虑「阴种」者「察段」于「阴体」
而
虑「果」者
若「等于」于「阳种」于「阴种」则「阳种」否则「零」
而
虑「无」者
若「等于」于「果」于「零」则「写引用」于「好」于「阴」否则「元」
而
「写数组引用」授以「整数」于「种」于「号」于「果」
)
或有「其他」则
「写引用」于「好」于「阴」)
而
鉴「终」而
有(「正则产出」于「值」)则「取」于「值」
或有「其他」则(虑「无」者「写引用」于「好」于「阴」而「零」)
)
而
虑「果」者「察段」于(「函」中「三」)而
「且」于(「读引用」于「好」)于(「等于」于「果」于「一」)
也。
「:文言:候选自全而削,互递同验,未定则尽拒。汉语:求封闭的整数函数集合,删除含未知操作的函数及所有依赖者;支持互递归。达到迭代预算仍未收敛则返回空集,不发布暂定证明。调用者不得单独把一次验纯整函数的假设检查当作最终证明。:」
「求纯整闭包」乃化「正则模块」而「正则模块」也。
「求纯整闭包」者会「诸函」而
递归虑「收」其化「整数」而化「正则模块」而「正则模块」者会「轮」而会「候选」而
若「大于」于「轮」于「三二」则
「罄」
否则
虑「余」者
「滤」授以「正则函数」
于(会「函」而「验纯整函数」于「候选」于「函」)于「候选」
而
若「等于」于(「长度」授以「正则函数」于「余」)
于(「长度」授以「正则函数」于「候选」)则「余」
否则
「收」于(「加」于「轮」于「一」)于「余」
而
「收」于「零」于「诸函」
也。