没有合适的资源?快使用搜索试试~ 我知道了~
C1中单位静态校验的重写逻辑方法
可在www.sciencedirect.com在线获取理论计算机科学电子笔记290(2012)51-67www.elsevier.com/locate/entcsC1中度量单位静态校验的重写逻辑方法MarkHills2FengChen3GrigoreRoRangsu4伊利诺伊大学厄巴纳-香槟分校计算机科学系摘要许多C程序假定使用隐式的特定于域的信息。一个常见的例子是测量单位,其中的值可以有标准的C类型和相关的单位。 但由于在C语言中没有办法表示这些额外的信息,因此很难检测到对特定于域的策略的违反,例如单元安全违反。 在本文中,我们提出了一个静态分析,基于使用重写逻辑定义的抽象C语义,用于检测C程序中的单元违规。 与类型化方法相反,分析使用C注释中的注释在函数头和函数体中,保持C语言不变。 初步评估结果表明,性能扩展良好,可以检测到错误,而不会造成沉重的注释负担。关键词:单元安全,重写逻辑,抽象语义,静态分析。1介绍许多程序使用特定于域的信息。一个常见的例子,经常发生在科学和工程应用中,是使用测量单位单位与特定的值或变量相关联;单位规则确定语言中的操作(加法,乘法等)如何改变和组合单位,并确定何时安全。在包括C在内的许多语言中,关于单位的信息是隐式的:程序员假设值具有特定的单位,而不是具有程序级表示,这些单位可以非正式地记录在源代码注释中。不幸的是,该信息的隐含性质意味着它不能用于自动确保1由NSF CCF-0448501和NSF CNS-0509321支持。2电子邮件地址:mhills@cs.uiuc.edu3电子邮件:fengchen@cs.uiuc.edu4电子邮件:grosu@cs.uiuc.edu1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2012.11.01152M. Hills等人理论计算机科学电子笔记290(2012)511 typedef结构{2双原子量;3双原子数;4 }元素;56//@前(单位):unit(material->atomicWeight)= kg7 //@ pre(UNITS):unit(material->atomicNumber)= noUnit8//@ post(单位):单位(@结果)= m^2 kg ^-19 double radiationLength(Element * material){10双一 = material->atomicWeight;11双Z= material->atomicNumber;12双L =log(184.15/pow(Z, 1.0/3.0));13双Lp =log(1194.0/pow(Z, 2.0/3.0));14返回(4.0*alpha *re*re)*( NA/ A) *15(Z * Z * L + Z * Lp);16}1718//@前(单位):unit(material->atomicWeight)= kg19 //@ pre(UNITS):unit(material->atomicNumber)= noUnit20//@ pre(单位):单位(密度)= kg m^-321 //@ pre(UNITS):单位(厚度)=m22 //@ pre(UNITS):unit(initEnergy)=kg m^2 s ^-223 double finalEnergy(Element * material,double density,24double thick,double initEnergy){25双X0intmaximum();26return initEnergy/exp(thick/X0);27}Fig. 1. 电子能量示例,以C为单元操作是安全的,即,运算符总是应用于具有兼容单位的操作数确保这一点的负担直接落在程序员身上。这使得严重的特定于域的错误可能无法被检测到。严重错误的可能性不仅仅是理论上的。1999年9月30日,美国宇航局大约在此之前的15年,发现号航天飞机在午夜时分坠毁,试图将一面镜子对准 海拔10,023英尺;软件将此数字解释为10,023海里,或大约60,900,905英尺[27]。手动检查可能是小程序的一种选择,但不能扩展到大型程序。即使在小程序中,某些计算也可能非常复杂,并且可能依赖于非局部信息,例如全局变量的内容和函数调用的结果,这使得手动检查具有挑战性。例如,M. Hills等人理论计算机科学电子笔记290(2012)5153用于计算电子5的最终能量的程序的一部分在图1中示出。如果没有一个方法来记录预期的单元并检查正确性,那么代码是否是单元安全的就不明显了。事实上,第26行将报告一个单位错误:radiationLength计算返回的单位是米2千克-1,而thick的单位是米,所以thick除以X 0的单位是米-1千克。但是,exp需要一个无单位参数,这意味着注释不正确或radiationLength未正确使用。已经提出了许多方法来加强程序中的单元安全性,其中一些在第2节中讨论。在本文中,我们提出了一个新的解决方案,C语言,CPF[UNITS]。CPF[UNITS]基于CPF 框 架 [16] , 是 概 念 验 证 C-UNITS 系 统 [29] 中 引 入 的 思 想 的 重 要 扩 展 。CPF[UNITS]允许将单元特定的注释以函数前置条件、函数后置条件、断言和假设的形式添加到C程序中。然后,使用C的抽象重写逻辑语义(CPF的一部分)和UNITS策略(某些语言特征的单元特定语义的集合)的组合以及注释语言和注释语义的组合来检查这些注释的有效性。因此命名为CPF[UNITS],表示由UNITS策略参数化的CPF本文的其余部分组织如下。我们首先在第2节介绍相关的工作,包括早期的C-UNITS系统和基于类型的方法。然后,我们在第3节中介绍了C语言的抽象重写逻辑语义,假设熟悉术语重写和基本熟悉等式或重写逻辑。第4节介绍了测量单位,第5节介绍了CPF[UNITS]单位安全检查器的详细信息。第6节介绍了初步评估结果,第7节介绍了未来可能的我们的网站提供本文中描述的所有工具和示例的下载,以及基于Web的实验界面[1]。2相关工作单元安全性的相关工作往往分为三类:基于库的解决方案,其中操作单元的库被添加到语言中;语言和类型系统扩展,其中添加新的语言语法或类型规则以支持类型检查上下文中的单元检查;以及基于注释的解决方案,其中用户提供的注释有助于单元检查。基于库的解决方案已经为几种语言提出,包括Ada [15,23],Ei el [19]和C++[7]。NASA喷气推进实验室的任务数据系统团队这种显式方法的一个明显缺点是库支持的单元是固定的:添加新单元需要用新类扩展库,并可能添加或修改[5]这个例子是从Jiang和Su关于Osprey的工作中借用的54M. Hills等人理论计算机科学电子笔记290(2012)51现有的方法,以确保新的类得到适当的支持。基于语言和类型系统扩展的解决方案通过将单元引入类型系统并潜在地引入语言语法来工作,允许编译器或解释器使用扩展的类型检查算法来检查表达式的单元正确性。MetaGen [5]是Java的MixGen [4]扩展的一个扩展,它提供了允许为面向对象程序指定尺寸和单元信息的语言特性其他使用语言和类型系统扩展的方法针对ML[21,20],Pascal [13,17]和Ada [14]。一个较新的工具,Osprey [18],也使用类型化的方法来检查单元安全性,允许使用修改版本的CQUAL [12]在C程序中使用类型注释(例如$meterint)。然后,可以使用多个工具的组合来检查这些注释,这些工具包括注释处理器、约束求解器、联合/查找引擎和高斯消除引擎(后两个用于减少不同约束的数量,并正确处理作为矩阵的单位类型的鱼鹰表示)。Osprey的一个限制是无法表达函数参数和返回值的单位之间的关系,这可以通过更丰富的注释语言来实现//@ post(UNITS):unit(@result)^2 =unit(x)double sqrt(double x){. }相反,这种类型的关系必须通过手工编辑处理过程中生成的文件来添加鱼鹰还检查尺寸(即,长度),而不是单位(即,米或英尺),而不是将单个维度中的所有单位转换为规范单位。这可以掩盖潜在的错误:例如,将声明为单位米的变量传递给期望英尺的函数不是错误。另一方面,Osprey包括检查显式转换正确性的功能,捕获常见的转换错误,例如使用错误的转换因子。基于注释的系统,包括JML [8]和Spec# [6],已经应用于许多问题领域,但并不专门用于单元。基于注释的单元安全系统包括C-UNITS系统[29],它使用了关于抽象语义和注释的概念,这些概念首先出现在BC(一种小型计算器语言)的上下文中[9]。CPF[UNITS]受到C-UNITS工作的启发,并采取了类似的方法,重点是使用抽象语义和注释。然而,CPF[UNITS]在三个重要方面扩展了这一方法。首先,CPF[UNITS]被设计成模块化的:C的抽象语义已经使用过去几年开发的概念完全重新定义,作为重写逻辑语义项目的一部分[25]。语义分为核心模块,由所有CPF策略共享,以及单元模块,专用于CPF[UNITS]。这允许所有策略共享核心模块中的改进,简化了单元检查逻辑,并大大提高了理解和修改语义的容易性第二,CPF[UNITS]旨在覆盖C的更大部分。C-UNITS被设计成一个原型,并遗漏了一些重要的C功能,对结构,指针,强制转换,switch/case语句,goto或递归函数调用的支持很少或根本没有。支持M. Hills等人理论计算机科学电子笔记290(2012)5155k(lookup(X)<$env<$[X,L,U]<$lvp(L,U)图二. 示例C语义规则,以K表示eq k(lookup(X)-> K)env(Env [X,L,u(U)])= k(val(lvp(L,u(U)-> K)env(Env [X,L,u(U)])。图三. 示例C语义规则,Maude表达式也是有限的,主要集中在常用的表达式,更复杂的内存场景(指针结构,指针数组等)被忽略。CPF[UNITS]支持所有这些特性,并使用更高级的解析器来处理更大类的C程序。最后,CPF[UNITS]的设计更具可扩展性。虽然C-UNITS需要完整的分析程序,但CPF[UNITS]分析单个功能,从而导致较小的单个验证任务。CPF[UNITS]使用的技术,像大多数(如果不是全部)静态分析一样,可以根据抽象解释[11]来构建,其中解释的域是测量单位的代数然而,CPF[UNITS]大量使用了最近开发的重写逻辑语言定义技术,这些技术基于抽象语法树作为延续的表示;建立重写逻辑语义和抽象解释之间的关系本身就是一个有趣的主题,但它超出了我们在本文中的目的3C语言逻辑语义的抽象重写C的抽象语义是使用Maude [10]定义的,Maude是一种用于重写逻辑的高性能语言和引擎。当前程序被表示为嵌套项的“汤”(多集),这些嵌套项表示当前计算、环境(将名称映射到抽象值和其他信息)、分析结果、簿记信息和特定于分析的信息。最重要的信息是名为k的计算,它是当前计算的一阶表示,由一系列以->分隔的指令组成。计算可以被看作是一个堆栈,当前指令位于左侧右边是计算的剩余部分。这种方法在有关重写逻辑语义学项目的论文中有更详细的描述[24,25]。为了简化CPF语义中规则的表示,我们使用K表示法[28],其中包括许多简化约定。图2和图3显示了CPF[UNITS]工具(见第5节)中使用的抽象C语义中包含的语义规则的示例,首先是K表示法,然后是Maude。该规则表示内存查找操作。在这里,如果正在查找标识符X,并且环境包含一个名为X的项目,其位置为L,单位值为U,则将就地返回一个包含L和U的位置值对lvp(L,U56M. Hills等人理论计算机科学电子笔记290(2012)51op _^_:单位率->单位。op:Unit Unit-> Unit [asynchronous]。等式U ^ 0 =noUnit。等式U ^1= U。等式U U = U ^ 2。eqU(U^Q)=U^(Q+1)。eq(U^Q)(U^P)=U^(Q+P)。eq(UU')^ Q =(U ^ Q)(U ' ^ Q)。eq(U^Q)^P=U^(Q*P)。ops noUnit anyfailcons:-> Unit. 操作米m英尺f:->单位。图四、测量单位,Maude的查找操作,而环境保持不变6.K版本使用了三种K约定:>用于代替)来表示“和其他所有内容”,在Maude版本中扩展为-> K; >用于集合匹配(“其他所有内容到任意一侧”),这需要Env来表示Maude中的“其他所有内容”;替换通过在术语的已更改部分下划线来Unit。op u:Unit ->Value。op ptr:Location ->Value。位置->价值。op struct:Identifier SFieldSet ->Value。opunion:Identifier SFieldSet ->Value。见图7。 CPF[UNITS]值,Maude5.3.2CPF[UNITS]:抽象值CPF[UNITS]值是单位值和表示C指针、结构、联合、数组和枚举(被视为常量)的值的组合。单位值是在图4所示的单位理论中定义的,用包含简单C表达式的C特定单位值进行扩充,例如指数中的常数整数。指针表示为位置;解引用访问该位置的实际值,例如单元、结构或另一个指针(用于多级间接)。数组也有类似的表示形式,这允许它们像指针一样使用,但限制它们只包含一个值,所以所有的数组元素被认为具有相同的单位。结构和联合包含结构或联合类型的名称(匿名结构和联合由CIL命名)和一组字段/位置对,以指示每个字段的值存储在哪里。函数指针用一个特殊的值表示,别名分析用于确定通过指针的间接调用调用哪个函数;如果无法在调用站点确定唯一的函数,则会发出警告。CPF[UNITS]策略使用的值定义的子集如图7所示。5.3.3CPF[UNITS]:C声明处理声明的CPF[UNITS]规则为函数的全局变量、形式参数和局部变量提供了内存不同的分配器用于每个C对象类型,分配适合对象的初始值。例如,标量的分配器最初将该声明唯一的“新鲜”单元与标量相关联,而指针的分配器将引用与新的内存位置相关联。结构和联合变量的声明基于结构或联合声明中包含的字段分配分配是递归的;结构分配也分配结构的字段,而数组和指针的分配也分配数组或指针的基类型,联合当前表示为类似结构(即,我们不试图只分配一个由联盟中的所有字段共享的位置)。一个具有挑战性但常见的情况是,结构包含指向其他结构的指针。不可能预先分配整个内存表示,因为这可能是(理论上,[9]这使得我们的分析具有路径敏感性,尽管我们并不试图追踪哪些条件导致了哪条路径。M. Hills等人理论计算机科学电子笔记290(2012)5161至少,在有限的。结构内的指针是用分配触发器创建的,它将在第一次尝试访问指针时分配指针在处理完函数体/验证任务中的所有声明之后(CIL将所有声明移动到函数的顶部,使用重命名到模型阴影),使用断言(来自注释)和赋值的组合将初始值赋予局部变量。例如,断言可以指示变量x具有单位meter;然后,像inty =x;这样的声明将meter与Y也是。形式参数和全局变量的初始单位仅基于函数的前提条件。如果一个前提条件或赋值没有指明变量的初始单位,它会保留其赋值的新(唯一)单位,这将允许检测表达式中滥用变量的错误。在所有初始分配完成后,锁定过程锁定某些内存位置,以确保它们不能以注释中未反映的方式进行更改。例如,不可能通过作为形参给出的指针写入新单元。这确保了在函数外部可见但不包括在前置条件和后置条件中的更改被阻止,允许检查是真正的模块化的。最后,采取“检查点”,在函数体中进行任何更改之前保存原始赋值。这使得这些原始值可以在以后的单元检查中访问,比如在检查为表示函数后置条件而添加的断言时。5.3.4CPF[UNITS]:C表达式为了计算CPF[UNITS]中的表达式,语义规则需要正确地修改,组合和传播表示单元和C对象(指针,结构等)的抽象值。表达式以及断言语句也是发现单元安全违规的点,因此可能产生故障的表达式的语义图8包括一组代表性表达式的规则,说明了如何传播抽象值和检测故障。第一个规则模拟乘法运算。这里,给定两个单位值U和U 第二条加法规则的结构与第一条相似,但也必须检查单位的组合是否正确。这是通过使用mergeUnits合并单元来完成的。在合并中,如果一个单位是any或cons,这两个单位都可以被视为任何单位,则返回另一个单位否则,这两个单位必须匹配,而不执行单位之间的自动转换。 如果单元不匹配,或者其中一个单元失败,则返回fail以指示单元安全违规。 这将强制执行加法的单位规则-两个操作数的单位必须相同。要检测故障并发出警告,使用checkForFail,如果结果单元失败,将打印错误消息。10可以使用注释来覆盖这种锁定行为,但这将生成一条警告消息,提醒用户这样做可能会造成不合理。我们正在努力将别名分析结果纳入锁定过程,以缓解这一限制。62M. Hills等人理论计算机科学电子笔记290(2012)51[1]U*U' = U U'[2]U+ U[3]U> U[4](lvp(L,V)=[5](lvp(L,U)+=[6]* (lvp(L,ptr(L ')= llookup([7]lvp(L,struct(X ',(sfield(X,L')_). X= llookup(见图8。 CPF[UNITS]表达式规则,K第三条规则处理优先于关系操作。这里的规则与加法相同:要比较两个值,它们必须具有相同的单位。除此之外,返回的单位是noUnit,因为将单位分配给比较结果没有意义。第四条规则用于赋值。在这里,左值的计算结果是一个lvp,或者位置-值对,对象的位置和当前值被赋给它。右侧表达式的值将在当前值上赋给同一位置。虽然这适用于单元,但它也适用于其他C实体,例如指针和结构的表示。对于+=操作数,数字规则是+和赋值规则的组合,既执行失败检查,又执行对左值位置的赋值。在这种情况下,值应该是单位,因为有必要比较它们来验证操作是否安全;指针算术需要不同的规则。在第四条和第五条规则中,括号被添加以清楚地区分K=和C赋值=。最后,第六条和第七条规则展示了指针和结构的某些方面都处理好了指针被表示为位置-指向位置L的指针具有值ptr(L)。在取消引用时,查找指针中保存的位置以检索其值。一个结构被表示为一个包含结构类型名称的元组和前面提到的从字段名称到位置的有限映射;有限映射中不需要的部分被表示为。当在结构中查找字段X时,如S.X,使用映射检索X的位置,然后查找以带回分配给字段的值5.3.5CPF[UNITS]:注释语言、断言和假设单元注释语言如图9所示。Unit包括一个运算unit,用于检查表达式的单位;单位指数,其中Q可以是有理数;基本单位,如米或千克;以及单位乘积,用于指定新单位。UnitExp包括单元、单元相等性测试和一些逻辑M. Hills等人理论计算机科学电子笔记290(2012)5163单位U::=单位(E)|单位(E) Q|步|U UUnitExpUE::=U |U = UE |UE和UE |UE或UE|UE暗示UE|非UE见图9。 单位注释语言连接词逻辑运算符有其标准的优先级,在这里所示的简化文法中没有反映出来单位注释语言可以在标记为UNITS注释的注释中使用 这些注释被更改为自定义断言和假设状态,并具有特定于策略的处理。CPF[UNITS]将根据当前环境,通过首先确定任何表达式的单位来检查断言和假设。 假设s被视为单位赋值,赋值从右到左-- unit(x)= meter将单位meter赋值给变量x,而unit(x)= unit(y)将y的单位赋值给x。通过比较,断言被视为逻辑检查,使用单元的组合执行单元比较图4中的理论,以确定单元何时相等,以及检查表达式时在单元合并期间使用的单元兼容性概念。未注释的函数和对象被保守地处理,函数被赋予默认的注释,对象被赋予新的单位(在上面的第5.3.3节中描述),允许检测不正确的使用5.4运行CPF[UNITS]作为使用CPF[UNITS]的示例,图1显示了使用单位的C程序的一部分。如第1节所述,这段代码包含单元错误并不明显。通过添加图中所示的注释,CPF[UNITS]可以检查程序的单位错误。这将给出以下输出:函数finalEnergy:ERRORon line 26(1):Assert failed!此消息显示代码实际上有一个单位错误,在本例中为在线错误。26.第1节解释了该错误的潜在原因。类似地,任何断言失败都将报告给用户,并在可能的情况下提供附加信息。例如,由加法操作触发的错误将报告行号以及错误是由无效加法引起的事实6评价使用两组实验进行评价。所有测试都在同一台计算机上进行,这台计算机是奔腾43.40 GHz,具有2 GB RAM,运行Gentoo Linux和Maude 2.3。首先,重点放在性能上,确保使用每个功能分析可以按需扩展。结果示于图10. 在这里,每个测试执行一系列数值计算:64M. Hills等人理论计算机科学电子笔记290(2012)51总时间每个功能的测试LOCX100X400x4000X100X400x4000直256.3923.00229.800.060.060.06安278.6231.27307.540.090.080.08诺斯普利特6912.7146.08467.890.130.120.12分裂6927.40106.551095.340.270.270.27以秒为单位的时间所有时间均为每次测试的三次运行的平均值。 每个函数的代码行(line of code),在源文件中有100、400或4000个相同的函数见图10。 CPF[UNITS]性能测试准备时间检查时间LOC功能注释错误FPex18.c0.0830.7541831030fe.c0.1130.79619第二章(三)910coil.c0.11359.870299第四章(三)1433projectile.c0.1220.88231第五章(二)1600projectile-bad.c0.1210.86631第五章(二)1610big0.c0.2735.22327051000big1.c0.99822.853117051000big2.c33.144381.367966111000以秒为单位的时间所有时间均为每次测试的三次运行的平均值。函数计数包括括号中的带FP代表假阳性。见图11。 CPF[UNITS]单位误差检测直线代码;ann包括与straight相同的代码,但添加了许多单元注释;nosplit包括许多嵌套条件,这些嵌套条件统一地改变变量的单元,只留下一个环境;split包括嵌套条件,这些嵌套条件在不同的分支中不统一地改变变量单元,产生八个不同的环境,在这些环境中需要评估语句对于每个函数,使用CCCC工具[22]得出的代码行数,相同的函数重复100,400或4000次。如图10所示,性能几乎是线性增长的:要检查的函数数量增加四倍,总处理时间大约增加四倍。每个函数的处理时间很短,这使得CPF[UNITS]成为在开发过程中检查单个函数的现实选择,这在其他一些需要一次检查整个程序的解决方案(如C-UNITS)中是不可能的拆分环境会增加执行时间,但并不过分:在八个环境中,每个函数处理拆分的时间大约是处理nosplit的两倍,而不是八倍,后者只有一个环境。最后,在units注释语言中处理注释似乎不会增加多少开销;注释在处理过程中被视为语句,因此在某种意义上,只需添加额外的第二组实验与Osprey使用的一些相同示例进行比较,其中一些示例最初来自C-UNITS,结果显示在M. Hills等人理论计算机科学电子笔记290(2012)5165图11. fe. c是图1所示的示例;coil. c是电感计算器的一部分;projectile. c计算射弹的发射角; projectile-bad. c也是如此,但具有有意引入的单位误差。big0.c、big1.c和big2.c包含一系列重复的算术运算,旨在测试CPF[UNITS]可以处理的函数的大小,其中big2.c是一个特别不切实际的例子。总的来说,图11显示注释负担并不重:有时需要对变量声明进行假设,而经常需要前置条件和后置条件,Osprey需要的注释数量相似(尽管Osprey使用的注释数量通常较小)。big0.c、big1.c和big2.c不需要注释,而coil. c需要14个注释,包括函数原型。fe.c需要9个注释,ex18.c需要10个注释。projectile.c的例子特别有趣:使用一种更灵活的an-符号语言允许比其他一些系统更通用的程序版本被检查(如第2节所讨论的),维护单位多态性,而projectile-bad. c包括一个Osprey无法捕获的错误,因为该错误涉及在同一维度中使用不同单位(磅与千克)的变量。总的来说,在projectile.c和projectile-bad. c中,5个函数和2个原型类型只需要16个注释。coil. c展示了CPF[UNITS]方法的一个缺点:其中一个goto语句永远不会稳定,这意味着单位随着每次迭代而不断变化。 这会在程序中引发一个错误,在这种情况下,这似乎是一个假阳性。7今后的工作和结论本文介绍了一个基于C语言抽象重写逻辑语义的静态分析工具CPF[UNITS],用于检查C程序的单元安全性。该工具提供了一种模块化、可扩展的方法来检测单元违规。与许多基于类型或库的方法不同,CPF[UNITS]不需要对基础语言进行更改最后,使用模块化框架,C策略框架和重写逻辑中的底层抽象语义允许快速测试新功能和扩展,例如注释语言的扩展。有几个领域可以扩大合作伙伴关系[单位]。首先,有些C代码还不能安全地分析。 这包括使用以下功能的代码,不是类型安全的,例如指针算术和联合,以及使用二义性函数指针的代码。扩展CPF[UNITS]定义,同时使用来自CIL的其他分析信息,应该可以安全地处理更多的此类情况。其次,围绕别名和全局变量的一些保守假设分析能力,而不会失去正确性。第三,对全局变量和结构定义的注释将允许对相关单位的假设。66M. Hills等人理论计算机科学电子笔记290(2012)51全局变量或结构的实例只声明一次,而不是在使用它们的函数中声明它们;这些都是目前正在添加的。第四,错误信息正在改进。 最后,还有一些有用的注释, 正确处理,包括依赖于指数中变量的单位注释(例如,给定整数n,变量x的单位为n)。扩展注释语言的功能将增加CPF[UNITS]的功能,使其能够处理更复杂的情况。引用[1] C政策框架,http://fsl.cs.uiuc.edu/cpf。[2] 火星气候Orbiter,http://mars.jpl.nasa.gov/msp98/orbiter.[3] NIST关于常数、单位和不确定性的参考,http://physics.nist.gov/cuu/Units/。[4] Allen,E.,班内特和R. Cartwright,A First-Class Approach to Genericity,in:OOPSLA96比114[5] Allen,E.,D. Chase,V. Luchangco,J. W. Maessen和J. Guy L. Steele,Object-Oriented Units ofMeasurement,OOPSLA384-403[6] Barnett,M.,K. R. M. Leino和W.Schulte,规范#编程系统:概述,在:CASSIS49比69[7] 布朗,W。E、SIUNITS中的应用模板元编程:基于单元的计算(2001)。[8] 伯蒂湖,Y. Cheon,D.R. Cok,M.D. Ernst,J.Kiniry,G.T. Leavens,K.R. M. Leino和E.民意调查,JML工具和应用程序概述,见:Proceedings of FMICS[9] 陈芳,G. R. P. Ven katesan,尺寸安全性的基于规则的分析,见:RTA'03的程序设计,LNCS 2706(2003),pp. 197-207.[10] Cl avel,M.,F. 杜兰,S。 Ek e r,P. Lincoln,N. Mart's-Oliet,J. Meseguer和C. L. Talcott,编辑,“关于Maude的一切-一个高性能逻辑框架,如何指定,编程和验证系统Rewriting Logic,[11] Cousot , P. and R. Cousot , Abstract Interpretation : A Unified Lattice Mod
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![dll](https://img-home.csdnimg.cn/images/20210720083646.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.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)
会员权益专享
最新资源
- 保险服务门店新年工作计划PPT.pptx
- 车辆安全工作计划PPT.pptx
- ipqc工作总结PPT.pptx
- 车间员工上半年工作总结PPT.pptx
- 保险公司员工的工作总结PPT.pptx
- 报价工作总结PPT.pptx
- 冲压车间实习工作总结PPT.pptx
- ktv周工作总结PPT.pptx
- 保育院总务工作计划PPT.pptx
- xx年度现代教育技术工作总结PPT.pptx
- 出纳的年终总结PPT.pptx
- 贝贝班班级工作计划PPT.pptx
- 变电值班员技术个人工作总结PPT.pptx
- 大学生读书活动策划书PPT.pptx
- 财务出纳月工作总结PPT.pptx
- 大学生“三支一扶”服务期满工作总结(2)PPT.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](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)