-
Notifications
You must be signed in to change notification settings - Fork 0
/
Preface.html
522 lines (355 loc) · 20.5 KB
/
Preface.html
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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Preface</title>
<script type="text/javascript" src="jquery-1.8.3.js"></script>
<script type="text/javascript" src="main.js"></script>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Preface</h1>
<div class="code code-tight">
</div>
<div class="doc">
<a name="lab1"></a><h1 class="section">前言</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab2"></a><h1 class="section">简介</h1>
<div class="paragraph"> </div>
这本电子书是一个关于软件基础 ，可靠软件背后的数学的课程.
主题包含基本逻辑概念，用计算机辅助定理证明，Coq证明助理（Proof Assistant），
函数式编程（Functional Programming），操作语义（Operational Semantic），
霍尔逻辑（Hoare Logic），还有静态类型系统（Static Type System）。
这个课程的预期受众是从高级本科生到博士与及研究生的读者、
尽管一定的数学熟练度会有帮助，
本书没有做任何“读者有逻辑学或编程语言的背景”的假设。
<div class="paragraph"> </div>
这个教程的最大创新是，本教程是百分之百形式化，并且机械验证的：
所有的文字都是字面意义上的，Coq脚本。
<div class="paragraph"> </div>
它是用于于一个Coq交互式会话一起阅读的。
本书的所有细节都完全用Coq形式化了，习题也是被设计于来Coq做出。
<div class="paragraph"> </div>
文件被整理为一系列覆盖了一学期内容，环环相扣的核心章节，
与及一定的包含额外主题的“附录”。
所有的核心章节都适合高级本科生与及研究生。
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab3"></a><h1 class="section">导论</h1>
<div class="paragraph"> </div>
构建可靠的软件很难。现代系统的规模，复杂性，介入构建过程的人数，
还有置于系统之上的需求的范围，使得构建或多或少正确的软件很难，
更不用说百分百正确。同一时间，因为信息处理继续融入社会的各个方面，
程序错误于漏洞的代价越来越严重.
<div class="paragraph"> </div>
计算机科学家与及软件工程师对这些挑战，通过设计一系列的改进软件质量的手法，
包含对管理软件项目与及编程团队的建议（比如极限编程（Extreme Programming）），
库（比如模型-试图-控制器（Model-View-Controller），发布-订阅（Publish-Subscribe））
与及编程语言（面向对象编程（Object Oriented Programmin），
面向切面编程（Aspect Oriented Programming），函数式编程（Functional Programming））
的设计哲学，还有用来指定，论证软件属性的数学与工具来应对。
<div class="paragraph"> </div>
这门课的重点是最后一个方法。本书教程把五个概念穿插在一起：
<div class="paragraph"> </div>
（1）逻辑学里面的基础工具，用于构建并且证明精确的关于程序的假设；
<div class="paragraph"> </div>
（2）用证明助理构建严谨的逻辑论据；
<div class="paragraph"> </div>
（3）函数式编程思想，同时作为编程方法与及程序跟逻辑学之间的桥梁；
<div class="paragraph"> </div>
（4）形式化的用于论证程序属性（一个循环对所有输入都会终止。
或者一个排序函数或者编译器满足特定规格）的手段；与及
<div class="paragraph"> </div>
（5）用类型系统建立一个对于某一个编程语言的所有程序都满足的特性
（所有类型正确的Java程序不能在运行时被破坏）。
<div class="paragraph"> </div>
这五个主题任一个都可以轻易填满一整个课程；
把它们五个塞在一个课程中很自然地表面很多会被遗留在外。
但是我们希望读者会认为5个主题互补，与及同时教授五个内容会创建一个使读者
可以轻松进入任一主题的根基。一些更深的阅读的建议会在 <span class="inlinecode"><span class="id" type="var">Postscript</span></span> 一章出现
<div class="paragraph"> </div>
<a name="lab4"></a><h2 class="section">逻辑学</h2>
<div class="paragraph"> </div>
逻辑学是研究证明—不可被质疑的对真理或者某一特定命题的论证的学科。
我们对逻辑学在计算机科学中所占的中心地位写了一卷又一卷的书。
Manna与及Waldinger称之“计算机科学的微积分”，与此同时，Halpern的论文
<i>On the Unusual Effectiveness of Logic in Computer Science</i> 列出各种不同
逻辑学对计算机科学提供关键工具，洞察的方法。的确，他们观察到
“事实上，逻辑学在计算机科学中比在数学中远远的更有效。
这很值得提起，特别是因为过去100年间，逻辑学发展的动力大部分来自数学”
<div class="paragraph"> </div>
特定的说，归纳证明的基础几号在计算机科学中处处可见。
你肯定以前见过它们，比如说在离散数学或者算法分析中，但是在我们的这个课程
我们很会对之在你前所未有的深度下进行检测。
<div class="paragraph"> </div>
<a name="lab5"></a><h2 class="section">证明助理</h2>
<div class="paragraph"> </div>
逻辑学与计算机科学的交流并不是单方面的：计算机科学也对逻辑学造了重要的奉献。
其中一个是发展可以作为帮助构造命题/证明的工具软件。
这些工具分为两个范畴：
<div class="paragraph"> </div>
<ul class="doclist">
<li> 提供一键式操作的自动化定理证明器（Automated Theorem Prover）：
你给它们一个命题，它们返回真，假，或者超时。
尽管他们的能力被限制到特定的推理中，他们在最近几年大幅成熟，
并且现在在各种各样的场合都有被用上。自动化定理证明器的例子包括
SAT，SMT，还有Model Checker。
<div class="paragraph"> </div>
</li>
<li> 证明助理是一种会对于构建证明中比较常规的部分自动化，
并且在更困难的地方依赖于人类的混合式工具。
常用的证明助理包括Isabelle， Agda， Twelf， ACL2， PVS，与及Coq,还有很多其他的。
</li>
</ul>
<div class="paragraph"> </div>
这节课基于Coq，一个在1983年起就在一定数量的研究所与及大学中发展的证明助理。
Coq提供了一个丰富的用于机械验证形式化论证的环境。Coq的内核是一个很简单的，
保证只有正确的推论发生的证明检查器。在此内核之上，Coq环境提供了高层的证明开发设施，
包括强大的，用于半自动化构造证明的策略，与及一个庞大的包含了各种定义，引力的库。
<div class="paragraph"> </div>
Coq容许了各种各样的在计算机科学与及数学上的研究的进行。
<div class="paragraph"> </div>
<ul class="doclist">
<li> 作为一个对编程语言建模的平台，Coq成为了
需要对复杂语言定义进行描述，论证的研究员的一个标准工具。
比方说，Coq被用于检查JavaCard平台的安全性，得到了最高阶通用准则验证。
再比方说，Coq被用在x86与及LLVM指令集的形式化规范中。
<div class="paragraph"> </div>
</li>
<li> 作为一个开发被形式化验证的软件，Coq被用于建造Compcert，
一个被完全验证并带有优化，并被用于证明精妙的浮点数相关的算法的正确性的C编译器。
同一时间，Coq也是Certicrypt，一个用于论证密码学算法的安全性的环境的基础。
<div class="paragraph"> </div>
</li>
<li> 作为一个现实的依赖类型编程的环境，Coq激发了数不清的创新。
举例说，Harvard的Ynot项目在Coq中嵌入了“关系式霍尔推理”（一个霍尔逻辑的扩展）
<div class="paragraph"> </div>
</li>
<li> 作为一个高阶逻辑的证明助理，Coq被用于证实一定数量的数学里的重要结果。
比方说，Coq的包含复杂计算进证明的能力使得Coq可以开发出第一个四色定理的式化证明。
这个证明以前在数学家之间有争议性，因为它包含了大量的分情况检查。
在Coq形式化中，包括计算方面的正确性，所有东西都被检查了。
近年来，Feit-Thompson定理，分辨有限单群的第一个大步被在更大的努力下，
在Coq内成功形式化了。
</li>
</ul>
<div class="paragraph"> </div>
如果你对名字感到好奇，Coq官网声称：“一些法国计算机科学家有用动物命名他们的软件的传统：
Caml, Elan, Foc, Phox都是这个隐秘的传统的例子。在法国，“Coq”是公鸡，也
听起来像Calculus of Construction，Coq的基础的首字符。”公鸡同时是法国的国家象征，
“Coq”也是Thierry Coquand，Coq的早期开发人员的名字的头三个字母。
<div class="paragraph"> </div>
<a name="lab6"></a><h2 class="section">函数式编程</h2>
<div class="paragraph"> </div>
函数式编程既代表一系列的，几乎可以在任何编程语言里面用的惯用法，也代表
被设计于强调这些术语的编程语言，包括Haskell，OCaml，StandardML，F#，
Scala，Scheme，Racket，Common Lisp，Erlang，还有Coq。
<div class="paragraph"> </div>
函数式编程已经有数十年历史了—实际上，它甚至可以追溯到Church的λ演算，
这可是发明与1930年代，内时候计算机时代还没开始呢！
自从90年代初以来函数式编程享受了业界的软件工程师与及语言设计者的兴趣的激增，
并且在如Jane St. Capital，Microsoft，Facebook，与及Ericsson等公司的高价值的
系统有关键地位。
<div class="paragraph"> </div>
函数式编程的最基础宗旨是，尽可能的，计算应该是纯的，也就是说，
执行一段代码的效果只有生成结果：计算应该与输入输出，赋值，可变变量，指针重定向等脱离。
比如说，一个指令式的排序函数接受一个数字列表，重组指针，使得列表被排序，
一个纯的排序函数会取一个列表，返回一个含有同样数字，但是被排序的新列表。
<div class="paragraph"> </div>
用这样的风格编程的最明显的好处是这样做使得程序更容易被明白/进行论证。
如果在一个数据结构上的所有操作返回新数据结构，并且旧的结构没有被改动，
我们就不需要担心旧的数据结构会不会在其他地方用到，
改程序的一部分会不会破坏程序的另一部分的属性。
在并发式程序中，每一块可改状态都是漏洞的潜在来源，所以这些考虑变得更关键。
事实上，业界最近对函数式编程的兴趣一大部分来源于在并发下，它的简洁的行为。
<div class="paragraph"> </div>
最近人们对函数式编程的兴奋还有另一个，跟第一个原因有关的原因：
函数式程序经常比指令式程序更容易并行化。
如果一个计算没有除了生成结果以外的作用，他什么时候被执行就毫不重要。
类似的，如果一个数据结构从来没有被修改，它可以被随意复制到任何地方。
的确，位于超大量分布式计算处理器（如Hadoop）的中心，
并且被Google用于索引整个互联网的MapReduce惯用法就是函数式编程的经典例子。
<div class="paragraph"> </div>
对于这个课程来说，函数式编程有另一个重要的地方：
它充当了逻辑与及计算机科学的桥梁。
事实上，Coq自身可以被看成微小但是有极大表达能力的函数式编程语言与及
一系列用于声明/证明定理的工具的集合体。更多的，当我们做更深的检测的时候，
我们会发现Coq的这两边其实是同一机制的两面（比如，程序则证明）
<div class="paragraph"> </div>
<a name="lab7"></a><h2 class="section">程序验证</h2>
<div class="paragraph"> </div>
本书的前三分之一被用于发展逻辑学与及函数式编程的概念框架，
与及提升用Coq对非平凡构造的建模，论证的熟练度。
从此之后，我们会续渐地把重心偏移到两个对构建可靠软件（以及硬件）
有核心重要性的话题上：用于证明特定程序的属性的与及
用于证明对于一整个编程语言都满足的属性的技巧。
<div class="paragraph"> </div>
对于这两个话题，我们要做的第一件事是找出一个用数学对象表示程序的方法，
与及用函数/关系表示它们的行为，因为我们需要对它们进行精确的描述。
我们这方面的工具是抽象语法（Abstract Syntax）与及操作语义，
一个通过写抽象解释器规定程序行为的方法。
在一开始，我们尽量用“大步（big-step）”的，更简单可读的操作语义，
之后，我们会转换到一个更细节化的“小步（small-step）”的，
可以在不终止的程序与及包含更多语言特性（比如并行化）下更有效的风格。
<div class="paragraph"> </div>
我们第一个考虑的编程语言是Imp，一个微小但包含了变量，赋值，条件，循环的编程语言。
我们会学习两张不同的对Imp程序论证的方法。
<div class="paragraph"> </div>
第一，我们考虑我们该如何空额手两个Imp程序是等价的-对所有的内存状态，有同样的行为。
这个等价的观念因此成为了对元程序（操控程序的程序，比如编译器，优化器）的正确性的标准。
我们也会构建一个简单的优化器，并证明其正确性。
<div class="paragraph"> </div>
第二，我们开发一个用于证明Imp程序满足他们行为的形式化规范的方法学。
我们引入霍尔三元组-Imp程序，跟描述程序开始之前/结束之后所满足的条件-
前条件，后条件的概念。与及霍尔逻辑，一个专用于方便地对命令式语言进行论证，
内建了循环不变项（loop-invariant）等概念的“领域特定逻辑”的论证基础。
<div class="paragraph"> </div>
这课程的这一部分是打算给读者尝试
在一系列现实的软件与及硬件的证明工作里面用到的关键概念与及数学工具。
<div class="paragraph"> </div>
<a name="lab8"></a><h2 class="section">类型系统</h2>
<div class="paragraph"> </div>
我们的最后一个主要话题，类型系统，一组用于构建对于一个编程语言里面所有程序的属性的工具，
包含了课程的最后三分之一部分。
<div class="paragraph"> </div>
类型系统是最久经考验，也是最流行的轻量级形式化验证手段的例子。
他们的论证能力很一般-以至于自动检查器可以在编译器，连接器，分析器里面建造，
然后被不明白类型系统理论的程序员应用。（其他的轻量级形式化方法的例子包括
硬件及软件的模型检查器，契约检查器，与及运行时属性检查器）。
<div class="paragraph"> </div>
这个话题使得这个课程圆满：我们在这一部分研究的语言，simply typed lambda calculus，
本质上就是Coq自身的内核的一个简化的模型！
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab9"></a><h1 class="section">现实细节</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab10"></a><h2 class="section">章节依赖性</h2>
<div class="paragraph"> </div>
一个章节之间的依赖性与及一些建议路径的图可以在文件<span class="inlinecode"><span class="id" type="var">deps.html</span></span>中找到。
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab11"></a><h2 class="section">系统需求</h2>
<div class="paragraph"> </div>
Coq可以在Windows， Linux， OS X上执行。 你将需要：
<div class="paragraph"> </div>
<ul class="doclist">
<li> 一个最近的Coq，可以从Coq网页取得。所有内容都能在8.4下运行。
<div class="paragraph"> </div>
</li>
<li> 一个跟Coq交互的交互式集成开发环境（IDE）。目前为止，有两个选项：
<div class="paragraph"> </div>
<ul class="doclist">
<li> Proof General是一个基于Emacs的IDE。对emacs已经舒适的用户更喜欢这个。
它需要另外安装（google "Proof General"）。
<div class="paragraph"> </div>
</li>
<li> CoqIDE是一个更简洁的独立IDE。它跟Coq一起发布，
但是在一些平台上编译之需要额外安装为了用户界面之类的东西的软件包
</li>
</ul>
</li>
</ul>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab12"></a><h2 class="section">练习</h2>
<div class="paragraph"> </div>
每一章都包含大量的习题。每一个习题都有用一个“星级评分”标记。
星级评分的意义是：
<div class="paragraph"> </div>
<ul class="doclist">
<li> 一星：很简单的，强调课程的重点的习题。对于大部分读者，1-2分钟应该足够了。
养成看到一个就做一个的习惯。
<div class="paragraph"> </div>
</li>
<li> 二星：直截了当的习题（5或10分钟）。
<div class="paragraph"> </div>
</li>
<li> 三星：需要一点点思考的习题（10分钟到半小时）。
<div class="paragraph"> </div>
</li>
<li> 四或五星：更困难的习题（半小时或以上）。
</li>
</ul>
<div class="paragraph"> </div>
有些习题被标注为“高阶”，有些习题被标注为“可选”。
做非高阶，非可选的习题已经够提供一个不错的对核心概念的覆盖率。
可选习题提供一点点更多的关键概念与及可能引起一些读者兴趣的附加主题的额外练习。
高阶练习是给想要更多挑战（以及一个更深的对概念的理解）的读者。
<div class="paragraph"> </div>
请不要把习题的答案放在公众地方：Software Foundation，
作为自学教程与及大学课程，被广泛使用。如果习题答案很容易取得，
这让这本书对一般有会打分的作业的大学课程变得远远没那么有用。
作者特定的要求读者切勿把习题答案放在任何可以被搜索引擎找到的地方。
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab13"></a><h2 class="section">下载Coq文件</h2>
<div class="paragraph"> </div>
一个包含所有“发布版本”的笔记的源代码的tar文件
（作为一系列的Coq脚本与及HTML文件）可在此获得：
<pre>
http://www.cis.upenn.edu/~bcpierce/sf
</pre>
如果你在一个课程里面用这些笔记，你可能有本地扩展的版本的这些文件。
如果如此，你应该用它们，而不是用发布版本。
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab14"></a><h1 class="section">对授课员的标准</h1>
<div class="paragraph"> </div>
如果你有意用这些课件授课，你一定会找到你希望改进，增加的东西。
我们欢迎你的奉献！
<div class="paragraph"> </div>
请您发一封电子邮件给Benjamin Pierce，说明你自己，你希望如何用这些课件，
还有你执行“htpasswd -s -n NAME”的结果（NAME是你喜欢的用户名）。
我们会给你我们的subversion 仓库与及开发者邮件列表：
在仓库中你会找到一个包含更多指引<span class="inlinecode"><span class="id" type="var">README</span></span>。
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab15"></a><h1 class="section">翻译</h1>
<div class="paragraph"> </div>
因为一个志愿者翻译团队，Software Foundation可以在<span class="inlinecode"><span class="id" type="var">http</span>://<span class="id" type="var">proofcafe.org</span>/<span class="id" type="var">sf</span></span>日文中被阅读。
感谢他们的工作！
<div class="paragraph"> </div>
</div>
<div class="code code-tight">
<br/>
</div>
</div>
<div id="footer">
<hr/><a href="coqindex.html">Index</a></div>
</div>
</body>
</html>