（计算机应用技术专业论文）线性时序逻辑在失业保险审计中的应用研究.pdf

气 c l a s s i f i e di n d e x ： u d c ： ad i s s e r t a t i o nf o r t h ed e g r e eo fm e n g a p p l i c a t i o no f l i n e a r t e m p o r a ll o g i c o n a u d i to f u n e m p l o y m e n t i n s u r a n c e c a n d i d a t e ：h a nb i n g s u p e r v i s o r ：p r o f h u a n gs h a o b i n a c a d e m i cd e g r e ea p p l i e df o r ：m a s t e ro fe n g i n e e r i n g s p e c i a l i t y ：c o m p u t e ra p p l i c a t i o nt e c h n o l o g y d a t eo fs u b m i s s i o n ：d e c e m b e r ，2 0 0 9 d a t eo f o r a le x a m i n a t i o n ：m a r c h ，2 0 1 0 一 u n i v e r s i t y ：h a r b i ne n g i n e e r i n gu n i v e r s i t y 哈尔滨工程大学 学位论文原创性声明 本人郑重声明：本论文的所有工作，是在导师的指导下，由 作者本人独立完成的。有关观点、方法、数据和文献的引用已在 文中指出，并与参考文献相对应。除文中己注明引用的内容外， 本论文不包含任何其他个人或集体己经公开发表的作品成果。对 本文的研究做出重要贡献的个人和集体，均已在文中以明确方式 标明。本人完全意识到本声明的法律结果由本人承担。l 作者( 签字) ：韩卜 日期： 乙o ，。年? 月日 哈尔滨工程大学 学位论文授权使用声明 本人完全了解学校保护知识产权的有关规定，即研究生在校 攻读学位期间论文工作的知识产权属于哈尔滨工程大学。哈尔滨 工程大学有权保留并向国家有关部门或机构送交论文的复印件。 本人允许哈尔滨工程大学将论文的部分或全部内容编入有关数据 库进行检索，可采用影印、缩印或扫描等复制手段保存和汇编本 学位论文，可以公布论文的全部内容。同时本人保证毕业后结合 学位论文研究课题再撰写的论文一律注明作者第一署名单位为哈 尔滨工程大学。涉密学位论文待解密后适用本声明。 本论文( 口在授予学位后即可口在授予学位1 2 个月后口解 密后) 由哈尔滨工程大学送交有关部门进行保存、汇编等。 矿i 二立：i ， 作者( 签字) ：踢纠乙导师( 签字) ：寥文摩 日期：少年乡月形日乙矽年岁月石日 哈尔滨工程大学硕士学位论文 摘要 在社会保险审计的过程中，理解被审计地区的法规和业务流程是非常重 要的环节。各地的法规政策是开展业务的基础，根据法规政策来构建当地的 业务模型也是理解业务的有效手段。目前，模型检测的方法很多，线性时序 逻辑已经受到广泛的关注，并且已经应用到模型检测中。 本文根据法规政策的文本描述，构建当地的业务工作流程。依据时间序 列上业务事件发生的时间不同，对构建的业务模型进行化简、完备失业保险 业务处理流程模型等操作。基于有限状态自动机的失业保险业务处理流程模 型构建完毕后，应用线性时序逻辑对模型的时序性质加以描述，针对该时序 描述，应用线性时序逻辑语言编写程序，程序作为模型检测输入的一部分。 本文提取失业保险法规政策的约束条件，作为失业保险业务模型检测的标准， 再将法规的线性时序逻辑语言描述转换成线性时序逻辑程序，这部分程序作 为模型检测输入的约束条件。以上两部分程序作为输入条件来检测失业保险 业务模型的正确性。 本文利用线性时序逻辑来描述失业保险业务处理流程模型的时序性质。 根据线性时序逻辑语法规则描述的线性时序逻辑公式，应用n u s m v 来检测 构建的模型。避免审计人员和社保人员对生成疑点的意见和看法的不一致， 指导审计方法的生成。 关键词：线性时序逻辑；失业保险审计；有限状态自动机；模型检测 哈尔滨工程大学硕士学位论文 a b s t r a c t i nt h ec o u r s eo fs o c i a li n s u r a n c ea u d i t , i ti so fg r e a ti m p o r t a n c et ou n d e r s t a n d dt h el a w sa n db u s i n e s sp r o c e s s e so ft h ea u d i t e da r e af o rt h e ya r et h eb a s i so f b u s i n e s sp r o c e s s i n g b u i l d i n gb u s i n e s sm o d e la c c o r d i n gt ot h er e g u l a t i o n sa n d p o l i c i e si sae f f e c t i v em e t h o d n o w , t h e r ea r el o t so fw a y sf o rm o d e lc h e c k i n g l i n e a rt e m p o r a ll o g i ch a sb e e nw i d e l yc o n c e m e d ，a n dh a sb e e na p p l i e dt om o d e l c h e c k i n g i nt h i st h e s i s ，t h eb u s i n e s sw o r k _ f l o wi sb u i l ta c c o r d i n gt ot h er e g u l a t i o n sa n d p o l i c i e s i nt h ef o r mo ft e x t a c c o r d i n gt ot h ed i f f e r e n tt i m ew h e nab u s i n e s s h a p p e n s ，b u s i n e s sp r o c e s s i n gm o d e li ss i m p l i f i e da n di m p r o v e dt og e ta l la c c u r a t e m o d e lt od e s c r i b et h eu n e m p l o y m e n ti n s u r a n c eb u s i n e s s a f t e rt h eb u i l d i n go f u n e m p l o y m e n ti n s u r a n c e b u s i n e s s p r o c e s s i n g m o d e lb a s e d - o n a u t o m a t o n , a c c o r d i n gt ot h ed e s c r i p t i o no ft e m p o r a ll o g i c ，l i n e a rt e m p o r a ll o g i cl a n g u a g ei s a p p l i e dt ow r i t ep r o g r a m ，w h i c hw i l lb eap a r to fi n p u to fm o d e lc h e c k i n g t h i s p a p e re x t r a c t sr e g u l a t i o n sa n dp o l i c i e so nu n e m p l o y m e n ti n s u r a n c ef o rt h e yw i l l b et h es t a n d a r do ft h em o d e lc h e c k i n go fu n e m p l o y m e n ti n s u r a n c e a n dt h e nt h e i n e a rt e m p o r a ll o g i cl a n g u a g eo ft h er e g u l a t i o n sa n dp o l i c i e sw i l lb et r a n s f o r m e d i n t ol i n e a rt e m p o r a ll o g i cp r o g r a mw h i c hw i l lb ea p a r to ft h em o d e lc h e c k i n g i n p u t a si n p u tc o n d i t i o n s ，t h ea b o v e - m e n t i o n e dt w op r o g r a m sa r eu s e dt oc h e c k t h ec o r r e c t n e s so fu n e m p l o y m e n ti n s u r a n c eb u s i n e s sm o d e l ，t oa c h i e v et h e p u r p o s eo fa n a l y z i n ga n dc o m p l e t i n gt h em o d e lo fu n e m p l o y m e n ti n s u r a n c e f i n a l l y , t h es e q u e n t i a ln a t u r eo ft h em o d e li sd e s c r i b e d 、i t l ll t l n u s m vi s u s e dt oc h e c kt h eb u i l tm o d e la c c o r d i n gt ot h el i n e a rt e m p o r a ll o g i cf o r m u l a s d e s c r i b e d 诵t l lt h el t lg r a m m a r , w h i c hc a na v o i dd i s a g r e e m e n to nd o u b t f u lp o i n t 哈尔滨工程大学硕士学位论文 1 g e n e r a t e db ya u d i ts t a f fa n ds o c i a ls e c u r i t ys t a f fa n dg u i d et h eg e n e r a t i o no fa u d i t a p p r o a c h k e yw o r d s ：l i n e a rt e m p o r a ll o g i c ；u n e m p l o y m e n ti n s u r a n c ea u d i t ；f i n i t e - s t a t e a u t o m a t a ；m o d e lc h e c k i n g 哈尔滨丁程大学硕士学位论文 目录 第1 章绪论1 1 1 课题背景和意义。1 1 2 课题需求。3 1 3 国内外研究现状。4 1 4 本文研究内容与组织结构。5 1 4 1 论文研究内容5 2 2 自动机的相关概念及化简方法1 0 2 1 1 基于可区分状态表的化简方法：1 0 2 1 2 时间自动机的化简方法。1 l 2 1 3 模糊自动机的化简方法1 2 2 3 模型检测方法及模型检测工具介绍1 3 2 3 1 基于u m l 的模型检测。1 3 2 3 2 模型检测工具介绍1 4 2 4 失业保险特点及失业保险审计流程1 6 2 4 1 失业保险特点及享受条件。1 6 2 4 2 失业保险审计流程18 2 5 本章小结1 9 第3 章失业保险业务处理流程模型构建2 0 3 1 失业保险业务处理流程模型构建步骤2 0 3 2 失业保险业务处理流程模型提出2 0 3 - 3 失业保险业务处理流程模型完善2 2 3 4 失业保险业务处理流程模型化简2 6 3 5 本章小结3 0 哈尔滨工程大学硕士学位论文 第4 章线性时序逻辑表示及检测结果分析3 1 4 1 构建后模型时序性质到l t l 公式转换3 1 4 2n u s m v 的配置过程。3 7 4 3 失业保险业务处理流程模型的检测4 0 4 4 模型检测结果分析4 3 4 5 本章小结4 6 结论：4 7 参考文献4 8 攻读硕士学位期间发表的论文和取得的科研成果5 2 致谢5 3 哈尔滨工程大学硕士学位论文 第1 章绪论 1 1 课题背景和意义 自新中国成立以来，社会保障制度得到不断地完善。城镇以基本养老保 险、失业保险、基本医疗保险为主要内容的社会保险体系和以住房公积金为 基础的住房保障体系日趋完善，农村最低生活保障、新型合作医疗、救灾救 济以及社会养老保险、五保供养等制度基本建立n 1 。初期，社会保障的数据 以档案管理的方式来保存砼1 ，浪费存储空间，不利于资料的检索和更新。审 计单位和社保单位是审计和被审计的关系，审计人员和社保人员对国家法规 政策的理解也是面教口授，如果在法规政策理解方面存在分歧，那么，在审 计工作的最后环节( 疑点核实过程) 中将会出现问题，因为基于同一部分的 法规政策，针对同一个问题产生的疑点，如果审计人员和被审计人员对政策 的理解不一致，对产生的疑点也存在争议，对疑点的认同程度也会不同。假 如存在的较大的理解差异，被审计的单位有可能认为这根本不是一个疑点， 所以，法规的形式化描述是相当重要的，这样可以减少理解的差异。在审计 软件的开发过程中，明确的界定审计方法的关系，这不但是对法规政策理解 程度的体现，也是软件开发过程中对业务需求的一种定义。处理好这些关系 有助于软件开发，帮助理解业务需求。 伴随着科学技术的进步和计算机技术的蓬勃发展，计算机已经应用于许 多领域，近些年来，计算机技术已经应用到社会保障审计工作中口3 ，利用计 算机存储技术替代了纸质形式的文件记录，这无疑是向前迈进了一大步，在 审计的过程中，对已有文件的梳理也是一个重要环节。针对不同的业务将存 储的内容数字化，将这些信息存储在计算机中的形式也要和实际的业务相关 联，针对业务需求将社保数据按照规则进行管理，如果能尽最大的程度的与 国家的法规政策靠拢，那么将会方便审计工作，节省时间、提高工作效率。 随着国家对社会保险重视程度的加大和社会的进步。对社会保险审计的 哈尔滨t 程大学硕士学位论文 要求也就越来越高h 3 ，加之计算机技术在社会保险审计的应用也越来越多、 越来越深入，社会保障方面的计算机审计技术越来越受到各地政府部门及审 计机关的重视。然而，社会保险审计所需要解决的问题也越来越复杂哺1 ，因 为需要处理的数据量愈来愈庞大，社保部门对审计业务的理解程度要求也越 来越高。以失业保险为例，失业保险的业务处理流程具有很强的时间性，参 加失业保险的人员，在失业前、失业中、失业后的状态迁移是在时间的序列 上完成的，这使得失业保险的业务处理流程在时间方面具有较强的依赖性。 所以针对失业保险的业务流程建立相应的社会保险业务模型是非常有必要 的，这不但能够清楚的表达失业保险审计中的业务流程，同时也能够为将来 更好的开展失业保险业务奠定基础，对失业保险业务操作流程也能起到指导 性的作用。在审计软件的开发前期，只有软件开发人员了解审计相关业务， 才能使审计软件更好地发挥审计效果。这也有助于软件开发人员根据法规中 体现的业务需求设计出满足审计要求的审计软件，达到期望的审计效果。 自从1 9 7 7 年，伯努利( a p n u e l i ) 把时态逻辑引入计算机科学1 ，时态逻 辑在计算机方面的应用就已经开始了。从时态逻辑发展而来的其他逻辑也很 多，各种不同的时序逻辑如：t c t l ( t i m e dc o m p u t a t i o nt r e el o g i c ) ，m i t l ( m e t r i ci n t e r v a lt e m p o r a ll o g i c ) ，r t t l ( r e a l t i m et e m p o r a ll o g i c ) ，c t l ( c o m p u t a t i o nt r e el o g i c ) 和l t l ( l i n e a rt e m p o r a ll o g i c ) 口_ 妇等相继提出。 在国内，8 0 年代初把时态逻辑用于软件开发的整个过程，包括需求定义、规 约、设计、验证、代码生成和集成。在2 0 0 0 年以后基于线性时序逻辑的自动 机转换、化简和验证得到重视。 由于线性时序逻辑语言能够应用比较简单的规范语言来表示自动机的性 质，有效的避免不必要的回调来检测自动机的状态，是一种不同的理论应用 在表示自动机状态的迁移过程中，这是线性时序逻辑公式的优势所在，所以 线性时序逻辑适合用来描述已经构建完成的失业保险业务处理流程模型的时 序性质。 本文的课题主要来源于以下几个项目： 2 署工作。与以往不同的是这次部署工作从以往的基本养老保险扩展到五险： 基本养老保险、医疗保险、失业保险、工伤保险和生育保险。审计的领域逐 步扩大。 软件开发的过程和软件部署过程中一方面克服了并解决了诸多困难、问 题，另一方面也体现出一些不可回避的问题。下面以失业保险为例来说明在 部署过程中发现的问题。 ( 1 ) 软件开发过程中太多的业务关系存在于法规政策当中，处理好这些 关系是软件能否发挥最大效用的决定性因素，同时这也是失业保险业务掌握 情况的体现，所以明确失业保险的业务处理流程对审计效果和软件开发都是 比较重要的； ( 2 ) 确保生成审计方法的正确性，这也是失业保险业务的准确描述，这 也是尤为重要的； ( 3 ) 软件部署过程中，不同的审计人员对政策的理解不尽相同，这是自 然语言的一个弊端，如何明确的表述法规中的业务关系，使审计人员在业务 方面上最大程度的保持意见一致，这对审计工作后的疑点核实是大有裨益的； 基于以上的原因，本文提出应用线性时序逻辑这种形式化的语言表示失 哈尔滨工程大学硕士学位论文 业保险中的业务处理流程，形式化语言的无歧义性可以尽可能的减少不同人 对法规政策理解的偏差。针对失业保险的业务处理流程建模并应用模型检测 的手段来确保构建的失业保险业务处理流程模型是失业保险业务的真实反 映，构建的模型不但能够减少理解的歧义，同时还能够指导软件开发过程， 根据规则提出相应的审计方法，减少业务上的状态，从而精炼审计方法，削 减开发成本。 1 3 国内外研究现状 线性时序逻辑( l t l ，l i n e a rt e m p o r a ll o g i c ) 是在不明确引入时间的情 况下描述事件发生顺序，规约并发系统性质的优秀形式化工具n 到。 1 9 7 7 年，在文献 6 中，伯努利基于先前的模态逻辑和时序模态研究工。 作把线性时序逻辑引入计算机科学用于推理交互系统。把它作为开发并发式 系统和反应式系统时进行规格验证和说明的工具，在此阶段，线性线性时序 逻辑主要用于描述交互系统的行为和规格验证方面，还没有引入到其它更具 体的领域，比如，程序设计方面等，也没有应用，但是，说明了时序逻辑语 言能够应用在计算机科学领域，具有十分重要的意义。 在文献 1 3 中，c l a r k e 应用线性时序逻辑公式的性质表述构建模型的性 质来减少空间状态规模，达到提高性能的目的。在社保审计领域中处理失业 保险业务流程，应用该方法无非也是一个较好减少空间的方法。 1 9 8 3 年，在文献 1 4 中，唐稚松院士提出一个时序逻辑系统x y z e ， 这是一个具有常见语言风格且可用于实际编程运行的程序语言。它的统一框 架既能表示抽象规范，又能表示各种新的程序范型如：面向对象程序设计、 可视图形程序设计、多媒体、分布式程序设计等，而且还能表示自动机状态 更好的表示失业保险业务处理流程。 4 哈尔滨工程大学硕士学位论文 一i iw i i 文献 1 5 中作者将系统应用在复杂软件系统构架形式化当中，是线性时 序逻辑应用的再次扩展。 在文献 1 6 和文献 4 3 中李广元、a t l e e 利用时序逻辑描述实时系统及实 时系统的模型检测，根据时序逻辑模型的语义来削减软件开发成本，阐明软 件系统的真实内涵，同时在文献 1 8 ，1 9 中，他们利用时序逻辑帮助系统设计 人员和相关人员准确地了解系统、铁路系统的故障预测和m d g h d l 中，是 线性时序逻辑的具体应用，其应用范围之广，其理论同样也可以应用到社保 审计的失业保险业务处流程中。线性时序逻辑语言是一种形式化的语言3 ， 能够描述具有时序性质的模型。 在文献 2 1 和文献 2 2 中g i a n n a k o p o u l o u 和a n p i n gh e 的研究表明线性 时序逻辑与自动机的性质间可以相互表示，这就使得线性时序逻辑的适用范 围更加广泛。在失业保险审计中，参加失业保险人员的状态迁移可以应用线 性时序逻辑表示，因为参加失业保险的状态迁移是在线性时序上完成的，并 且线性时序逻辑中的线性时序模型可以用来表述基于自动机构建的失业保险 业务处理流程模型来构建，本文将线性时序逻辑理论应用在失业保险审计当 中。 1 4 本文研究内容与组织结构 1 4 1 论文研究内容 应用计算机对社会保险进行审计是现在审计的趋势，所以对业务人员来 说每个险种的业务流程也就更为重要。对于每一个险种来说，社会保障的业 务流程在审计工作开展之前必须弄清楚、明白。因为这是审计工作能否顺利 展开的关键。如果对被审计地区的业务流程掌握程度较深，那么审计的效果 也会比较好。以失业保险为例：参加失业保险的人员，在工作时间长短、失 业金享受的年限、在失业状态中领取就业金后失业保险金享受年限减少和下 一次的就业过程，是一个按照时间序列发生的一系列事件。本文运用线性时 序逻辑公式描述失业保险业务处理流程模型，并通过n u s m v 检测工具验证 哈尔滨工程大学硕士学位论文 模型中参保人员状态迁移的正确性。论文的主要内容包括以下几点： ( 1 ) 以失业保险的业务流程处理为例，根据h 地区的失业保险法规政策， 应用有限状态自动机理论描述失业人员的状态迁移情况，构建失业保险业务 处理流程模型。 ( 2 ) 针对基于有限状态自动机构建的失业保险业务处理流程模型进行状 态消减，化简失业保险业务处理流程模型，避免在检测过程中出现状态空间 爆炸的问题。 ( 3 ) 根据国家的失业法规政策，在特定的语言环境下生成关于国家失业 法规政策的线性时序逻辑公式的描述，这里的线性时序逻辑公式表示是模型 检测工具输入的一部分，如图1 1 中的p a r t 2 部分。 ( 4 ) 以构建完成的失业保险业务处理流程模型为基础，应用线性时序逻 辑公式描述失业保险业务处理流程模型中的时序性质，这里的线性时序逻辑 公式表示也是模型检测工具输入的一部分，如图1 1 中的p a r t l 部分。 ( 5 ) 运用n u s m v 模型检测工具完成对失业保险业务处理流程模型的检 测，并对结果做出分析。 本文的研究内容的相关联系说明如图1 1 所示。 地方的法规政策 蓠 1 流程； 圜 j p a r t 鬻纂劫l ：失业保险业务 i 处甏瓣质t n u s m - = 的l t l 语言描述 l r t 2 ：来源于国家政 策的l t l 语言描述 欧的法规政策h 基搿蒜瓣线 失业保险业务处理流程模 型的l t l 描述存在问题 业务流程存在问题 根据国家法规生成的l t l 语言存在问题 图1 1 研究内容的相关联系说明 1 4 2 论文组织结构 论文的具体安排如下： 6 剌 哈尔滨工程大学硕士学位论文 第1 章论述模型检测在社会保障审计中现实意义，根据课题的背景，提 出基于线性时序逻辑的模型检测。阐述本文的工作，应用线性时序逻辑表示 失业保险业务处理流程模型的时序性质，验证失业保险审计过程中的业务流 第3 章基于本文介绍的有限状态自动机和线性时序逻辑理论，建模失业 保险业务处理流程，化简失业保险业务处理流程，并运用线性时序逻辑公式 来表达模型的时序性质。最后运用模型检测工具n u s m v 进行模型检测。 第4 章针对失业保险业务处理流程模型的检测结果做出详细、具体、深 入的分析。如果模型检测的结果是一个迹，则表明被检测的模型存在一处或 者多处与约束条件不符合的状态迁移过程。 结论部分给出线性时序逻辑可以应用在失业保险中这个结论，可以应用 模型检测的方法达到验证业务模型的目的。 7 哈尔滨工程大学硕士学位论文 i i 宣i 宣i i i i i i i i 置i i i i i i i i i i i i i i i i i i i i i i 宣i i i i i i i i i i i i i i i i i 宣i i i i 萱i i i i i 萱萱i 置置 一 第2 章相关基础知识介绍 现阶段，模型检测的应用已经十分广泛，无论是在需求分析阶段还是在 软件测试方面都有所应用。常见的模型有状态机模型和时序逻辑模型，这两 种模型也是比较成熟的模型，本文中也涉及到相关的知识。下文将介绍线性 时序逻辑、有限状态自动机的相关知识以及本文应用的模型检测工具 n u s m v ，最后给出失业保险的相关知识。 2 1 线性时序逻辑的相关概念 定义2 1 线性时序逻辑语法1 ：给定原子命题集合彳尸，标准布尔连接符 和时态算子1 ( n o t ) 、x ( n e x t ) 、f ( f i n a l l y ) 、g ( g l o b a l l y ) 、r ( r e l e a s e ) 、 a ( a n d ) 、v ( o r ) 、u ( s 仃o n gu n t i l ) 和一( i m p l i c a t i o n ) 。线性时序逻辑的 语法可定义为： ( 1 ) 对于所有的原子命题，a p ，则f 是公式。 ( 2 ) 如果和y 是公式，那么1 ，x ，f 矽，g 矽，r 吵，痧 ，矽vy ， 妒u f ，专5 f ，也都是公式。 定义2 2 线性时序逻辑模型3 ：一个线性时序逻辑模型是一个三元组 胙( s ，r ，l a b e l ) ，定义为： s ：状态的集合： r ：s s 是一个后继函数； l a b e l ：s 专2 胛是映射，该映射给每个状态的原子命题集合赋值。 定义2 3 线性时序逻辑语义1 ，给定原子命题p a p ，线性时序逻辑模 型胙( s ，r ，l a b e l ) ，并且占s 和t 1 ，t 2 是线性时序逻辑公式。线性时序 逻辑公式的语义解释为 j l = p i f f p l a b l e ( s ) ； j l = t 1 v t 2 i f f s | _ t 1 v s i = t 2 ； s | - - - , t 1 i f f 1 ( j | - 丁1 ) ； 8 哈尔溟工程大学硕士学位论文 s j = x 丁l i f f r ( s ) t 1 ； ( 影o ) ，马i - t 1 ( v 0 k _ ，r j ( s ) l = t 1 ；r o ( s ) ，上u 乙+ l = b ( r ( j ) ) ) ，z 0 。 设m = ( 砖s o ；尺；上) 为k r i p k e 结构阻3 ，用乃表示路径万= s 0j l ，j 2 从 标号f 开始的后缀部分，即：死= s i8 f + l ，s m ，；以表示路径万= s os l ，s 2 ， 上的第一个状态，即状态s o 定义2 4 设m = ( 砖s d ；r ；三) 为k r i p k e 结构，万为m 中的( 从某个状 态开始的) 任一路径，、f 与以为线性时序逻辑时态公式，在m 的基础上 定义万i t 说明t 在路径y 上成立，万l t 说明f 在路径万不成立，其它情况如 下： ( 1 ) 疗l = t r u e ； ( 2 ) 万| f a l s e ； ( 3 )万l = p i f