From 2ab888b4eff8f9a5a3600a1e6527e497f6ec6d6e Mon Sep 17 00:00:00 2001 From: Sg Date: Sat, 5 Aug 2023 12:14:47 +0800 Subject: [PATCH 1/6] doc(ch1): revise --- docs/docs/tutorial-chapter-1/introduction.md | 122 ++++++++++++++++--- 1 file changed, 107 insertions(+), 15 deletions(-) diff --git a/docs/docs/tutorial-chapter-1/introduction.md b/docs/docs/tutorial-chapter-1/introduction.md index 059bed8..a00548d 100644 --- a/docs/docs/tutorial-chapter-1/introduction.md +++ b/docs/docs/tutorial-chapter-1/introduction.md @@ -2,42 +2,134 @@ sidebar_position: 1 --- -# 直观的类型 +# 自然语言和编程语言中的类型 ## 自然语言中的类型 在知道类型系统的定义之前，我们其实都已经是汉语这门自然语言中的「类型」专家了。 -> 例 1：997 是一个质数。 +:::info 例子 -> \*例 2：997 是一个跑。 +例 1：自然数 997 是一个质数。 -如果我们来判断这句话第二句话是否正确，我们可以立刻下结论——它是错的——而不用去理解这个命题涉及的任何数学概念。因为这句话在**语法**上就是错的。这其实就是一种类型检查。 +\*例 2：自然数 997 是一个运动。 -那么，在编程语言这个形式系统里，我们是不是也可以有类似的快速「检查」？ +::: -——这样，我们可以用很低的成本来验证程序是否是对的，而不需要去跑程序本身。 +如果我们来判断这句话例 2 是否正确，我们可以立刻下结论——它是错的——而不用去理解这个命题涉及的任何数学概念。 + +——你可能会想：*自然数怎么可能会是运动呢？它们似乎是两类不相交的概念。* + +我们在无意识中就运用了自然语言中的类型来排除掉了一些不正确的语句，因为这些语句在**语义**上就是错的，即便它完全符合语法。 + +而这可以看成是一种广义上的类型检查。我们只需要去检查这个语句中的词汇类型是否相近、是否符合常识，就可以快速地筛出那些不可能为真的语句。我们其实早就已经能够熟练地对自然语言中的语句做「类型检查」了。 + +那么，编程语言又如何呢？ ## 编程语言中的类型 -在一些编程语言中，变量的类型可以在运行程序之前就能确定下来。具有这种性质的语言，叫做静态类型语言；反之，则叫做动态类型语言。 +### 类型检查 + +对于编程语言，我们也会有类似的**类型检查**机制。一般来说，我们会先进行**语法检查**，再进行**语义检查**（类型检查是其中一部分），快速筛选掉那些必定存在错误的程序，而不需要去跑程序本身，最终达到提高程序的运行时安全性的目的。 + +```mermaid +graph TB + Start[开始] + SyntaxCheck[语法检查] + SemanticCheck[语义检查] + Success["成功(有运行的价值)"] + Failure["失败(程序必定存在错误)"] + + Start --> SyntaxCheck + SyntaxCheck -->|通过| SemanticCheck -->|通过| Success + SemanticCheck -->|失败| Failure + SyntaxCheck -->|失败| Failure +``` + +### 静态类型 vs 动态类型 -```cpp -// CPP 是一门静态类型语言 +*在一些编程语言中，变量的类型可以在运行程序之前就能确定下来*。 + +具有这种性质的语言，叫做**静态类型(statically typed)**语言；反之，则叫做**动态类型(dynamically typed)**语言。 + +例如，C++是静态类型语言。 + +```cpp {2} bool a = true; a = "test"; // 会在编译时报错 ``` -```js -// JavaScript 是一门动态类型语言 +例如，JavaScript是静态类型语言。 + +```js {2} let a = true; a = 'b'; // 完全合法 ``` -而有一些编程语言当中，表达式类型之间的转化需要显式地进行，锱铢必较。 +### 强类型 vs 弱类型 + +表达式类型之间的转化需要显式地进行的编程语言，叫做**强类型(strongly typed)语言**。 + +```cpp {2} +string foo = "foo"; +foo + to_string(1); // 需要显式将int转换为string类型 +``` + +反之，那些类型之间的转化大都可以隐式进行的，叫做**弱类型(weakly typed)语言**。 -这种语言，叫做强类型语言(Strongly-typed Languages)； -反之，那些类型之间的转化大都可以隐式进行的，叫做弱类型语言(Weakly-typed languages)。 +```ts {2} +const foo = "foo"; +foo + 1; // 无需显式转换即可相加 +``` + +:::caution + +强弱类型是一个比较主观的概念，并没有严格的学术上的定义，无需纠结于此。 + +::: + +强对弱，静态对动态，我们有两个正交的维度。而每个编程语言各自的强弱动静也有程度差异。因此，我们可以尝试把语言根据其各个维度的程度，画在一个二维平面坐标系上，方便对不同编程语言之间进行比较。 + +:::tip 练习 +思考你所熟悉的编程语言的强、弱、动、静性质及其程度，在平面坐标系上标出这些语言的位置。 +::: + +## 类型检查——抽象解释视角 + +### 从具体到抽象 + +1. **「类型」是对具体对象的抽象**。抽象让我们只关注我们所关注的「性质」，而非具体的细节。 + + +1. **「类型」是一种推理工具。**在对具体对象进行抽象得到「类型」之后，我们就可以对它们的性质进行推理。 + +```mermaid +flowchart + subgraph ConcreteDomain [具体域: 苹果] + AppleAttr["属性：苹果细胞壁"] + AppleEat["操作：吃"] + AppleAddition["操作：苹果上的加法\n1个苹果+1个苹果 -> 2个苹果"] + end + + subgraph AbstractDomainNat [抽象域: 自然数类型] + NatAddition("操作：自然数上的加法\n 1+1 -> 2") + end + + subgraph AbstractDomainFruit [抽象域: 水果类型] + FruitEat("操作：吃") + FruitAttr["属性：水果细胞壁"] + FruitAddition["操作：水果上的加法\n1个水果+1个水果 -> 2个水果"] + end + + AppleEat --> FruitEat + AppleAddition --> FruitAddition --> NatAddition + AppleAddition --> NatAddition + AppleAttr --> FruitAttr + + ConcreteDomain -.->|具体事物抽象为类型| AbstractDomainFruit + ConcreteDomain -.->|具体事物抽象为类型| AbstractDomainNat + AbstractDomainFruit -.->|类型可以抽象为另一个类型| AbstractDomainNat +``` -> 注意：强弱类型其实是一个比较主观的概念，并没有非常严格的定义。 +3. **「类型检查」是对抽象的正确性的检查。** 如果代码中进行了不正确的抽象，类型检查就会提示我们存在错误。例如，若我们尝试把「具体域：松鼠」的实例——一只松鼠——抽象为「水果类型」，那么就无法通过细胞壁这个属性的检查，因为松鼠是没有细胞壁的；若我们尝试把「自然数类型」抽象为「水果类型」，也会出现失败，因为自然数类型没有定义「操作：吃」。 \ No newline at end of file From 00a34cd3c5ac03d1181f4347c4fd7f419d928b02 Mon Sep 17 00:00:00 2001 From: Sg Date: Sat, 5 Aug 2023 12:15:36 +0800 Subject: [PATCH 2/6] add abstract interpretation perspective --- docs/docs/tutorial-chapter-1/introduction.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/docs/docs/tutorial-chapter-1/introduction.md b/docs/docs/tutorial-chapter-1/introduction.md index a00548d..efd17e7 100644 --- a/docs/docs/tutorial-chapter-1/introduction.md +++ b/docs/docs/tutorial-chapter-1/introduction.md @@ -132,4 +132,8 @@ flowchart AbstractDomainFruit -.->|类型可以抽象为另一个类型| AbstractDomainNat ``` -3. **「类型检查」是对抽象的正确性的检查。** 如果代码中进行了不正确的抽象，类型检查就会提示我们存在错误。例如，若我们尝试把「具体域：松鼠」的实例——一只松鼠——抽象为「水果类型」，那么就无法通过细胞壁这个属性的检查，因为松鼠是没有细胞壁的；若我们尝试把「自然数类型」抽象为「水果类型」，也会出现失败，因为自然数类型没有定义「操作：吃」。 \ No newline at end of file +3. **「类型检查」是对抽象的正确性的检查。** 如果代码中进行了不正确的抽象，类型检查就会提示我们存在错误。例如，若我们尝试把「具体域：松鼠」的实例——一只松鼠——抽象为「水果类型」，那么就无法通过细胞壁这个属性的检查，因为松鼠是没有细胞壁的；若我们尝试把「自然数类型」抽象为「水果类型」，也会出现失败，因为自然数类型没有定义「操作：吃」。 + +### 抽象解释 + + \ No newline at end of file From 89e1a361bca9de2b6f0bb2f1d2715535d6d2b6fb Mon Sep 17 00:00:00 2001 From: Sg Date: Sat, 5 Aug 2023 12:16:34 +0800 Subject: [PATCH 3/6] mod --- docs/docs/tutorial-chapter-1/introduction.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/docs/tutorial-chapter-1/introduction.md b/docs/docs/tutorial-chapter-1/introduction.md index efd17e7..4c4df75 100644 --- a/docs/docs/tutorial-chapter-1/introduction.md +++ b/docs/docs/tutorial-chapter-1/introduction.md @@ -95,7 +95,7 @@ foo + 1; // 无需显式转换即可相加 思考你所熟悉的编程语言的强、弱、动、静性质及其程度，在平面坐标系上标出这些语言的位置。 ::: -## 类型检查——抽象解释视角 +## 类型检查的抽象解释视角 ### 从具体到抽象 From a93ddab1e84459476341552f15b49983b5bb51b1 Mon Sep 17 00:00:00 2001 From: Sg Date: Sat, 5 Aug 2023 16:55:34 +0800 Subject: [PATCH 4/6] add program analysis perspective --- docs/docs/tutorial-chapter-1/introduction.md | 40 +++++++++++++++++--- 1 file changed, 34 insertions(+), 6 deletions(-) diff --git a/docs/docs/tutorial-chapter-1/introduction.md b/docs/docs/tutorial-chapter-1/introduction.md index 4c4df75..e77d4be 100644 --- a/docs/docs/tutorial-chapter-1/introduction.md +++ b/docs/docs/tutorial-chapter-1/introduction.md @@ -28,16 +28,18 @@ sidebar_position: 1 ## 编程语言中的类型 -### 类型检查 +对于编程语言，我们也会有类似的**类型检查**机制。 -对于编程语言，我们也会有类似的**类型检查**机制。一般来说，我们会先进行**语法检查**，再进行**语义检查**（类型检查是其中一部分），快速筛选掉那些必定存在错误的程序，而不需要去跑程序本身，最终达到提高程序的运行时安全性的目的。 +### 编译视角看类型检查 + +一般来说，我们会先进行**语法检查**，再进行**语义检查**（类型检查是其中一部分），快速筛选掉那些必定存在错误的程序，而不需要去跑程序本身，最终达到提高程序的运行时安全性的目的。 ```mermaid graph TB - Start[开始] + Start[编译开始] SyntaxCheck[语法检查] SemanticCheck[语义检查] - Success["成功(有运行的价值)"] + Success["成功(有运行的价值，进入后续流程)"] Failure["失败(程序必定存在错误)"] Start --> SyntaxCheck @@ -46,6 +48,32 @@ graph TB SyntaxCheck -->|失败| Failure ``` +### 程序分析视角看类型检查 + +**程序分析(program analysis)**是对程序运行时行为提供安全的、可计算的近似预测的技术[^1]。从程序分析的视角来看，编译过程中的**语法检查**和**语义检查**都是不执行程序而对目标程序进行分析的手段。这一类手段被称为**静态分析(static analysis)**。 + +[^1]: Nielson, F., Nielson, H. R., & Hankin, C. (2015). Principles of program analysis. Springer. + +类型检查是一种重要的静态程序分析技术，它也会被称为类型系统。 + +```mermaid +graph + subgraph ProgramAnalysis["程序分析(program analysis)"] + subgraph StaticAnalysis["静态分析(static analysis)"] + TypeChecking["类型检查(type checking)"] + Linter["Linter"] + ControlFlowAnalysis["控制流分析(control-flow analysis)"] + DataFlowAnalysis["数据流分析(data-flow analysis)"] + AbstractInterpretation["抽象解释(abstract interpretation)"] + end + subgraph DynamicAnalysis["动态分析(dynamic analysis)"] + Testing["测试(testing)"] + Monitoring["监控(monitoring)"] + ProgramSlicing["程序切片(program slicing)"] + end + end +``` + ### 静态类型 vs 动态类型 *在一些编程语言中，变量的类型可以在运行程序之前就能确定下来*。 @@ -102,7 +130,7 @@ foo + 1; // 无需显式转换即可相加 1. **「类型」是对具体对象的抽象**。抽象让我们只关注我们所关注的「性质」，而非具体的细节。 -1. **「类型」是一种推理工具。**在对具体对象进行抽象得到「类型」之后，我们就可以对它们的性质进行推理。 +2. **「类型」是一种推理工具。**在对具体对象进行抽象得到「类型」之后，我们就可以对它们的性质进行推理。例如，一旦我们知道「苹果」可以被抽象为自然数之后，其实就可以将苹果当成自然数来处理。 ```mermaid flowchart @@ -136,4 +164,4 @@ flowchart ### 抽象解释 - \ No newline at end of file +抽象解释是一种非常强大的理论框架，它可以把许多的静态分析技术。 \ No newline at end of file From 095548350f85334f60ae42645c9177d36778107a Mon Sep 17 00:00:00 2001 From: Sg Date: Sat, 5 Aug 2023 17:19:48 +0800 Subject: [PATCH 5/6] more --- docs/docs/tutorial-chapter-1/introduction.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/docs/docs/tutorial-chapter-1/introduction.md b/docs/docs/tutorial-chapter-1/introduction.md index e77d4be..19933b5 100644 --- a/docs/docs/tutorial-chapter-1/introduction.md +++ b/docs/docs/tutorial-chapter-1/introduction.md @@ -60,7 +60,8 @@ graph TB graph subgraph ProgramAnalysis["程序分析(program analysis)"] subgraph StaticAnalysis["静态分析(static analysis)"] - TypeChecking["类型检查(type checking)"] + TypeSystem["类型系统(type system)"] + EffectSystem["效应系统(effect system)"] Linter["Linter"] ControlFlowAnalysis["控制流分析(control-flow analysis)"] DataFlowAnalysis["数据流分析(data-flow analysis)"] @@ -164,4 +165,5 @@ flowchart ### 抽象解释 -抽象解释是一种非常强大的理论框架，它可以把许多的静态分析技术。 \ No newline at end of file +抽象解释（abstract interpretation）是一种非常强大的理论框架，它可以把许多静态分析技术统一起来囊括其中。 +它的核心思想是：将具体域中的程序抽象化，放到抽象域中进行推理。由此，我们从原始的程序得到了一种新的、抽象的程序。通过执行这些抽象的程序，我们可以得到原始程序的部分性质。 \ No newline at end of file From 5e0da46e569b8e6770ef9adf7c61943b0c55dd15 Mon Sep 17 00:00:00 2001 From: Sg Date: Sat, 5 Aug 2023 18:28:41 +0800 Subject: [PATCH 6/6] add sign analysis --- .../tutorial-chapter-1/img/sign-analysis.gif | Bin 0 -> 9288 bytes docs/docs/tutorial-chapter-1/introduction.md | 47 +++++++++++++++--- 2 files changed, 40 insertions(+), 7 deletions(-) create mode 100644 docs/docs/tutorial-chapter-1/img/sign-analysis.gif diff --git a/docs/docs/tutorial-chapter-1/img/sign-analysis.gif b/docs/docs/tutorial-chapter-1/img/sign-analysis.gif new file mode 100644 index 0000000000000000000000000000000000000000..631db7094e74a9f9fc3364e11ba02d93a6515a81 GIT binary patch literal 9288 zcmV-OB)8i~Nk%v~VcPmn)(UA+KK?6+He}X0YrO?E9m;#3X5x-`$7~< zT#VMcfSd|!EQ8Vv9SxcrM_jfe4crYzVQLLPrcEj_PMIBdz|4iYjVk^6;a`Rrmnu z8yN*7%9W8g`tisTiprQY4VA0|v!=|MI(y!^*(RsYDbwQuw-!h6D(`oD2P2tFtze27o*)QhJX*F|x?D@0kB8f*Uovh2WzssuCp#CGb zHM!EV^Ss8ht2Q^emlhlU-zxj^F5Z9o4hAbEAY%(vsb z4m^8w@89B@Kac)=2R6PhG1Qk}r(}_EHxZwsYa@bsmSBw~7 ziQ>hz#c}z$@FEW{eyEy^P7r8gJ1VmE-hDWBz#*d83%y#VO~74zyyYB6wD& zXL&}}I2xdr0NKEXelBuoWQiK+l7w(F3WKIbRGI*neeyX7q>f!$X8yW2mMYL#yS@dd~-<#u|aHcGP;b7BOu?&*iDZ1y%r4Thoa?5VJ?%L~zzj%#H zudHXBg&r^4M%r(^3-=-LTLc%ZFsUN?nQv~(_GrVqTMDY!#07h-1i}t#46p)PVrwxT z5w9iku_P~Ha(pO1yza}Yri>=Y@(#IUV>6qD@y#~lEWn&x@jR^0)6SbKf%W}0w6aB? zjCIRiRQ*M~;zGT`z7mMN71LnU9OltlM`bp+PJf*wvfna5wozOI9h<&J|Ach3Z}Ua) z+!YAk(A`pAt#;aO0@t=2UJneml8sybYj`@7pN+PgM)!^R+I}njbO(fsUO6|V6RjSO zR-R7tv}x34|Y2muuB|y#fNild+xXk5613p5l6fXv&WLWVa<18Jj`G} zKLho*EI*Csm|*Wj^kfyrz1-SMV?7t;>jFF*-iMXd`Ix3pO!#H z_`&eMH2)1sfcC4O?()aGG61lDmNVcQ9Jr`OERYH7V_yI!xGQpC&}sw>76gy+!Qz4L zYaP5;2}yFo28D2dDFk5)y@0^Au%dTnkRNnjSi=>jONX7K)d=0P3mWDShh^d++laVB zByP=!T8QCQ#3aNX#*c|z*r5LA7-2;uIFTunisBJ-kwv2IAdDrW;uW?y6mxlTiAua7 z7R`7MIGV6jKYWV4V#X#pGOms0)8p9ucrQ9?C1rRt0vV;Kh}_}ukVs&p4$#OFrWMkV ze4K+LDVahYUa|pID*nq!gLJU|76G61kfRBr^i7+H z6m{yLTlGNN$dyi1oqA+ODP=lJoW``8bOR?uUrJD#hJg>I48%{P#>Y09@~94j7)1d> z$~ah3r`@C~B|Ftqb0!j|t^@@?%QXX16wnV`#a6D`AQf_CRiiy)1Xv~j*nUXVrej48UxRs0yy8@^ zEih~gNa`Biw1BYAI7w0Ez*)E&Xn@Z|-(`8!)}V;C2D1>xW8H~b&uX<}tkvaf7aOgY z%yzf>x$Osx{)@TF8nvFJ;%aI?@LX;oX1HlhfN34jPV7>*kH4jyT{oMqoZ8iI&cWy( z2{GF!Znuwx?e6<@xkK@y&uzv*X*VnI*bv!wX)bi_7~?BnKtvY;puLEB|Am3Xp!C3p z&7pt)+uHy`hrVA}Zyq^N6bqN&tME+jat&#skj@ugu~mYG^Y}umoH)BG{GuB{3}6(0 zn8ae)?}b620^}ZoacmQ?VOyr#0T0N%%_^}DPFzM71Qwb^7VL}Jfu?KxD^ZgmS>rYDiX9OgFfb;=odrERZ_tkTwY%_$}8 zl;I5ivxBOH51ShR%)-RzEk*X$%zD z6nL&{ISifK4j*J~jn-VK>G$djjCwt#{wQfseOe9{?!2nz8-;t{+{| z&*3=O5p^%KeQULdc&^nWmNccGE$oZ5B+k^Fc0e43$!2G(Z{sHSw@24mKz1e8q8>G| zaXW@9y_rU++#BjPYA$orsa#pRx45&aZ2V%IxF`uSz4@Iue?Mz*yyBcg>)r3x)o*Knb#$C;EF&!Q1Q5X4ZXZ7=l-&E*ICAu+< z4s;c!d|T8m@&Ph#+218R=Qr~m)OkKjmUnwnQ>T+xO0sUTfxP2V$I{1rKJ>xK9q@P$ zJK?QyljQu}?sw;V*7}Zk!pC^#7eag5)$Ve(W6kY-I@~CG`t>j!-sPY_(k>t`dV^6t zQ$+)iFs{}*If37dgUh-b*Fse*J?B|*MQ|`fagbm_|kY&%P9(^DKPZ8%18pi;dQixMGw66Hl7Y1cggoeb zpf^t92QYqTcwE?d2uLMpD1%=}g*ccQES5C0HdRd6ds(=B47i18MsR~Cd=YqsT}dGi8Tfk)wo{H&GO&{)W0|hmz=dDHuVo z$A~T%agCUUK<9^MsDWYVfV4-7ju?gA_i<&2iV63KtjIK$s9kWl0GVh%BjrS@GZB2Z zeTa8%&F3!nC5UcUie&eKWS4ZfxQeNygFCp4gZPP{Xm`God@IwufyvHQZ>B?YB83(uoz*c;6R)_1KSj<0*OQkpsDiFbI-$sEQf0 zk_+jEb8#!_=yWtNk(D4)4?}mS=ZW}Hh57h7!d(X#thFXfJ@8sc={RlbEa5T{_u8B>7UWDVf=5 z1g2SMUnydrwVKRhYM?ZmG8HuK_z2JTmJta8$(azOWSe{jRy1AUc*>fJioDEbj zF;Pq+fm758Tf8ZXyJ?+ML}khn0h6{wvNM)Gc4_{AxsKvlJ>*%Q5^dBrL3Tp>SI+75gw~3%8%4R170PU%m%C&4QdPXZ#qC3i?BRYl9C85)h zZnA)*F8YfJDupNNp{aJGzDQ658lb%iq*$h+9l8JvHlyi@q)DcvOB#&FRixKLXIYA( zR0?-1dZl4{9}*CuNjgpN#-z3Ipel8yqGOMaR^XKMqX3fiU0sc{(qo?wKh){ZLYk0hSjHWU7Z#8vdk(x^RlRsEqmm*%_#B3a2%Rp@V9kmx`$! zWubY>scz~3pxRz&8mX~LYn@6Emdd3qb*QKcsmz9}4AZBs3aPW&m8GhtmC9}8G^B`{ zq8nzbn4+b@nyY_GtkrsUb9xCUM<08|taj?Gn!1%~0;8*HOD*=LX?m>L@T)hbtjo%) zpgC}Sx-z5+bHy5}#g(q6ldSFPuG2bX4=S%vYOkznuAyqG8Z>Wb#jWo;H~<^4c(SFz z)T{+-t_Rzk!m6ta>#xs}uha^x;ySJvTdoufLKce-39GOgTQVKcu^#)PE#j!jB&!2U z7%h9UB3q^^8&h)HXP^2ZhZ3{n{z6+ljO5!EQ&ZGC)!(5nGYNO0!5} z4o+(~?uE6gnzD~7a2Lc%Z2C4%6SUdpt@qlH3PhtM;kDZurARAqTl*zq`-`C>wYFxa zM4PsY$wjf5S$NyF>!Fb3ilBiRvOhYrB>R_fBey-_x2pxXjYMh%>8C4DwmLhsdTV7Y zwzi(|xDjQxP&TPk(6pptHsjIrT7CErX zov)jdxjVb1`jUjp0mBt>-KRz%BZ~-WkCpJj2pU zq&7UgPBO3idzw6YyFM(%OZ<_Pk;U%VH58h?(Ml}Nd!$qB!-<=< ze6E!k7%9e9SzSY*jkd$?j`i*~Q6b zY{dXInxgy-7~G@JOUUrW#hN@Qwp+>f$-=Fw%TJKTGnUJ>yvs=3%Dr5mzZ}bGi>{nR z$51?n$BfKxoXHIG%9#nw3~aK@+%pXWs9S8r*sRPaV2(87y3Ps9D$J>)oU?Q!&eq$_ zf^5#@JTI%m4f@TzRtf`s&htCW$t=Rw z)nyFJ&>1_L4{gV{P{-l>%=T>2U0YlkeZUo3&!+*#c z7+_1!(f%ODq)gE>P1F3E&=k_8c=hrtSPWu!?VQcGMSr(l%-0Y2doi4UHA3!PkMz5-<{$_<7e`yg*eWgA=h(a2Y7~u(*rF@gblp3g zw%F|3*`4vMqrIt6!Pz<-*pW@tq21G#z0x4zMW_v$PXr4&tf8&_*XZD6Bp z+k%JN;mVuEecKD2v%h`S&@|Yao2Q=(6-Qg1$_>@Moz=FA-Nx;@6TQ0dY`*kc-F)(! z{-O=pk;~nh{oTTSoFUrX?)<$LL&;K2r*%!)DUC(o%>%j_-!I&^WPGmUh2J@-(PeVP zh^D6hoeX8;IrUA_#w0W5*D7oqE$<|ky>7!>cmP*`%jvMz(%OZm094?laUV>FOexEL@p)TvP z4x5(x>9$TgwXW;A{;Rk?>g-VJImtv<~bTsOy-_>^9?!k`C-86zZ*L z>)DR0!EWe>4oawQtX6*N$=>Rjx9!wk?egU8ukP%*IE~(@?dV>-t_aVLt_rG5YIeS! z}Y>|K_Bm){_oh1>n8lG;%)Ctq3_VV5@eqkSAXkMN$|UFeXd^g z`xf|;Bkz59?(YRZ{=qKMrcayUYyl zxku~kNObhQ&is{+m`)4)weRylM)-Vq=QXiswoU!CAC92g#r{`bmy8|oUnj?b-|VDg z`QWGi((e0RSL~Vv>7JkRN~{sr#r5ppm_CNxM@sR znDS7YZ*?e@I|s8v9I zMpfn_FToBdJKam^n zpyg)Ha<8#X2B&-}c(cL7L%gL)^tZvJ?_h zln0nYPiRUu8&*+_vQW%=bn|Fyk2-#mn!Hp>C1o@XgJg$i~WKv<1d=U8%-R&=gQBs8PWglnXNh-iTP?;@HZ_W)Ddg<%u=h3d-TH z6;u_5G>I)J$oR7EJxTYFqq_h(Yp&~SY9Yp46$`$sm~cpj^xpN%==B`px3h_cgr}#U zF44aigzlW&go>FB=a6z|UN^v=k(5!kkaZL+kz_>C8uOv&7LwBck-XcK$leQ!PW~a*Hf&sj=2s zg#opvQMXz(R#-nFv5O5}FlT~;79wPXFkRv1ohMGZ43s{Vda?~$j$y*e1hu+`rA5a2 zPbPjoIjgc)-WX$C?i}skB!3*w({C5&Xu^S>8Re4>ACC1v!NxN8sc+#u>D`wPK6T%Mf#0S6GjZk-*{#&5G&L_kFrSLBkM3)Y`Cbbv730RJEjd3uS zB$^{92}ziV(2t%2q9qGCM?*4?NWfU6CqH?xM~d=-YYb%2PFYG|wXc@K>);c!!^l`F zE|j!8 zE&zR=LgVSuR$@}6R;p(*IQr6A#gu6_4QFtS8qi$Lv|^d6Qy%k~xm98>s0vJK{jQ2g zqEb?)vjCSx=gBgswri>iW2&vr`plZ9)s$UT&sPbG$dSgStWV1-z1XT&?#)$b5lU-a z1(mL<^7V^e+G^-jN1VGd@KS#r>>txc*u4O@v3aG{Z(ML#u1X88=6S4Sp=j8}hR?F2 z(d_<6KfBh>V%Dvo4Q>2Ri`LS5aI}mCO-=>q3|Se-Vk(yV{Zxhsh1=rI_o)jS8r@$Efa$#!yj9U01t9-7a@S z=v^Z&ceR3Z)^nTcpC#qjV_-S&)>5mp_x{1S$Hkv~cZf~nHTS;cMekYkRUOCt_dV=g zYId79V37GGz}f0>1q!TR`>qYY`>jogM69OZqRMa|wk3v33S$DZ$HnWdF$6+vVF~l+ zNgXOxnNk&&9_L8M2Da2k8>>wOue5e~EwXxf3}qAl_@w;xZ+~0dT1kdDZw4gPjsC9$ zW)PS5$yJVrlv8}-E1USgCHAbAw=844%K42GD>KCItg~Y()VU6(4V77(<`bcrwQ!yS zl4Uv}B#PN+hHmGcg}Np=@s>P`L9w7wMT$IQE=GthDxK^6UGFlQZjd%LoF+YJ3`y5E z{as5@NR1yagL;``ZsF*Byu9O$^tn%0N#^ktR1X#u zM<#Ta$h=q{cCo4Y?smqz4z|8Ex#U~#lx+@!56qsr`E8^k1sMm_R>~AB{_9?X!yAHx zeRi#30>8kusoJg~^n=rTZIqtJ;MnbSfj|Ccfp0nFzteHLUwd+U5_IO<>~^g;KJZhc zR^gAXd3K`h?;Y!$;@fs%%eDLSL$^HUqA9x2Yktu(;(U`#UpoJKPHw4tJLp(v;asoI z@mH;{zHHvPig%jZu=Bd?0vw{_g*!D2=<^99{CAIrPOTK!_FW{FiAMRuYKi?~;MB}qxHsj{~tSt|>_or!lly9k? zv5Hqx@3_*B=D4lG_V4Q+$NyTYf#xqz9!`1a59sEN0TJi?cnX9pa5bF8s5bBd&+q=$ zuL29O>8vXONsH$;EC2zl-m>rWK9H0qFawDU1+B`W&gKF2@AkxQ2Fb1jRqI)Jke*yC z25-Y>bkNv_ko$b_2b*y6fH3E>Y{`u92q(e=w+}(6LIhze3eoQg&2I-WQ2XdA0%yp` zc+UP_aQCWk^cYCt25@c)&NOAF(I3q^|$*RTZzE)MT!6Zb4hC^5TIO)fC;NkuLF3u6QdM)8%>?i9OF6WdS;Im#7Z@eISv0g~X!JgpRAFc)R(0F#Rs%`Xs-ED?8M zT1amA5-R0f&lzzK7mX1CJyFtnQ3mtm8(5=q-X$EF5vfv<4YAQ0oyroY5f9}s8%2l% z$uYeaVF|+V8*MQYSFsPfQ99&g9{X_*_i=V2Zyv`WUeYNaQSlsUOC1N190QU7VJqqe z5(?o_w)T-BBXT1fvLg2?!!8ouLNen>&?7l=BmOnAA;GQp9J0-x67Oy+Ec=itXG|(_q%7g`D9cYM-*WWWlJDjcP~vhg zk>@O7&-%PF4^8smnk+E+@-X{y`^J(HL&GpVM=htWE)jDwPp|nF^BHwTvLN#>C6h8e zv+*YIGQHtJz_JQEXS_ZQRZ%r?0^EW?n zBrno2`{r8kQGayvE`f77e-NbROe2#s{x8`mI#-i9t@AjY6ECT<_NepcSfV>g^E$;d zBJ0k$PLn0UlWcgwAdDkDjdMKVGb_u}d1TX?+!H+GGe2jOE=i_7$x}4-GeCo;I>7`p z&r>D|R6rG!uR3#V{L?6Hb3rAv7j-iylM^u`bV4;WAn&t7@d7{@N;x-lL>G{#Kvd&) zlSEatC=--sGIT{@bVEo&2&Gz6eO?oOxct~ ziL)5jv`yu7MH_Sr$8=8dG*1&nk3a8JPyO^yIWtYou}=ZDPz`n9QqngMbx|2r25%@l q8#PiTH8Mx&K_~T6F*Q&}vqCeqQ$6*?F7#7HbyP{URCA#K0028TcUZmv literal 0 HcmV?d00001 diff --git a/docs/docs/tutorial-chapter-1/introduction.md b/docs/docs/tutorial-chapter-1/introduction.md index 19933b5..aba8632 100644 --- a/docs/docs/tutorial-chapter-1/introduction.md +++ b/docs/docs/tutorial-chapter-1/introduction.md @@ -126,13 +126,52 @@ foo + 1; // 无需显式转换即可相加 ## 类型检查的抽象解释视角 -### 从具体到抽象 +### 抽象解释 + +**抽象解释（abstract interpretation）**是一个非常强大的理论框架，它提供了一个可以把许多静态分析技术统一起来的视角。 + +它的核心思想是：**将具体域中的程序抽象化，放到抽象域中进行推理；再将在抽象域中进行推理得到的结论具体化，映射回具体域，从而得到关于具体域中程序性质的结论**。 + +我们来看下面这个非常经典的符号分析的例子。 + +:::info 例子：如何计算一个表达式的符号[^2] + +[^2]: [Abstract Interpretation](https://pages.cs.wisc.edu/~horwitz/CS704-NOTES/10.ABSTRACT-INTERPRETATION.html) + + +假设有一个语言只有高精度整数和其上的乘法$\times$。 + +其具体域（在图中左侧，标记为C）就成了 + +那么，在抽象域上，它的乘法表就是： + +| $\times$ | neg | zero | pos | num | +|:----:|:----:|:----:|:----:|:----:| +| neg | pos | zero | neg | num | +| zero | zero | zero | zero | zero | +| pos | neg | zero | pos | num | +| num | num | zero | num | num | + +示意图如下 + +![符号分析](./img/sign-analysis.gif) +::: + +符号分析中，抽象域中的几个元素：num、neg、zero、pos其实都可以看成是一个类型。我们通过定义抽象域上的乘法表，较好地描述了具体域中的元素在乘法下的转换规律。 + +### 抽象解释下的类型 + +通过抽象，我们从原始的程序得到了一种新的、抽象的程序。通过执行这些抽象的程序，我们可以得到原始程序的部分性质。 + +我们把程序中的元素（整数）及其上操作（乘法）看成是具体域中的元素，把类型看成是抽象域中的元素，而类型检查器就提供了抽象域中元素的计算规则，是一个抽象域中语言的解释器。 1. **「类型」是对具体对象的抽象**。抽象让我们只关注我们所关注的「性质」，而非具体的细节。 2. **「类型」是一种推理工具。**在对具体对象进行抽象得到「类型」之后，我们就可以对它们的性质进行推理。例如，一旦我们知道「苹果」可以被抽象为自然数之后，其实就可以将苹果当成自然数来处理。 +3. **「类型检查」是对抽象的正确性的检查。** 如果代码中进行了不正确的抽象，类型检查就会提示我们存在错误。例如，若我们尝试把「具体域：松鼠」的实例——一只松鼠（没有表现在图中）——抽象为「水果类型」，那么就无法通过细胞壁这个属性的检查，因为松鼠是没有细胞壁的；若我们尝试把「自然数类型」抽象为「水果类型」，也会出现失败，因为自然数类型没有定义「操作：吃」。 + ```mermaid flowchart subgraph ConcreteDomain [具体域: 苹果] @@ -161,9 +200,3 @@ flowchart AbstractDomainFruit -.->|类型可以抽象为另一个类型| AbstractDomainNat ``` -3. **「类型检查」是对抽象的正确性的检查。** 如果代码中进行了不正确的抽象，类型检查就会提示我们存在错误。例如，若我们尝试把「具体域：松鼠」的实例——一只松鼠——抽象为「水果类型」，那么就无法通过细胞壁这个属性的检查，因为松鼠是没有细胞壁的；若我们尝试把「自然数类型」抽象为「水果类型」，也会出现失败，因为自然数类型没有定义「操作：吃」。 - -### 抽象解释 - -抽象解释（abstract interpretation）是一种非常强大的理论框架，它可以把许多静态分析技术统一起来囊括其中。 -它的核心思想是：将具体域中的程序抽象化，放到抽象域中进行推理。由此，我们从原始的程序得到了一种新的、抽象的程序。通过执行这些抽象的程序，我们可以得到原始程序的部分性质。 \ No newline at end of file