没有合适的资源?快使用搜索试试~ 我知道了~
0HAL编号:tel-036220120https://theses.hal.science/tel-036220120提交日期:2022年3月28日0HAL是一个多学科开放获取档案,用于存储和传播科学研究文献,无论其是否发表。这些文献可以来自法国或国外的教育和研究机构,也可以来自公共或私人研究中心。0HAL多学科开放获取档案,旨在存储和传播法国或国外的教育和研究机构、公共或私人实验室发表或未发表的科学研究文献。0面向证明的领域特定语言设计用于高可靠性软件0Denis Merigoux0引用此版本:0Denis Merigoux. 面向证明的领域特定语言设计用于高可靠性软件. 编程语言 [cs.PL]. 巴黎科学与文学大学,2021. 英文. �NNT : 2021UP- SLE006�. �tel-03622012�0在巴黎高等师范学校和Inria(Prosecco)准备0面向证明的领域特定语言设计用于高可靠性软件0由Denis MERIGOUX支持02021年12月13日0巴黎数学科学中心第386号博士学院0计算机科学专业0评审委员会成员:0Karthikeyan B HARGAVAN Inria研究主任 导师0Évelyne C ONTEJEAN CNRS/巴黎-萨克莱大学研究主任 评委0Derek D REYER MPI-SWS教授 评委0Sarah L AWSKY Northwestern Pritzker法学院教授 评委0Xavier L EROY 法国学院/Inria教授 评委0Jonathan P ROTZENKO 微软研究院研究员 导师0Bas S PITTERS 阿尔胡斯大学副教授 评委10致谢0亲爱的冒险读者,当你翻阅这篇手稿时,愿你的勇气得到回报,这些文字将使你能够触摸到支持的无形网络,这个网络使得这个干燥而复杂的科学工作成为可能。如果我是唯一署名这篇论文的人,那是因为我的亲人、朋友和同事们给予了我无尽的帮助。正是因为他们,我才能保持动力和对研究员职业的不断追求,这个职业充满了无尽的怀疑和令人不安的问题。我也要把这篇论文献给他们;在这里,我无法逐个列举每个人的名字,所以我要衷心感谢那些在这些文字之外能够认同自己的人。首先,我要感谢一个出色的工作环境,让我能够适应并在非常舒适的条件下工作。首先要感谢欧洲研究理事会通过CIRCUS奖学金资助我的博士学位,以及Inria提供的博士合同,每周工作时间为38小时30分钟,为我提供了额外的报酬和休假。事实上,直到2021年,标准的博士合同每月的薪水是1769欧元,净收入约比最低工资高150欧元。虽然最近通过的研究规划法案预计到2025年将博士合同的薪水提高到2300欧元(注),但博士学位的薪水与博士生的资格水平以及生活成本相比太低,特别是在巴黎地区,这使得许多候选人无法负担得起这种情况多年。显然,博士合同的许多其他方面也需要改革,这些合同的分配条件也可以改善,特别是在人文学科领域。我希望与这些问题相关的斗争将继续下去:2009年建立的博士合同的社会成果表明,在这些问题上取得进展是可能的,特别是当我比较目前的情况时française au milieu anglo-saxon où les doctorants n’ont ni contrat de travail,ni congés, ni même permanence du salaire tout au long de l’année (césure lesmois d’été).Grâce à ce cadre confortable, j’ai pu dédier ces trois années de doctoratà ma recherche et à ses applications, ayant décidé de ne pas prendre demission d’enseignement. Ainsi les journées au deuxième étage du centre Inriade Paris (hors confinement COVID), jalonnées par les pauses thé et café, ontété l’occasion d’interminables et très productives discussions avec mes cherscollègues de laboratoire : Ben “l’ancien”, Marina, Natascha, Carmine, Thibaut,Blipp, Florian, Roberto, Kenji, Ram, Aaron pour la vieille génération ; Son,Théophile, Théo, Paul-Nicolas, Aymeric et Xavier pour la jeune générationqui monte malgré le silence des médias ; C˘at˘alin, Bruno, Vincent, Adrienpour les permanents qui assurent la continuité de Prosecco à travers lesâges. En dehors de Prosecco, je voudrais remercier François, Jacques-Henriet Pierre-Évariste dont les conseils plus ponctuels mais non moins précieuxm’ont été d’une grande aide. Enfin, last but not least, l’inimitable Mathieu qui,non content d’être le meilleur assistant de recherche du monde, a réussi àpasser de l’autre côté de la barrière pour commencer lui-même son doctorat.Évidemment, cette liste ne serait pas complète sans les mentions spécialesréservées à mes deux mentors intellectuels, véritables sherpas rompus auxpistes escarpées de la formalisation. Tout d’abord, celui qui m’a ouvert la portede la vérification appliquée à l’automne 2017 en me proposant de postulerchez Prosecco en tant qu’ingénieur de recherche, le distingué Principal CheeseResearcher Jonathan, auteur du best-seller XUL de la célèbre série “Lescahiers du programmeur” chez Eyrolles. Je remercie Jonathan qui, tel unVictor Hugo profitant de son exil contraint pour mieux exercer son génie,contribue au rayonnement de la France en dédiant une partie de son temps àla formation de jeunes et naïfs doctorants avec rigueur et humanité, patienceet confiance, sagacité et attention. J’espère que nous pourrons à nouveaugravir les montagnes du Pacifique nord-ouest ensemble, à défaut de l’Everest !Ensuite et logiquement, je suis infiniment reconnaissant d’avoir pu bénéficierde la direction stratégique et visionnaire de la star de la cryptographie vérifiéeet mécène de phalanstère artistique, l’unique et formidable Karthik. Toujoursprésent aux moments critiques, l’autonomie qu’il m’a confiée m’a surpriset honoré, témoignant de sa confiance et sa générosité ; j’espère que j’enaurais été à la hauteur durant ces trois années. Karthik, j’espère également terecroiser prochainement dans une galerie d’art du VIe arrondissement ou uneréception mondaine à Paris ou à Pondichéry, soit partout là où ton caractère2insaisissable te mènera. Enfin, je voudrais terminer sur un remerciement àDan Gohman, qui a été mon directeur de stage à Mozilla, et grâce auquelj’ai acquis le goût des compilateurs et la connaissance de WebAssembly,connaissance qui a été le déclencheur de mon recrutement à Prosecco.Poursuivant cette liste à la Prévert, il est temps de s’arrêter sur les personnesqui ont peuplé ma version de l’été 2019, à Seattle et au cœur du réacteur de larecherche en méthodes formelles de Microsoft, bizarrement plus fondamentaleque celle menée avec son partenaire public Inria ! Merci donc à Nik, Danel,Aseem, Chris, Tahina et Jonathan (encore une fois) de m’avoir fait vivreun concentré de science vivante et stimulante dans les locaux aux fenêtrestrop peu nombreuses mais à la cantine fort goûteuse du bâtiment 99. Lesdiscussions passionnées autour du tableau blanc rempli de contre-exemplesinvalidant notre modèle avorté de logique de séparation resteront à jamais pourmoi un exemple vibrant de science en gestation, bouillonnante et virevoltante.Mais ces journées éprouvantes, qui commençaient à 7 h 30 après 30 minutesde transport dans le bus privé de Microsoft à travers les autoroutes urbainesde Seattle, n’auraient pas été complètes sans les soirées en compagnie demon colocataire devenu cher ami Aymeric, et les autres jeunes recrues de l’étéSydney, Jay et Haobin, avec qui moult IPA houblonnées furent consommées.Mais au-delà du petit monde des méthodes formelles, j’ai pu étendre monhorizon des possibles grâce à d’extraordinaires rencontres, fortuites ou pro-voquées par mes recherches. Je veux ici commencer par remercier Sarah,respectable professeure de droit fiscal qui a su maintenir la flamme de saconviction scientifique malgré sa fulgurante carrière, et qui m’a accueilli avecrespect et attention lorsque je me suis présenté à elle, ignorant presque toutde son domaine d’expertise et prétendant apporter une solution au problèmequ’elle soulevait. Respect et attention également que je voudrais souligner etremercier chez Liane, dont j’ai passé avec succès les fourches caudines deson examen de probité pour informaticiens, et qui m’a ouvert les portes d’unmonde juridique étranger, mais pourtant rapproché de l’informatique par unevéritable invasion technoptimiste, qu’il serait maintenant temps de tempérerpour y distinguer le bon grain de l’ivraie. Merci donc à Liane et ses brillantesétudiantes comme Lilya de m’avoir aidé à vérifier mon implémentation ducalcul allocations familiales au cours de séances de pair programming quinous ont laissé perplexe quant à la qualité du législateur français. Merciégalement à Marie qui a bien voulu nous guider Liane et moi dans la jungle dela transformation numérique de l’administration, nous faisant profiter de sonexpérience durement acquise et de sa tolérance au positivisme scientifique340对于一个如她一样敏锐和清醒的社会学家来说,这是一个非凡的经历。从理论到应用,这次奇妙的冒险涉及到了我们所说的有时过于行政的行政机构,我有幸与之接触的代表们推翻了我许多的偏见。因此,感谢那些M代码的可怜人,他们像阿特拉斯一样承担着支撑国家良好运转的重任,他们表现出了令人印象深刻的冷静。感谢那些在公共部门支持我疯狂的技术转移计划的人,感谢DGFiP金字塔各个层级的人:James,Laurent,Christophe,Violaine,Lisa,Éric,Tomasz,Audran和其他许多人。还要感谢那些精力充沛的退休人员,比如Dominique,他对过去的了解为未来提供了启示,以及自由软件、开放科学和算法监管的先驱们:Bastien,Soizic和Simon。显然,如果没有Raphaël的决定性和坚定不移的支持,这一切都不可能实现,他愿意放下他作为武术大师的角色与我一起写OCaml。还要感谢Inria及其科学总代表,特别是Alain和Jean-Christophe,他们相信我的项目,并允许我在论文答辩后继续推动它。面对如此多的支持和教授们对我的培养,我自己努力地为人类知识的传承做出了贡献,将我的努力集中在个人传授而不是集体传授上。因此,我感谢Nicolas和Alain选择我作为实习导师,并希望他们不会对我太苛刻,因为他们是我在这个领域的第一批实验对象。当然,在工作之外,还有许多朋友们以善意支持我关于税收计算的无尽轶事。当然还有phlysle的朋友们:Clara,Antoine(×3),Maxime,Gautier,Jules,Grégoire,Gaëtan,José,Dhruv。还有萨克莱高原上的其他不幸者们:Goeffrey,Matthieu,Nilo,Thomas,Marc,Basile,Camille,Pierre-Cyril,Robin,Bénédicte和其他许多人。还有不屈不挠的击剑者和周四晚餐的老朋友们:Raphaël,Marion,Adrien,Flora,Arthur,Philippine,Quentin,Vincent,Charles,Mathilde,Alexandre,Romain,Jean-Pierre,Jean-Baptiste,Lara,Marguerite,Nina,Soizic,Thibaut(×2)和Théo。最后,我想以我最亲近、最重要的支持者们结束:我的父母André和Sylvie,我亲爱的姐姐Celia,我的祖父母Michel和Chantal,他们毫无保留地、充满爱意地陪伴着我完成了这个论文,尽管他们有时很难理解其中的来龙去脉。最后,我想把这本手稿献给50那个我与之开始关系的奇妙博士阶段,她在论文的所有考验中每天陪伴着我,她是我在许多快乐或困难的时刻的灵感和安慰:我亲爱的Yoko。02021年11月23日,巴黎70出版物列表0J. Protzenko, B. Beurdouche, D. Merigoux, and K.Bhargavan,“在WebAssembly中形式化验证的密码网络应用程序”,2019年IEEE安全与隐私研讨会(SP),2019年,第1256-1274页。DOI:10.1109/SP.2019.00064。0N. Swamy, A. Rastogi, A. Fromherz, D. Merigoux, D. Ahman, and G.Martinez,“Steelcore:一种可扩展的并发分离逻辑,用于有副作用的依赖类型程序”,ACM程序语言进展,第4卷,第ICFP期,2020年8月。0DOI:10.1145/3409003。[在线].可用:https://doi.org/10.1145/3409003。0A. Fromherz, A. Rastogi, N. Swamy, S. Gibson, G. Martinez, D. Merigoux, and T.Ramananandro,“Steel:面向证明的并发分离逻辑中的编程”,ACM程序语言进展,第5卷,第ICFP期,2021年8月。DOI:10.1145/3473590。[在线].可用:https://doi.org/10.1145/3473590。0D. Merigoux, F. Kiefer, and K. Bhargavan,“Hacspec:简洁、可执行、可验证的高保证密码学规范嵌入Rust”,Inria,技术报告,2021年3月。[在线].可用:https://hal.inria.fr/hal-03176482。0D. Merigoux, R. Monat, and J. Protzenko,“法国税法的现代编译器”,第30届ACMSIGPLAN国际编译器构造会议论文集,CC2021,虚拟,韩国共和国:计算机协会,2021年,第71-82页,ISBN: 9781450383257。0DOI:10.1145/3446804.3446850。[在线].可用:https://doi.org/10.1145/3446804.3446850。0D. Merigoux, N. Chataing, and J. Protzenko,“Catala: 一种法律编程语言”,ACMProgram. Lang.会议论文集,第5卷,第ICFP期,2021年8月。DOI:10.1145/3473582。[在线].可用:https://doi.org/10.1145/3473582。90摘要01. 用灵活的语言连接程序和证明110I. 高保证密码软件5302. LibSignal�: 将验证的密码学移植到Web上5503. hacspec: 高保证密码规范10304. Steel: 分而治之的证明义务1550II. 高保证法律专家系统20105. M LANG: 法国税法的现代编译器20306. Catala: 一种法律规范语言2410结语2911101. 用灵活的语言连接程序和证明0目录01.1. 通用框架的兴衰...1301.1.1. 程序验证背景...1301.1.2. Coq、Fiat及其后续...1901.2. 用于程序验证的领域特定语言...2201.2.1. 规范问题...2201.2.2. 领域特定解决方案...2701.3. 推动验证技术前沿的新方法...3101.3.1. 划分子集并连接证明...3101.3.2. 面向证明的领域特定语言...370本论文的贡献...400摘要0没有像巴别塔那样的神话般的起源故事来解释编程语言和形式化方法工具的多样性:相反,不同的范式和框架用于解决不同的问题对计算机科学家来说是直观的[1]。另一方面,为了效率和避免重复,产生了形式化方法的共同基础设施的紧张关系。在本章中,我们认为推进验证技术的发展意味着创建多样化的工具和领域特定语言。这引发了两个问题:首先,确保在框架之间共享努力;其次,确保各种领域特定语言对其目标受众即领域专家仍然具有相关性。0简单、贫乏、透明的工具是一个谦卑的仆人;复杂、秘密的工具是一个傲慢的主人。0(伊凡∙伊利奇,《共融性》,1973年)0一盎司实践通常比一吨理论更有价值。0(恩斯特∙弗里德里希∙舒马赫,《小即是美》,1973年)This work, although centered around programming language design, is deeplyconnected to formal methods and one of its active research areas: programverification. The goal of program verification is to prove some properties aboutthe source code of a program, the result it returns upon execution and theeventual side-effects it can have.The properties that one can prove about a program are diverse. Someare common to all programs : whether the computation terminates or not,whether the program accesses the memory in a well-behaved fashion (memorysafety), etc. Some are very specific and relate to what a program is trying todo: in that case, the property that we are trying to prove about the program isakin to a specification of the program, expressed in a more concise or abstractway than the program itself.For instance, one might want to prove that the source code of a program Pimplementing a map data structure as an optimized red-black tree does indeedbehave like an abstract map. This property can be expressed by attachingto the state of P a ghost abstract map M, with an invariant I stating that avalue is stored in P if and only if it is stored in M. Then, the property holds ifwe can prove that the invariant I is preserved by all the operations in P.In this chapter, as well as the rest of the dissertation, we will focus onapplications of program verification to real-world examples: programs thatrun in production inside some device or organization and provide services.1301.1. 通用框架的兴衰01.1. 通用框架的兴衰0本节概述了程序验证社区中不同的技术方法以及它们在工具基础设施方面的影响。特别是,我们指出了通用证明助手Coq在程序验证社区中的日益普遍存在:虽然它被认为是成功的,并且在其领域中通常是不可避免的,但我们认为它的持续改进将不足以显著推动技术发展。事实上,可以认为Coq现在已经达到了其早期技术设计决策所限制的界限。因此,对专门的工具的需求正在增加,以及连接这些不同工具的技术。01.1.1.程序验证的背景1401.用灵活的语言将程序连接到证明0当然,这种关注是非常狭窄的,不能代表程序验证研究的多样性和复杂性。这个编辑选择是由我们对该领域中更应用研究的一般倾向所引导的。0一个分裂的联邦国家我们选择的程序验证定义是故意宽泛的,以包括属于它的各种技术。事实上,将属性和程序编码到能够执行证明的逻辑系统中的方法非常多样。我们将在这里列出在这方面的主要思想流派。请注意,在本小节和论文的其余部分中,我们不考虑针对物理系统的模型检查(例如UPPAAL[2]),因为我们考虑的是程序实现验证,而不是规范模型检查。符号执行。符号执行[3]是最早的程序验证形式。正如最近的一项调查[4]所提醒我们的那样,符号执行的原则是用符号替换具体的程序输入,并通过跟踪程序的执行来传播这些符号。当遇到条件时,通常必须同时考虑与真条件或假条件相对应的两条可能的执行路径。然后,程序的结果可以表示为依赖于输入符号的逻辑表达式。然而,由于程序中的每个分支都导致需要考虑的新路径,路径的数量随着程序的大小迅速增加:这就是“路径爆炸”。符号执行面临的另一个具有挑战性的问题是无界循环,这需要推断一个循环不变量。一些工具通过将所有循环展开到固定次数的迭代中来解决这个问题,这是有界模型检查的一个示例。符号执行的主要实际应用是模糊测试:使用随机源探索输入空间,为程序的边界情况制作相关的测试。像Klee[5](建立在LLVM之上)和SAGE[6]这样的工具与模糊测试器一起用于发现各种低级、系统软件的边界情况。这个研究方向今天仍然活跃[7]。抽象解释。为了自动推断无界循环的循环不变量,抽象解释提供了一种解决方案[8],[9]。这种技术基于一个坚实的理论框架,可以适应几乎任何编程语言的语义,可以简洁地描述为将输入空间划分为域,并映射这些域在程序执行过程中的演变。通过证明循环迭代不会改变变量的域,可以得出循环不变量。1501.1.通用框架的兴衰0可以推断出。抽象解释已成功应用于实际的航空航天软件[10],其中著名的Astrée[11]分析器。抽象解释的缺点正是其优点:输入域(以及相应的抽象函数)的选择可能会变得繁琐。域太大可能会使分析不准确,而使域过于具体可能会导致证明困难,并导致分析资源消耗的爆炸。问题在于,域的选择是用户与证明器进行交互的唯一方式。这种交互瓶颈使得在整个过程全局自动化时难以推理局部困难的证明部分。霍尔逻辑和最弱前置条件。程序验证的前两个领域都侧重于基于源程序和初始用户提供的工具配置的自动程序分析和证明。然而,开发人员也可以通过为程序的每个函数注释前置条件和后置条件来更细致地指导证明。这些条件实际上为函数定义了一个合同。合同本身由函数体上的证明支持:该证明的结论是,在假设前置条件的情况下,后置条件在函数结果上成立。另一方面,每个调用者必须检查前置条件是否成立,如果成立,则可以在函数调用后假设后置条件。这种程序验证风格对应于霍尔逻辑[12],它允许增加证明的模块化。霍尔逻辑是嵌入在许多交互式证明助手(如Coq[13]或Isabelle/HOL[14])中的程序验证框架的基础。基于霍尔逻辑的交互式证明的精确性和灵活性使得可以对像seL4内核[15]这样的实际关键软件进行程序验证。此外,通过最弱前置条件变换器[16],可以为该方法提供一些自动化,该变换器将子合同组合在一起,生成一个单一的属性,如果有效,则实现了证明。生成的最弱前置条件属性可以编码在自动求解器(SAT或SMT)中,并进行自动检查。交互式证明和自动化之间的这种结合是Why3 [17]或F�[18]等程序验证框架的核心。最后,一些证明器在设计其证明义务时选择了大多数自动化的方法,这些证明义务围绕着霍尔逻辑和与内存相关的分离逻辑,如Viper [19]和Verifast[20]。总的来说,上述技术已经将程序验证转变为一种可靠的技术,可以用于提高现实世界软件的保证水平。但是,我们必须更加准确地说明当前状态是什么。1601.使用灵活语言将程序连接到证明0属性复杂性0程序规模0最前沿的技术0图1.1:插图:程序验证的前沿在哪里?0现有技术可以实现的最高水平。为此,请考虑图1.1的说明。我们选择在众多可能的轴线中,将状态投射到两个轴上,即程序规模和属性复杂性。这些轴与我们关注程序验证的实际应用相匹配。该图的要点如下:我们很清楚如何在小程序上证明复杂属性,或者在大程序上证明弱属性。让我们通过几个例子来证明这些说法。在下面的讨论中,我们故意忽略了技术的基础方面以及所有步骤和抽象的认证问题。如前所述,我们更关心这些技术如何提高现实世界软件的保证水平。为了达到这个目标,我们愿意采取务实的认证要求,并考虑整个信任链。因此,信任链的强度取决于其最薄弱的环节。最薄弱的环节可能在于缺乏编译步骤的认证,但通常并非如此,我们将在1.2.1节中进行论证。0通过错误消息进行程序验证的技术转移到工业界和现实软件的历史始于静态分析作为其入口点[21]。在这种设置中,普遍的逻辑是:运行关键软件的大型组织希望改善其庞大的遗留代码库的安全性。这个组织的工程师没有任何形式方法的技能,但幸运的是,他们中的一些人熟悉类型化语言,并习惯于编译器错误反馈循环。根据Astrée的这个有洞察力的用户故事的详细说明[22],成功的转移关键在于用更复杂的静态分析和程序验证形式的警告消息劫持传统的编译器错误消息的形式。由于经过良好训练的工程团队习惯于使用-Wall标志维护代码库,并追踪所有警告,提供更精确和微妙的警告和可能的错误指示将改善代码库。这种木马方法还有其他几个工业级的支持者,例如法国原子能委员会(CEA)的Frama-C[23],[24]或Facebook的Infer[25]。虽然这种方法使得填补了图1.1右下象限,但它有几个限制其范围的缺点。首先,它的有用性在很大程度上取决于底层静态分析方法的误报率和漏报率。当然,太多的漏报意味着该工具在检测错误方面不起作用。但是太多的误报可能会引发用户流失:当程序员感觉到该工具没有提供准确的信息时,她将停止信任它,并不再关心警告。其次,分析工具只能推理裸源代码,通常无法访问支撑程序行为的各种不变量和逻辑条件。虽然一些工具提供了一种注释语言,让用户以正式的方式编写注释,但在遗留代码库中进行这样的注释是一个令人生畏的任务,超出了普通软件工程师的能力和培训范围。因此,对大型遗留代码库进行静态分析的工具由于缺乏源代码本身的正式全局和局部上下文,以及对证明的困难部分的手动指导,而无法证明关于程序的复杂属性。setting is the following: a large organization running critical software wantsto improve the safety of its large, legacy codebase. The engineers of thisorganization do not possess any formal methods skills, but luckily some ofthem are familiar with typed languages and are used to the compiler errorfeedback loop. The key to successful transfer, as detailed by this insightfuluser story on Astrée [22], is to highjack the traditional formal of compilererror messages with warning messages powered by more complex formsof static analysis and program verification. As a well trained engineeringteam is used to maintain a codebase with the -Wall flag enab
下载后可阅读完整内容,剩余1页未读,立即下载
![docx](https://img-home.csdnimg.cn/images/20210720083331.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- BSC关键绩效财务与客户指标详解
- 绘制企业战略地图:从财务到客户价值的六步法
- BSC关键绩效指标详解:财务与运营效率评估
- 手持移动数据终端:常见问题与WIFI设置指南
- 平衡计分卡(BSC):绩效管理与战略实施工具
- ESP8266智能家居控制系统设计与实现
- ESP8266在智能家居中的应用——网络家电控制系统
- BSC:平衡计分卡在绩效管理与信息技术中的应用
- 手持移动数据终端:常见问题与解决办法
- BSC模板:四大领域关键绩效指标详解(财务、客户、运营与成长)
- BSC:从绩效考核到计算机网络的关键概念
- BSC模板:四大维度关键绩效指标详解与预算达成分析
- 平衡计分卡(BSC):绩效考核与战略实施工具
- K-means聚类算法详解及其优缺点
- 平衡计分卡(BSC):从绩效考核到战略实施
- BSC:平衡计分卡与计算机网络中的应用
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)