（计算机软件与理论专业论文）自动提取源代码的验证模型.pdf

自动提取源代码的验证模型 计算机软件与理论 硕士生：李佩娉 指导教师：张治国 摘要 复杂的软件系统往往有很多未知的系统错误，这些潜在错误给软件的 可靠性、稳定性带来了很大的挑战性。模型检测技术( 建模) 能够从软件 的源代码中提取出该软件的形式化模型，继而可以采用验证工具对该形式 化模型进行验证并且能够定位出软件的潜在错误。然而，事实证明，人工 建模是非常耗时耗力并且建模很容易引入未知错误，不能如实反映软件系 统。对于大规模的软件系统来说，即使是经验丰富的专家也觉得难以下手。 因此，人们越来越希望有一种自动或者接近自动的模型提取方法。 基于以上分析，本文对建立软件的形式模型进行了大量的研究，并且 提出了一种解决方案自动提取源代码的验证模型( 形式模型) 本文 的研究工作包括：1 、对c 语言的各种语句进行语义分析，把分析的语句 等价转换成以表达式的形式来描述，从而建立了形式模型；2 、在实现过程 中，本文选用了一种c 语言的解释工具- - - - - c t o o l ，把源代码转换成抽象 语法树( a s t ) ，从而实现对语句抽象等级模型的建立。然后对抽象语法 树进行等价语义转换，从而建立表达式抽象等级模型，也就是形式模型。 本文利用c a d e n c es m v 工具对形式模型进行模拟实验，计算模型的结 果。比较c 源代码的结果和模型的计算结果，两者是相等的实验结果表 明提取的模型和源代码是等价的，从而证明本文提出的模型自动提取方法 是有效的。本文提出的自动模型提取方法节省了建模的耗费，同时也真实 的反映系统的源代码。 关键字：模型提取，源代码，模型检验，抽象语法树( a s t ) a u t o m a t i ce x t r a c t i o no ff o r m a l m o d e lf r o mr e a ls o u r c ec o d e s o f t w a r ea n dt h e o r e t i c a lc o m p u 协rs c i e n c e n a m e ：l ip e i p i n g s u p e r v i s o r ：z h a n gz h i g u o a b s t r a c t t h e r ea r cal o to fu n k n o ws y s t e me r r o r sw h i c ha r eb i gc h a l l e n g et os o f t w a r e r e l i a b i l i t ya n ds t a b i l i t yi nc o m p l e xs o f t w a r e m o d e ld e t e c t i o nt e c h n i q u e ( m o d e l i n g ) b a s e d0 1 1t h es o f t w a r es o u r c ec o d eo ft h es o f t w a r ei st oe x t r a c tt h e f o r m a lm o d e lo fs o f t w a r ea n dt h e nv a l i d a t et h ef o r m a lm o d e lf o rd e t e c t i o no f p o t e n t i a le r r o r h o w e v e r , f a c t sp r o v et h a ta r t i f i c i a lm o d e l i n gi sn o to n l yv e r y p h y s i c a l l yt a x i n ga n dt i m e - e o u s u m i n g , b u ta l s om o d e l i n gi se a s y t oi n t r o d u c e u n k n o w ne l f o e s f o rl a r g e - s c a l es o f t w a r es y s t e m s , e v e nt h em o s te x p e r i e n c e d e x p e r t sa l s of o u n di th a r dt os t a r t t h u s ，a l la u t o m a t e do rn e a r l ya u t o m a t e dw a y o fe x t r a c t i n gm o d e li sh i g h l yd e s i r a b l e b a s e do nt h ea b o v ea n a l y s i s ，t h i sp a p e rh a sag r e a td e a lo fr e s e a r c ho nt h e m o d e ld e t e c t i o nt e c h n i q u e ( m o d e l i n g ) t e c h n o l o g ya n dp r o p o s e san e ws o l u t i o n , a u t o m a t i ce x t r a c t i n go f f o r m a lm o d e lf r o mr e a ls o u r c ec o d e t h i sa r t i c l ei n c l u d e s , f i r s t l y , b u i l dm o d e lo f s t a t e m e n ta b s t r a c t i o nl e v e la f t e rs e m a n t i c a l l ya n a l y z i n g d i f f e r e n tk i n d so fs t a t e m e n t so fcc o d e t h e nb u i l dt h ef o r m a lm o d e lo f e x p r e s s i o na b s t r a c t i o nl e v e lf r o mm o d e lo fs t a t e m e n ta b s t r a c t i o nl e v e l t o i m p l e m e n t a t i o nt h i sm o d e l i n gm e t h o d , t h i st h e s i sc h o o s e sacp a r s l 目fc a l l e d c r o o l , w h i c hc o n v e r t sc c o d et oa b s t r a c ts y n t a xt r e e ( a 踊，t oi m p l e m e n t a t i o n b u i l d i n gm o d e lo fs t a t e m e n ta b s t r a c t i o nl e v e l a n ds e m a n t i c a l l yt r a n s l a t et h i s a s tt of o r m a lm o d e ld e s c r i b e di ne x p r e s s i o na b s t r a c tl e v e l t h i st h e s i su s e sc a d e n c es m vt os i m u l a t et h i sf o r m a lm o d e lf o re x p e r i m e n t a n di tc o m e so u tt h er e s u l to fm o d e l c o m p a r e dt h er e s u l t so fcr e a ls o n r o ：c o d e a n dt h em o d e l b o t ho ft h e ma r et h es a m e n ee x p e r i m e n ts h o w st h a tt h em o d e l e x t r a c t e da n dt h er e a ls o u r c ec o d ea r ee q u a l , w h i c hp m v e st h em e t h o dt h i st h e s i s p r o p o s e si se f f i c i e n t t h i sm e t h o do fe x t r a c t i n gm o d e lf r o mr e a ls o u r s ：c o d ec a n ；a v et h ec o s ta n d e x p r e s sr e a ls o u r c ec o d ec o r r e c t l y k e yw o r d s ：m o d e le x t r a c t i o n , r e a ls o u r c ec o d e ，m o d e lc h e c k i n 舀a b s t r a c ts y n t a x t r e e ( a s l 3 i i i 中山大学硕士学位论文 自动提取源代码的验证模型 第1 章问题陈述 本章首先总括问题背景，然后阐述本文需要解决的问题，介绍研究背 景，详细阐述目前相关的研究技术，然后综述本论文的主要工作，最后介 绍本论文的结构安排。 1 1 背景介绍 1 1 。1 模型检验 模型检验方法【1 】将原始设计表示成有限状态机，将要验证的性质用时 态逻辑描述。然后，遍历有限状态机以检验性质是否存在。模型检验的优 点是：全自动进行，无须人机交互。当断定某性质不满足时，模型检验能 提供导致出错的路径，以便于定位设计错误。图1 - 1 是模型检验的输入输 出。凭借时态逻辑强大的描述能力，模型检验能够对各种复杂的时序性质 进行验证。模型检验的主要缺点包括为系统建立模型困难，模型往往影响 到检验的有效性，状态空间爆炸问题。 围1 - 1 模型检验输入输出 模型检验的主要过程有以下三个步骤【1 】。 1 ) 建摸( m o d e l i n g ) 第一步是要把系统转换成模型检验机可接受的形式。在很多情 况下，这只是简单的编译工作。但在其它情况下，由于时间和内存 的限制，对系统建模需要模型提取以减少无关的或者不重要的信 息。本文主要研究的内容是对c 源代码建立模型。 第1 章问题陈述 添加性质( p r o p e r t y ) 在验证之前，需要说明系统满足的性质。这些性质通常以用某 种逻辑形式描述的。对于硬件和软件系统，它可以断言系统行为是 如何随着时间而发展的。 3 1 验证( v e r i f i c a t i o n ) 在验证中，计算机工具执行运算法则来验证系统的正确性。用 户给出系统的模型和性质描述。通过这些参数，就可以完成对一个 模型的验证。 相对于演绎方法来说，基于模型的检测方法有两个主要好处： 一旦系统模型被构建并且验证属性被设计好，验证过程完全自动 化，输出“是”和“否”；可以生成系统不满足属性的错误路径，使用 户可以根据这些信息修改模型。也就是如果出现错误，会输出导致 出错的一条路径，表示在哪种环境下此错误会出现，使用户能定位 错误并修复模型。 目前有很多验证工具，本文在实验中用到c a d e n c es m v 验证 工具，它是一个c a d e n c e 版本的符号模型检验机。详见第5 章。 1 1 2 模型建立存在的问题 模型检验在检测软件系统错误，提高软件系统可靠性方面是可行有效 的。然而，在模型检验系统代码可行有效的同时，建立模型是非常困难的。 即使是专家为大规模系统构建模型也不是一件容易的事【5 】。建模花费的时 间往往比写代码的时间还要多。为了构建模型，测试专家要与系统的设计 者沟通，有时甚至要研究源代码的应用开发，了解设计意团5 】。这个过程 或许需要几天，几周，有时甚至几个月。这是使用模型检验机的一个缺点。 由于市场的限制，生产商希望尽快卖出自己的产品，所以产品实现后额外 测试调试的时间通常是很少的。因此，自动或者接近自动模型提取方法可 以在保证质量的同时减低测试的耗费。 此外，测试技术应用在设计阶段还是实现阶段，是争议的话题。在设 2 中山大学硕士学位论文自动提取源代码的验证模型 计阶段发现错误会减少实现的开销，所以在设计阶段测试是一个很重要的 研究主题【6 】，例如u m l 。但是，对代码的测试也是不可忽视的，因为尽 管设计得再仔细，代码可能包含一些严重的错误。这些错误在系统的设计 中不存在，但出现在系统的实现中【6 】。在设计阶段检测模型比直接检测代 码更容易丢失这种错误。因为在设计阶段检测过程中需要大量的人为干预， 牵制了在实际系统中模型检验的使用。在人为抽象过程中，人为的错误会 在验证过程中丢失错误出现假的警告，从而增加模型检验的代价，减少模 型检验的有效。这种错误会在构建模型的时候被传入，在真实系统进化中 作为结果被“流传”【刀。因此，直接对源代码进行模型提取可以降低这类 错误的丢失率，减少人为干预的程度。 总的来说，建模存在两方面的问题：建模是非常耗时耗力并且建模很 容易引入错误。针对这两个问题，本文提出了一种自动模型提取方法，这 种自动提取方法节省了建模的耗费，同时经过实验证明是真实的反映系统 的源代码。 1 1 3 本文的解决方法 模型检验在检测软件系统错误，提高软件系统可靠性方面可行有效的 同时，建模过程也存在上述两方面问题一建模是非常耗时耗力和建模很 容易引入未知错误。基于上述两方面的问题，本文的研究目标是自动提取 源代码的验证模型( 形式模型) 。 本文对c 语言的各种语句进行语义分析把分析的语句等价转换成以 表达式的形式来描述，从而建立了形式模型；2 、在实现过程中，本文选 用了一种c 语言的解释工具c t o o l ，把源代码转换成抽象语法树 ( a s t ) ，从而实现对语句抽象等级模型的建立。然后对抽象语法树进行 等价语义转换，从而建立表达式抽象等级模型，也就是形式模型。 本文利用c a d e n c es m v 工具对形式模型进行模拟实验，计算模型的结 果。比较c 源代码的结果和模型的计算结果，两者是相等的。实验结果表 明提取的模型和源代码是等价的，从而证明本文提出的模型自动提取方法 3 第l 章问题陈述 是有效的。本文提出的自动模型提取方法节省了建模的耗费，同时也真实 的反映系统的源代码。 1 2 研究现状 目前对代码进行模型检验的研究已经有很多方法和工具。软件系统建 立形式模型的方法大概归类为以下六种【8 】 1 1 手动用形式语言直接创建一个软件模型，在模型检验机上进行检 测。这种方法要把系统分别用两种语言实现，一种是用于模型检验 的，另一种是用于系统实现的。 选取软件实现语言中的一个子集，直接用这个子集编写模型检验程 序。例如c 模型检测机( cm o d e lc h e c k e r ，c i v i c ) 【刀，扩展的j a v a 静态检测机( e x t e n d e ds t a t i cc h e c k e rf o r j a v a ，e s c l j a v a ) 【9 】。 3 、选取软件实现语言中的一个子集，把这个子集直接转换成形式语 言例如j a v a 路径探寻器( j a v ap a t h f i n d e r ，j p f ) 【i o 。 钔提取系统( 用软件实现语言实现) 的中间模型，再把中间模型转换 成形式模型。例如采用自动谓词抽象方法的c 2 b p 2 。本文采用这 种方法来实现模型的自动提取。 研在可执行设计阶段用软件描述语言开发系统，把这个设计模型转换 成形式语言。例如u m l 。 6 ) 通过测试可执行的路径来模型检验系统性质。例如受限的c 模型 检测机( cb o u n d e dm o d e lc h e c k e r ，c b m c ) 【1 1 1 。 1 2 1c 模型检测机 c m c 用是c 模型检测机( c m o d e lc h e c k e r ) 的缩写，它通过直接执行 原来的c 但+ + 代码来生成给定系统的状态空间。c i v i c 把系统建模为交互并 发行为( 进程) 的集合。对于每个进程运行未更改的a c + + 代码，c i v i c 4 中山大学硕士学位论文自动提取源代码的验证模型 负责安排和执行待测系统的进程。c m c 和所有的系统进程运行像一个简单 的操作系统。但和操作系统不同的是，c m c 试图寻找更多可能的系统状态， 这些状态是由选择不同的事件安排来决定的和其它不确定事件触发的。为 了能寻找这些不同的可能状态，c i v i c 必须能够保存和恢复系统的全部状 态。系统的每个进程在各自的堆和栈中执行。任何时刻，进程的状态由全 局变量的备份、堆、栈和它的上下文寄存器组成。进程通过进程上下文访 问共享内存进行通讯系统的状态可定义为所有进程和共享内存的联合 一旦预定执行的顺序，进程被允许执行一个确定的无阻塞的指令集，这个 过程叫转换。一个转换是原子步。 从c c + + 程序创建一个c m c 模型的步骤如下： 1 1 指定正确属性 在系统测试前，用户必须指定正确属性。有些属性不受范围约 束的。例如，程序不能访问不合法的内存和出现内存泄漏。有些有 特定范围属性必须作为断言在特殊的点指定。另外有些属性是全局 的。例如要求在路由表中不会出现回路。这种属性被指定为访问进 程上下文数据结构的布尔函数( 用c 语言写) 。 2 ) 建立测试环境 下一步，用户必须建立测试环境。对于网络协议，环境模型用 函数来模拟操作系统和协议之外的所有必须的东西。环境模型是替 代的a p i 函数和模拟该系统的数据结构的集合例如，用 c m c c h o o s c ( i n t ) i 弱数对非确定性的模拟。输入，此函数将随机的 返回0 到n - i 中的一个数。 v o i d * 髓l l o c ( s l z e _ tn ) f i f ( a l o c h o o s e ( 2 ) - o ) r e c a z 丑o ：，n 叫坩e t 舶擒i n i b t i cf a i l u r e a l l o cnb y t e sl r 谴h 砷硼r e g u r n ) 图1 2 在q l c m a n o c 。的实现非确定的分配内存 3 ) 提供初始函数和系统中每个进程的事件处理器 第1 章问题陈述 给定一个事件驱动的系统，用户必须提供初始函数和系统中每 个进程的事件处理器。用户还可以为每个事件处理器提供一个保护 函数。该函数是一个布尔函数，在给定状态时，决定事件处理器什 么时候有效。 1 2 2 扩展的j a v a 静态检测机 扩展的j a v a 静态检测机( e x t e n d e ds t a t i cc h e c k e rf o rj a v a ，e s c j a v a ) 【9 】是一个寻找普通程序错误的程序检测机。静态是指实现检测过程不需要 运行程序，扩展是指e s c 能比传统的静态检测机找到更多的错误。e s c 用 自动定理验证技术来对程序的语义进行检验，使之可以警告很多在运行时 间被现代编程语言找出的错误( 空引用，数组超界错误等等) 。它为程序员 提供了一种简单的可以形式表述设计结果的注释语言e s c j a v a 检查已注 释的软件，警告注释的设计结果和真实代码之间的矛盾，同时还警告代码 中的潜在运行时间错误和并发程序的同步错误( 死锁等) 1 2 3j a v a 路径探寻器 j a v a 路径探寻器( j a v ap a t h f i n d e r ，j p f ) f 1 0 是自动把j a v a 转换成 p r o m e l a 的工具，p r o m e l a 是s p i n 模型检验机的建模语言。j p f 允许程序员 用断言去注释他的j a v a 程序，用s p i n 模型检验机来验证。此外，死锁会 被识别出来。断言被指定为一些特殊类( 验证类) 的静态方法调用。j p f 支持j a v a 中的重要子集，也就是：动态生成具有数据和方法的对象，静态 变量和静态方法，类继承，线程和用于建模监控的同步原语( 同步声明， 等待和通知方法) ，异常，线程中断和大多数的标准程序语言结构，例如 赋值语句，条件语句和循环但是这个转换机仍然是一个原型，忽略了j a v a 的某些特点，例如包，过载，重要方法，递归，字符串，浮点数，某些线 程操作( s u s p e n d 和r c s u m c 操作) 和某些控制结构( c o n t i n u e 语句) 。 6 中山大学硕士学位论文 自动提取源代码的验证模型 1 2 4 自动谓词抽象方法 g r a fa n ds a i d i 首先提出了一种自动构造抽象模型( a u t o m a t i cp r e d i c a t e a b s t r a c t i o no fcp r o g r a m s ) 的方法，也就是谓词抽象【2 】。运用谓词抽象方法， 系统的具体状态可以根据它们在一个有限的谓词集中的值来定位抽象状 态。软件的谓词抽象有很多应用，包括探测程序错误，合成程序不变量， 通过谓词敏感性来提高程序分析的精确度。 c 2 b p 2 是在c 程序上运用自动谓词抽象方法提取形式模型的工具。 c 2 b p 是s l a m 工具包的一部分，s l a m 是一个结合运用谓词抽象，模型 检验，象征推理，重复提炼方法来静态检测暂时安全属性的程序。 给定一个c 程序p 和一个谓词集合e ( 纯c 没有函数调用的布尔表达 式) ，c 2 b p 自动地生成一个布尔程序b 附，e ) ，它是p 的抽象。一个布尔 程序本质上是一个只能使用布尔类型的c 程序。布尔程序的控制流结构与 p 的相同，但是只包括j e l 个布尔值，每一个布尔值代表e 中的一个谓词。 例如，如果e 中的谓词( x y ) ，其中x 和y 是p 中的整型变量，b p 假e ) 中有一个布尔值，当程序p 在p 点时如果( x - ，t ，一等等，格式如下： r e l a t i o n s h i p e x p r e s s i o n - e x p r l e x p r 2 r e l a t i o n s h i p e x p r e s s i o n - - , e x p r l = e x p r 2 r e l a t i o n s h i p e x p r e s s i o n 。e x p r l 一e x p r 2 第2 章对c 代码建模 曲三元表达式( 也称条件表达式c o n d i t i o n a le x p r e s s i o n s ) 其格式如下：c o n d i t i o n a l - e x p r e s s i o n _ 明”j ? 口c p r 2 ：e x p r 3 选择语句( i f i 吾句) 的提取 因为三元表达式和i f 语句在语义上是等价的，可以把i f 语句 转换为条件表达式。对于i f 语句： i f 。s t a t e m e n t i f ( e x p r e s s i o n ) s t a t e m e n t le l s es t a t e m e n t 2 ，提取如 下：i f 。s t a t e m e n t - - e x p r e s s i o n ? s t a t e m e n t l 7s t a t e m e n t 2 。最后通 过对s t a t e m e n t l 和s t a t e m e n t 2 的提取，确定最终的表达式。 3 ) 重复语句( w h i l e 语句) 的提取 w h i l e 语句可以由多个i f 语句来表示，所以在语义上，可以把 w h i l e 语句等价的转换为多个三元表达式。因为循环的次数在处理 的过程中是不确定的，所以在实现过程中本文使用循环次数受限的 方法来确定每次w h i l e 循环的次数。第3 章将会详细讨论。对于 w h i l e 语句： w h e 。s t a t e m e n t w h i l e ( e x p r e s s i o n ) b o d y ，提取如下： 砌池一s t a t e m e n t e x p r e s s i o n ? b o d y ：n u l l ；e x p r e s s i o n ? b o d y ? n u l l ； 最后通过对b o d y 的提取，确定最终的表达式。 2 2 建立模型 2 1 节分别从语句等级和表达式等级来分析了c 代码的语义，等价从语 句等级映射到表达式等级，并分析了各种语句提取的规则。使用这些规则 定义从程序代码到模型抽象和语义的转换，建立形式模型。 本文要提取的形式模型是基于表达式等级的表达式描述的。因为状态 是用变量来描述的，每次转换的结果都是变量值的改变。所以把焦点转移 到代码所定义的变量上，把变量的改变条件映射为模型状态的转换条件， 把改变后的变量加上相应的下标映射为模型的状态。因为针对的是变量， 1 4 中山大学硕士学位论文自动提取源代码的验证模型 所以代码中每个语句都要用表达式来描述。使用表达式形式描述的形式模 型是不存在选择性结构和重复性结构的。所以本文要把选择性结构和重复 性结构转换成表达式描述的循序性结构。建模过程中，在各个变量后加入 下标来实现结构的转换。 表2 1c 语言各种结构的流程图 循序性结构选择性结构 重复性结构 f o r 语 i f e l s e w h i l e 法 s w i t c h c a s e d o w h i l e l 唐 ， j r 量叫一 流 s t a t c m c m l t 程 0 s m c w , e m 21 图 s 埘e m c m 2 1 卣 l 竺一 根据2 1 2 节，表达式等级可以由语句等级提取而来，本文要提取的形 式模型是基于表达式等级的表达式描述的。形式模型建立规则如下： 1 ) 对每一个变量添加下标。对变量添加下标可以使同一变量在表达式 之间的联系分离，从而分离了表达式之间的关系。最终把选择性结 构和重复性结构转变成循序性结构。 代码中赋值语句直接转换为赋值表达式。 3 1 代码中i f 语句等价于三元表达式。i f 语句可以分成条件部分，t h e n 部分和e l s e 部分在对i f 语句建立形式模型时，要先分析i f 语句 的t h e n 部分和e l s e 部分，从而记录在j f 语句修改过的变量和变量 修改后的下标值。如此，在处理i f 语句时。直接在三元表达式的 相应位置填入变量和修改后的下标值。 l f i 第2 章对c 代码建模 代码中w h i l e 语句的转换是本文研究的难点。因为循环的次数在建 模过程中是未知的。先设定w h i l e 语句n 次( n 是一个用户设定的 常数) 循环。如果循环在少于n 次停止，则输出结果。如果条件在 1 1 次循环后仍然满足，则设定一个比n 大的循环次数，如此进行， 直到条件不满足。在例子中，本文设定n = 3 给定图2 - 3 的c 代码，本文可以画出它的流程图。 图2 - 3 c 代码和流程图 按照形式模型的建立规则，图2 - 4 是c 代码流程图到形式模型的转换 过程，图2 5 是形式模型的描述。 1 6 中山大学硕士学位论文自动提取源代码的验证模型 r 曼。翠l上孓旦i ；高丁1 高 蚺- 怛hn ? 妇：碡 归- 0 4 f i l ”y l ：业 l 甲甲 l “酽蝥卜倒暑， 亨患宁 热h 丰圳 l ：毫 中 l “蒈驽卜丰圳 圈2 4c 代码流程图到形式模型的转换 x l = o ： v l = 5 ： x 2 = x l y l ； x 3 = 2 ： y 2 = 3 ： x 4 = ( 蛇= = 1 ) ? 好：x 2 ； y 3 = ( x 2 = = 1 ) ? y l ：y 2 ； x 5 = x 4 + l ： 面= ( x 4 5 17 x 5 ：x 4 ； x 7 = x 6 + 1 ： x 8 = ( x 6 t r a v e m e _ d c c l a r a t i o n o h k ) ；) v m u a l v o i dp r i n t ( s t d ：o s t r e a m & o u t 缸l c v c l ) c o a s t ； 图4 - 5 声明语句类图 d e c l s t o m g e t y p cs t o r a g e ； t y p cf o r m ；l e ，i n t 嗣 s y m b o l+ n a m e ；t h es y m b o l b e h t gd e c h t e d f w r c s s i o n i n i t i a l i 2 r ； 酬 a e ：u t ；，f o rh n k l n gi n t o 地“ p e e l ( s y m b o l s y m = ( s y m b o l * ) n u l l 陬m t y 肚。t y p e x - d e c l o ； 圈4 _ 6 声明类图 中山大学硕士学位论文 自动提取源代码的验证模型 i f 语句类 璐t e m n t i 珈- s s l o n c o n d ； s t a t e m e n t t h e n l 3 1 k s t a t e m e n t+ c k c l 珈lc a nb en u l l 睦s t e m a t ( e w r e s s i o n c o n d s t a t e m e n t t h e n b l k , c o a s tl o c a t i o n & l o c a t i o n , s t a t e m e n t c k c b i k ln i j u 土 - 1 6 t c m m ( 1 ； v k t u a l v o i da c c e p t ( t r a v e t s a l 0 t - ，h t m v e s s o _ i f ( t h i s ) ；) v o i d p r m t ( s t d ：o s t r e a m & o u t , i n t k v e n c o n s t ； w h i l e 语句类 田 让语句类田 w h 豇e