Combining Coq and Gappa for Certifying Floating-Point Programs - ppt

现有的语义学大致可以分为4类：操作 语义学、指称语义学、公理语义学和代数语 义学。
在操作语义学中，程序语义的定义由一个 模拟程序解释的形式系统组成，即是一个由程 序所规定的一系列活动的执行过程。
这种方法的中心目的是确定一个解释主语 言抽象程序的抽象机。
机器通过一个离散状态序列来解释程序。
在指称语义学中，程序的指称语义比操 作语义更为抽象。
个 S j , j1…n，Qi(i1…r)是Sj的前置条件， Rk(k1…t)是Sj的后置条件。如果
(j1L n)├( Vsj (Q1,Q2 L ,Qr;R1, R 2,L , R t ))
那么
├{φ}P{ψ}+
3．程序的完全正确性证明
（1）良序集
用FLOYD方法证明程序的终止性，要依 赖于良序集的概念。我们说集合C关于“＞” 是良序的，如果对于x、y、zC，有： ● x≠y，那么x＞y或y＞x；
然而，这种机制在证明验证条件时才被应 用。因此，证明技术不能指导程序的开发。
12.2.6 HOARE的公理方法
1969年，HOARE在FLOYD理论的基 础上，定义了一个小语言和一个逻辑系统， 此逻辑系统含有程序公理和推导规则，目的 在于证明程序的部分正确性。此系统是一阶 谓词逻辑的扩充，这就是著名的HOARE系 统。
5．FLOYD归纳断言法存在的问题
FLOYD归纳断言法的主要缺陷是语法 和语义定义的相互独立性，在程序的开发中 没有形式地考虑它们最终的验证。在证明验 证条件失败的情况下，或者是由于程序的错 误，或者是由于有些断言不能被相应的SV定用 什么语法单位代替有错误的语法单位才能保证 验证条件成立；在后一种情况下，存在一个形 式化机制（变换器SVC）来帮助我们判断在语 法单位运行以后哪个断言是成立的。

程序员在完成某个模块的编程之后，一般总是要先对该模块 进行私下的测试，此时，可以先用白盒法选择(xuǎnzé)一些例子检 验程序的内部逻辑，再用黑盒法补充一些例子。程序员本人经私 下测试后认为程序根本可行，才会将程序交付出来。程序交付出 来之后，由其他人员以黑盒法为主再次对该模块进行测试。
联合测试又称集成测试或联调，其目的是根据模块结构图将 各个模块连接起来进行，以便发现问题。联合测试可以发现概要 设计时犯的错误，如模块界面上的问题等。与后面的系统测试一 样，联合测试的主要目标已不是发现模块内部的错误，所以通常 只采用黑盒法。
评审条款随系统的不同(bù tónɡ)可有所不同(bù tónɡ)，可根据软 件系统的性质和复查专家的经验来设定。
第九页，共14页。
第5章 软件检验
5.3 正 确 性 证 明
动态检验和静态检验的根本问题在于不可能说明软件中不存在错误， 人们所能做到的最好的结果是发现错误，因此自然希望(xīwàng)能找到 某种方法能确切地证明程序是没有错误的，这就出现了程序正确性证明 的研究领域。
第5章 软件检验
X Y
Z
模块X
图5.1 程序的输入(shūrù)变量与输出变量
第三页，共14页。
第5章 软件检验
白盒法是指测试人员必须了解程序的内部结构，此时，测 试用例是根据程序的内部逻辑结构来设计的。如果想用白盒法 发现程序中的所有错误，那么至少必须使程序中每种可能的执 行路径都执行一次。
例如，图5.1是一个很简单的程序，它有两个输入(shūrù)变 量x、y，一个输出变量z。假定程序是在字长为32位的计算机上 运行，且x、y都是整数，那么输入(shūrù)数据的可能值有 232×232＝264种。
程序走查(Code Walkthrough)是另一种有效的评审活动。走查的 关键在于：以人工运行作为媒介，通过这种方式启发与会者向程序 员提出种种问题，从而发现程序中的错是 将软件中常见的各类错误列成清单作为评审条款。评审过程中按评 审条款有针对性地进行检查，就可到达多、快、好、省的目的。

运行中是否会出现不能容忍的状态（死锁、活锁等）。
Formal Refinement（精化）：从抽象的高层描述出 发，严格地保语义地推导更接近实现的包含更多细节 的规范；通过反复精化，最终得到正确的可运行程序。
形式化规格
软件规格是指对软件系统对象及用来对系统对象进行 操作的方法集合，以及对所开发系统中的各对象在其 生存期间里的集体行为的描述。
形式化方法： 对未被聘用的应聘者，应尽快通知他们，尤其是最后候选人名单上的应聘者。他们想知道未补聘用的原因，一些有益的反馈会对他们
将来找工作有所帮助。 第三，注意车辆型号的搭配，同一个品牌的车，可能有不同的系列，有的车从小到大，有的车带天窗，有的车没有天窗，不同型号
的（规车1则）都 ，短应因跑搭为等配这项展时目示人要基用。身按体照于 自的规冲严 动定力的很格 化跑大道，定 或进精行力义 半，又不的 自集能中串数 动在跑竞学化道技。之概的这中不，念工仅思仅想和具是上竞语进毫赛无的言行戒要备。检求，，一语查也旦是相义和安互全清分绊的倒保晰 析，障就。，可特能无别严是重歧快受到伤义终。点。冲刺可时，以更要遵守
软件开发的期望
软件质量稳定，可靠性高 尽量提高开发的效率 尽量降低开发的成本
问题：现在的情况怎么样？
软件开发的实际情况
软件开发的实际情况并不乐观
项目经常延误，预算经常超支 开发的后续阶段常发现许多前期设计错误，更正
的代价高昂 发布运行的软件中常常存在着许多错误，时常崩
溃 软件维护和更新工作的代价很高
Formal Specification（形式化规格）：采用具有严 格数学定义的形式和语义的记法形式，描述软件设计 和实现;
Formal verification（形式化验证）：对形式化规范 进行分析和推理，研究它的各种静态和动态性质

4
Things are not getting easier The environment is becoming even less benign: • The overall market is much larger, so the potential cost of recall/replacement is far higher. • New products are ramped faster and reach high unit sales very quickly. • Competitive pressures are leading to more design complexity.
6
Limits of testing Bugs are usually detected by extensive testing, including pre-silicon simulation. • Slow — especially pre-silicon • Too many possibilities to test them all For example: • 2160 possible pairs of floating point numbers (possible inputs to an adder). • Vastly higher number of possible states of a complex microarchitecture. So Intel is very active in formal verificat verification work Intel uses formal verification quite extensively, e.g. • Verification of Intel® Pentium® 4 floating-point unit with a mixture of STE and theorem proving • Verification of bus protocols using pure temporal logic model checking • Verification of microcode and software for many Intel® Itanium® floating-point operations, using pure theorem proving FV found many high-quality bugs in P4 and verified “20%” of design FV is now standard practice in the floating-point domain