上下文相关过程和C语言中的计算类型推理的电子笔记

理论计算机科学电子笔记174（2007）61-78www.elsevier.com/locate/entcs上下文相关过程和C语言中的计算类型Andreas Schlosser Christoph Walther Michael GonderMarkus AderholdFachgebietProgrammiermethodikTechnischeUiversita？tDarmstadt Germanyhttp://www.informatik.tu-darmstadt.de/pm摘要我们将加强语言功能的改进，因为语言功能用于编写程序和制定有关程序的声明。上下文相关的过程允许规定过程被合理执行的上下文，从而避免程序代码中的运行时测试以及通过证明过程调用的无卡住来验证不存在计算类型导致更紧凑的代码，增加程序的可读性，并使类型系统的众所周知的好处也适用于非自由生成的数据类型。 由于上下文需求的满足以及类型检查变得不可判定，因此证明义务被合成以由手头的验证器证明，从而支持静态代码分析。关于类型层次结构的信息用于提高验证器的性能和效率保留字：上下文依赖，计算类型，类型推理，子类型。1介绍我们开发了CeriFun系统[1，14，15]，一个用于定义用函数式一阶编程语言L[12]编写的程序语句的系统。这种语言包括自由生成的多态数据类型的定义原则，以及基于以下内容在这些数据类型上操作的过程：递归，案例分析，let表达式和函数组合，以及关于数据类型和过程的陈述（L中称为过程在按值调用规程中进行评估。数据类型bool具有构造函数true和false，N用于自然数，构造函数为0和+（.. . ）的后继函数在L中预先定义。引理是通过使用案例分析和真值来表示连接词的泛量化来定义的。 后定义数据类型，构造函数的每个参数位置都提供了一个选择器函数，例如-（.. . ）是构造函数+（.. . ）从而表示前导函数，hd和t1是列表构造函数的选择器，1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.03862A. Schlosser等人/理论计算机科学电子笔记174（2007）612（i）bool=true，false结构N = 0，+（−：N）结构列表[@X]=ε，[in fix]：：（hd：@X，tl：list[@X]）函数[out fix]|（k：list [@ X]）：N <=如果？（1）0= 0，0 = 0，0 = 0（|tl（k）|）结束function[in fix]！！（k：list[@X]，n：N）：@X<=如果？ε（k）then*else if？0（n）then hd（k）else（tl（k）！！−（n））end endfunctionordered（k：list[N]）：bool=如果？ε（k）则为真否则如果？ε（tl（k））则为真else if hd（k）>hd（tl（k））then false else ordered（tl（k））end end endfunctionfind（key：N，a：list[N]，i，j：N）：bool=如果|一|> J如果j=ikey=（a！（一）如果j > i则设h：=i+，1（j−，in=（a！！ h）在如果mid> key然后find（key，a，i，−（h））else if key>mid then find（key，a，+（h），j）elsetrue end end endelse false end endelse false端函数binsearch（key：N，a：list[N]）：bool=如果？（1）A，B，C，D|一|））endlemmabinsearch is sound=sounda：list[N]，key：N如果{binsearch（key，a），key∈a，true}lemmabinsearch is complete={a：list[N]，key：N如果{ordered（a），如果{key∈a，binsearch（key，a），true}，true}A. Schlosser等人/理论计算机科学电子笔记174（2007）6163图1.一、用二分查找查找列表64A. Schlosser等人/理论计算机科学电子笔记174（2007）61参见Fig.1.类型变量前面有“@”，表达式形式为？cons（x）被用作x=cons（sel1（x），.，seln（x）），其中cons是构造函数，seli是属于cons的选择器，因此例如？：：（x）holds i表示列表x不为空。该语言还支持过程的不完全定义[16]（在文献中也称为松散规范或欠规范），在通常导致运行时错误或错误的情况下，使用符号*表示不确定的结果。例外.例如，程序！！计算列表的第n个元素，其中列表元素从0开始从左到右寻址因此，（k！！）n）是未定的（在！！的主体中用* 如果|K|≤ n。不完全定义也被用来定义抽象映射，如arity函数。 ǁ图3 .第三章。图1给出了一个L-程序的例子，用于通过二分搜索方法在有序列表中进行搜索，以及说明搜索过程的可靠性和完整性的引理，参见。[13 ]第10段。2上下文相关过程2.1语境从句我们把只能在特定上下文中执行的过程称为上下文依赖的过程.上下文依赖是计算机科学中的一个“老主题”。几乎所有的编程语言都提供了某种机制来规定上下文依赖性，dency，汇编语言，LISP的早期方言等是罕见的例外。如今，编程语言提供了精心设计的类型系统，允许在编译时检查上下文属性。我们在讨论上下文依赖时的重点是与类型检查不同的需求，这些需求通常是不可判定的，因此需要定理证明来检查上下文约束的满足情况。通常，过程的上下文需求是过程的形式参数上的谓词如果在调用上下文中不满足此要求，则过程调用的结果（如果有的话）可能是任意的因此，在调用上下文中满足上下文要求是过程按预期方式运行L-程序P的上下文相关过程f由以下形式的表达式定义：函数f（x1：τ1，. ，xn：τ n）：τ <=假定c f; body f .（一）上下文子句c f∈T（P），{x1，.，xn}）由假定声明给出的bool由布尔项表示，该布尔项用由程序P的数据类型和过程定义（由签名给出）定义的函数符号（除f外）构建P）和过程f的形式参数xi。上下文子句cf定义了一个前提条件，在执行f的过程调用时需要保持这个前提条件。由于assume声明是可选的，如果过程体中没有显式提供上下文子句，则默认情况下cf使用trueA. Schlosser等人/理论计算机科学电子笔记174（2007）6165FFF上下文相关过程的语义被简单地定义为其相对化版本函数f（x1：τ1，.，xn：τn）：τ< =主体ctx，其中bodyctx：= ifc fthen bodyfelse*end表示f的相对化body。以来所有的选择器都是不完全定义的，选择器也被分配了一个上下文子句：对于一个构造函数，cons与相应的选择器sel1，.，seln，选择器调用seli（x）的上下文子句c sel i定义为？cons（x）声明选择器只能应用于它所属的构造函数。例如，程序！！可以使用如图2所示的上下文子句来重新表述图1的结构。这个上下文子句要求过程调用（k！！n）只出现在保证n是列表k的合法地址的上下文中。作为|K|> n如果k=/ε，则对？ε（k）（和i∈T∈R∈R ∈S∈T*i∈R∈N）被简化在过程的上下文相关版本的主体中， 因此调用时没有异常！！now由context子句静态保证。因此，执行程序！！更重要的是，当（|K|，n）测试？ε（k）保存在上下文相关版本中。过程find的定义也在图2中得到了细化。上下文子句要求|一|对于列表a中的搜索区间的上界j和下界i， 同样在这里，由于在每次（递归）调用过程find时动态执行的测试被静态测试所取代，因此获得了更有效的过程：|一|>j和j> i被保存，这两者都导致成本与[log 2（j-i + 1）]成比例。|在原始版本的find。2.2语境假设为了保证过程（或选择器）f仅在术语t内的有效上下文中被调用，为t生成所谓的上下文要求，表示在t中调用任何f的上下文需要f的上下文子句cf（其中cf中的形式参数被调用的实际参数替换定义2.1 [上下文要求]对于项t，集合Octx（t）<$Occ（t）是t中所有上下文敏感事件的集合，即事件π∈Occ（t）使得t|π= g（ti，. ，t，n），并且g是选择器或过程函数符号。1项t的上下文要求CR（t）被给出为AND（{CR（t，π）|π∈Octx（t）}），其中CR（t，π）= if{COND（t，π），θ（c g），true} if t|π= g（ti，.，tn），θ用实际参数ti代替g的形式参数xi。2对于（1）中的过程f，f的上下文假设被定义为引理f$ctx<=πx1：τ1， . . . ，xn：τnCR（bodyctx），且该系数x该点是一个线性矩阵引理lem<=λx1：τ1， . . . ，xk：τkbodydylem（2）定义了一个引理m$ctx<=πx1：τ1， . . ，xk：τkCR（bodylem）.1通常，Occ（t）是所有出现的t，t| π表示t在出现π时的子项，t [π←r]由t替换t得到|π R2AN D （ {b1 ， ...， bn} ） - 所 有 的 随 机 数 都 是 AND （ b1 ， ...， BN ） -abb_reeviate_sabo_l_eanter_r_er_er COND（t，π）是子项t的所有第二个条件的共轭|π。66A. Schlosser等人/理论计算机科学电子笔记174（2007）61FCeriFundemandds hhaprocnteh et e hetesaproc hete e dh esap roc n t e e此外，在验证引理之前，例如，使用hd、tl、-（.. . ），和！！，语境假设！！$ ctx是为上下文相关过程生成的！！的上下文子句，并且（使用-（. . ）和FIND）为过程BinSearch的上下文相关版本生成上下文假设BinSearch$CTX。图2中也显示了图1中的词元binsearch的上下文假设是完整的2.3决定假说当调用一个不完全定义的过程时，可能会导致所谓的卡住计算 对于每个用户定义的过程函数f（x1：τ1，.，xn：τ n）：τ< =. . 、CeriFun是指在预处理过程中调整大小的过程函数τf（x1：τ1， . . . 、x n：τ n）：bool< =. .域过程f总是被完全定义的，即在调用域过程f时不会发生卡住的计算，并且在调用“母”过程f时提供了不存在卡住的计算的等价要求，即 计算Δ wf（q1，. ，q n）产生f（q1，. ，q n）不会卡住，详见[16]。图2：在过程中，我将执行一个三维空间！！由CeriFun提供的尺寸适合于生产-dure！！. 3因此在调用（k！！n）是保证i计算！！（k，n）为真。但是作为域程序，只是提供了一个递归的定义，|K|> n，计算（k！！n）不会卡住|K|>n满足于过程调用（k！！n）。使用域过程，可以确定是否存在卡住的计算静态地。 为此，给出了一个所谓的判定假设引理f$det=x1：τ1， . . . ，xn：τn如果{cf，τf（x1， . . ..判定假设简单地表示过程的上下文子句对于不存在卡住的计算是足够的因此，过程f的调用的上下文要求的真值必然不存在假设f4作为示例，图2显示了确定假设！！$为程序而生！！.3计算类型3.1非自由生成的数据类型L中的数据类型是自由生成的，这意味着L-程序P的单态类型τ的语义-要么直接定义，例如bool和N，要么以其他方式作为非单态数据类型的单态实例获得，例如list[N]，list[list[N]]等。可以定义为带载波的自由项代数3.当为上下文相关过程f合成BMPf时，将使用主体ctx[4]判定假设的验证通常不能被要求，因为抽象映射的调用，如过程映射。. 在图3中，两个变量是固有的不确定性。A. Schlosser等人/理论计算机科学电子笔记174（2007）61672（i）function[in fix]！！（k：list[@X]，n：N）：@X<=假设|K|>n; if？0（n）then hd（k）else（tl（k）！！−（n））endlemma！！$ Ctx=Ctk：list[N]，n：N如果，|K|> n，如果{？0（n），？ * （k），如果{？ * （k），如果{？+（n），|tl（k）|> −（n），false}，false}}，真}函数！！（k：list[@X]，n：N）：bool=如果|K|>n那么如果？0（n）那么呢？* （k）否则如果？：：（k）那么，请！（tl（k），−（n））else false end end否则假结束lemma！！$ det<= k：list [N]，n：N if {|K|> n，n！！（k，n），true}functionfind（key：N，a：list [N]，i，j：N）：bool <=假设如果{i> j，假，|一|};如果j=it henkey=（a！！（i），否则，让h：=i+1（j−，在let mid：=（a！！ h）在如果mid> key然后find（key，a，i，−（h））else if key>mid then find（key，a，h，j）else trueend end end端函数binsearch（key：N，a：list[N]）：bool=假设命令（a）;如果？（1）A，B，C，D|一|））endlemmabinsearch$ctx=nexta：list[N]如果{ordered（a），如果{？ε（a），tre，如果{？+（|一|），if{0>−（|一|），false，|一|>−（|一|）}，false}}，真}lemmabinsearch is complete$ctx=$a：list[N]，key：N68A. Schlosser等人/理论计算机科学电子笔记174（2007）61如果{order（a），if{key∈a，ordered（a），true}，true}图二. 上下文相关过程A. Schlosser等人/理论计算机科学电子笔记174（2007）6169T（P）c）τ上的构造函数符号的签名T（P）c然而，人们通常只关心T（n（P）c）τ的真子集。例如，素数集合P<$ N在数论中使用，而“类型”列表[P]的列表范式也被非常频繁地使用，例如用于高效搜索：图1的过程binsearch，例如，操作有序列表，其中有序是自由生成的数据类型列表[N]的真子集。所有这些例子都有一个共同点，那就是我们所关注的某些结构--素数、范式等。不是自由生成的，而是某些自由生成的数据类型τ的真子集。因此，. .必须用它来决定一个类型为τ的项是否是s的成员。随后，我们将使用像自由生成的数据类型这样的过程，我们称它们为计算类型，因为为它们提供了算法定义3.1[计算类型]设P是L-程序P的所有多态类型的集合，设W P是类型变量的集合，设M P是所有单态类型的集合。5我们将P的类型系统扩展为一个集合M：=Mi∈i其中M0=M和M一期+1：=Min{γ ∈ n（P）|γ：δ → bool for someδ∈Mi}<${<$[γ1， . . ，γn]|这是一个非对称的过程， . ，γn∈Mi}. P是所有多态类型的集合，其中允许使用来自M\M的计算类型实例化类型变量 类型γ ∈ P的基类型P（γ）∈P被定义为γ，如果γ∈M <$W，P（γ）：= P（δ），如果γ∈Mi+1，并且对于某些δ ∈ M i，γ：δ→bool，并且P（γ [γ1，.，γ n]）：= π [P（γ1），.，P（γ n）]。P-子类型关系≤P被定义为直接P-子类型关系«PP × P的自反和传递闭包，直接P -子类型关系被定义为满足以下条件的最小关系：（i）π（τ）<

下载后可阅读完整内容，剩余1页未读，立即下载