定义描述在函数式编程中的应用以及其在命令式程序开发中的作用

≤ ≤≤理论计算机科学电子笔记225（2009）83-98www.elsevier.com/locate/entcs定义刻划与Dijkstra奇整数的奇幂休·吉本斯1计算机科学系，爱尔兰都柏林三一学院摘要使用弗雷格-罗素风格的定义描述来赋予函数意义已经很久了，我们研究了它们在函数式程序开发中的应用，并从这些程序开发到正确的命令式程序的开发。特别是，我们调查的一个问题，“奇整数的奇权力”，讨论了Dijsktra的功能程序的发展。如果终止的正确性是如果不是一个问题，那么开发一个部分正确的程序是很简单的。为了开发一个完全正确的程序，还需要规范的其他性质关键词：定义描述，函数式编程，断言，部分和全部正确性。1引言定义摹状词的使用可以追溯到弗雷格和罗素[13]，也可以追溯到奎因[12]和斯科特[14]的进一步发展。在Kalish和Montague [9]中解释了定义摹状词的使用和定义。在本文中，我们考虑在函数式程序的开发中重用定义描述。由于断言在Dijkstra [5]和Gries [8]以及Refinement Calculus [11]所提倡的命令式程序的开发中具有核心作用，因此我们考虑了定义描述在函数式程序开发中的作用，然后可以进一步开发为命令式程序。在这篇文章中，我们详细研究了Dijkstra [6]所描述的一个规范的对于1p和奇数p和1k和奇数r使得1r2k，<存在，1 ≤ x <2k <$2k|（x p − r）odd x1电子邮件：hugh. cs.tcd.ie1571-0661/© 2008 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2008.12.06884H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）83我们正在使用'|' di vi des ' 的意 思。如果终止证明不是一个问题，那么可以很容易地开发出一个非常简单的部分正确的程序。终止性的证明使用归纳法，并从归纳法的证明中推导出一个简单的函数程序。在此函数程序的基础上，开发了一个完全正确的命令式程序，该程序类似于Dijkstra给出的程序。 使用函数程序推导出规范的进一步性质，并推导出替代函数程序。虽然替代函数式程序是直接的，但它向命令式程序的发展这种发展涉及到线性递归转换到一个适当的尾部递归形式，然后可以直接转换为命令式程序与尾部递归程序提供相关的循环的不变量。在规范的函数版本的开发中，我们使用了定义描述符1.1明确的描述，y=唯一满足p y=（x·p x）的（罗素）（（奎因）{y}={x·px}1.2定义描述，y=（least x·n≤x<$p x）<$n≤y <$py<$（<$x·n≤x y → <$（p x））特别是g n=（least x·n≤x<$p x）=（pn→n）<$（<$（pn）→（least x·（n+1）≤x<$p x）=if pn thenn elseg（n+1）在函数式编程列表方面y=（least x·n ≤x <$p x）y = head [x |x ← [n.. ]，px]1.3简单地板平方根作为定义描述的一个介绍性应用，我们开发了一个简单的程序，用于查找一个数的整数平方根对于0≤x，我们定义x的（正）平方根，如下：x=（r·0≤r<$r2=x）H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）8385[我们可以定义平方根，r=[XX XX]r≤r <$x≥（r+ 1）2））n（nr·0≤ry →x ≥（r+ 1）2）{witnessr=y−1}x≥y结束证明。Q让fl_sqrt x n=（least r·n≤r<$x（r+ 1）2）=if x（n+ 1）2thenn else fl_sqrt x（n+ 1）因此fl_sqrt x0=[x]将其作为函数式程序编写：x哪里_sqrt x n| x<（n+ 1）2 卢恩| x ≥ (n + 1)2 ≡ fl _sqrt x (n + 1)我们可以直接基于函数程序将这个尾部递归函数程序重写为具有循环不变量[实数−整数：：实数→整数286H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）83≤ ≤≤[x{上一条：0≤x}localn：Intbeginn：=0{Inv：fl_sqrtx 0 =fl_sqrtx n}当x≥（n+ 1）2时，n：=n+1end{fl_sqrtx0=n}[详细]结果 ：= n端在这里，尾部递归程序，sqrt，被用作循环不变式。在Gibbons [7]和Broy和Krieg-Bruckner [3]中进一步发展了尾递归和循环不变量之间的这种联系。2Dijkstra为了清楚起见，我们重复上面给出的Dijkstra规范。持续1p和奇数p和1k和奇数r使得1r2k，存在一个值x，使得<1≤ x <2 k <$2 k|（x p − r）odd x实施例2.113是存在性量化器x的 见 证 者 ，（x·1 ≤ x<24 <$24|（x3− 5）odd x）as24|（133− 5）16|（2197 - 5）2192= 137 ×16x在（<$x·0 ≤ x <$2k）中的证明|（x p− r））必须是奇数，因为2k|（x p− r）则xp−r是偶数，因此xp是奇数，因为r是奇数，因此x是奇数。2.1定义描述函数考虑下面的函数f，由一个定义描述来描述，用于找到x的见证，设prep r k=1≤p<$odd p<$1≤k<$odd r<$1≤r2k<前p r k→f p r k <$（least x·1 ≤ x<2k <$odd x <$2k|（xp − r））即使用前提条件{前p r k}f p r k <$（least x·1 ≤ x<2k <$odd x <$2k|（xp − r））H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）8387≡--≡--我们将f p r k重写为函数式程序。 使用列表理解，{前p r k}f p r k k k k头[x]|x ← [1.. 2k]，奇数x，2k|（x p-r）]或者使用高阶函数，滤波器前P R Kf pr khead（filter b[1，3，. ]）哪里b x x<2k 200万美元|（xp − r）因为一般来说，g n<$（least x·n≤x <$b x）如果b n那么n else g（n+1）我们得到一个交替的（尾递归）函数程序，f1，前P R Kf1p r k floc1哪里flocx| 2K|（xp − r）<$x<2k <$x| 否则，则返回floc（x+2）我们可以使用Quickcheck [4]来测试函数f和f1是否相同。我们可以将函数程序f1重写为迭代命令式程序：见图算法1（命令式f1）算法1Imperative f1f1：：Int×Int×Int→Intf1（p，r，k）{Pre：1≤p1≤k1≤r2localx：Intbeginx：=1{Inv：floc1 =floc x}n=100当<$（2 k|（x p−r）x<2k）dox：=x+2端{floc1 =x}{f1pr k=x}{2k|（x p− r）<$x<2k <$odd x}结果 ：= x端88H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）83|−∧≤∃·≤∧|−∃·≤∧ |−2K⇒−=−=−2K−这个命令式程序中的循环遍历奇数，直到它到达一个x，使得2k（xpr）x2k。<测试时，程序会对给定的输入暂停，但测试不足以证明正确性。如果循环终止，那么程序将给出正确的结果。3替代FP版本为了证明循环终止，我们回到了的假设（x·odd x 1 ≤ x<2k2|（x p− r））前p r k：1 ≤ p odd p 1 ≤ k odd r 1 ≤ r <2 k。在修饰演算的背景下，一个正常的策略是加强前提条件，但在这里，前提条件通过删除合取而被削弱，1r2k，因为它可以表明，（x1x2k（xp r））从较弱假设前Jrk：1≤poddp 1≤kodd r满足Pre的也满足PreJ，即Pre PreJ.稍后我们将证明对于（x1x2k（xpr））的最小见证x ∈ x ∈ x ∈ k是这样的，x ∈x∈ <2k。定理3.11≤ p <$odd p <$1 ≤ k < $odd r <$（nx·odd x <$2 k|（x p− r））证明（通过k上的归纳）基本情况（k=1）设x = 1;由于r是奇数，则1p − r是偶数，因此2|（1p − r）而且，x = 1是最小的x。诱导步骤：假设x是最小的x，使得奇x≠2k|（x p−r），确定最小奇数y使得2k+1|（y p− r）。如果2k+1|（x p−r），设y= x如果<$（2k+1|（x p−r）），则xp− r是奇数。设y=x+2k，yp r2K（x+2k）pr2Kx p+p xp−12k+. +px2（p−1）k+2pkr2K=x p− r+p xp−1+. +px2（p−2）k+ 2（p−1）kxp r{2k和p xyp−rp−1 奇怪的}2k是偶数H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）8389≡≡|−|−¬|F 第十一条2k+1|（yp−r）同样，y=x+2k是最小的，因为如果y=x+n，且n为偶数n，则（x+n）p−r=x p − r+p xp−1n+. +np2k2k=xp− r+n（p xp−1 +. +np−1）2k2k2k（x pr）但 （2k n（px p−1+. +np−1））asn2kandpxp−1+.< p-1是奇数。Q从这个归纳证明中，我们得到了递归函数程序f2prk，用于找到x，使得奇x≠2k|（x p−r）{≤p<$odd p<$1≤k<$odd r}2f2pr（k+1）if2k+1（xpr）then x else x+2k哪里2006年12月2日很明显，这个函数终止于前提条件：1 ≤k。定理3.2前p rk前prk<哪里pre p rk1 ≤ podd p1 ≤ kodd r1 ≤r2k证明（通过对k的归纳）基本情况：（k=1）f2pr1=1<2归纳步骤：（k>1）假设f2pr k2k<案例2k+1|f2pr kf2pr（k+1）=f2pr k<2K<2k+1案例<$（2k+1|f2pr k）f2pr（k+1）=f2pr k+2k<2k + 2k= 2k+1最终证明。Q90H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）83≤ ∧ ∧ ≤ ∧∧∈|−函数f2p r k也满足更强的规范：1≤p<$odd p< $1≤k<$odd r<$1≤r 2k→f2prk（least x·1≤x2kodd xxp mod2k=r）因此，它是一个满足Dijkstra给出的规范的函数程序Dijkstra提供了一个基于不变量的1≤x<2 k<$2 k|（x p−r）odd x关于他自己的强制性解决方案，Dijkstra在[6]中指出“I 如果你不相信我，你可以在你的同事身上试试我们从递归形式f2prk导出一个迭代解.3.1迭代版本上面的命令式程序f1，可以被认为是原始f的命令式解，一旦终止性得到保证。迭代程序的一个更直接的形式可以从递归程序f2发展出来.考虑集合F={（（p，r，k），y）·1≤k<$odd p<$1≤p<$odd r<$y=f2prk}设pre p r k = 1K奇数并联1p奇数r1 le r对于k= 1若（（p，r，k），x）∈F，则若2k+1（xpr）则（（r，k+ 1），x）F其他（（p，r，k+1），x+2k）∈F（（p，r，1），1）∈ F.集合F是有序对的归纳定义集合，使得（（p，r，k），y）∈Fy=f2prk基于归纳集F，我们得到迭代函数ft的具体化1≤k<$odd p，r< $1≤p，r→ftp n r k x<$（least y·k=n<$（（p，r，k），y）∈F <$x=y）我们写ftp n r k x作为函数程序，{odd p<$1≤k<$odd r}ftp n r k x− −{x=f2p r k<$1≤k ≤n}H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）8391| k= nx| 2k +1|（x p − r）<$ftn r（k +1）x| 否则n =tp n r（k +1）（x +2k）将其重写为命令式程序;参见算法2（Imperative ft），算法2Imperative ftft：：Int×Int×Int →Intft（p，r，k）{Pre：1≤p<$odd p<$1≤k<$odd r<$1≤r2}当地j，x：Int开始x：=1;j：=1{Inv：2k|（x p− r）<$odd x <$1 ≤ j ≤ k}而j/=kd0如果2 j+1|（x p− r）则j：=j+1其他x：=x+2j;j：=j+1结束结束{2k|（x p−r）<$odd x}结果 ：=x端而不是显式地使用2k，我们可以隐式地计算它，如下所示：见算法3（Dijkstra版本）。这是一个类似于Dijkstra开发的版本，就像这里开发的版本一样，不使用限92H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）83制1≤r2k。0，假设i为真，i为真。i=（leastj·<$b（gjx））tf。 考虑到GXi−1=（leastj·<$b（gj（gx）设gs1=[gi−1（gx），gi−2（gx）， . gx]通过归纳，\n gs1 =lr（g x）由于i>0lr x=n（lr（g x））x=n（\n gs1）x{defn. \n}=\ngs结束证明。Q4.2.1实施LR X由于lrx=\n[gix，gi−1x . 其中=（leastj·<$b（gjx））考虑到rimplementing |n（x：xs）。对于项目x和列表xs，定义一个函数lrt，通过lrtx xs=\n（x：xs）tf。lrt x[]=\n[x]=x此外，对于xs=y：ys/=[]，lrtx xs=\n（x：（y：ys））{prop. \n}H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）8397=\n（（nx y）：ys）=lrt（n x，y）ys98H. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）83\\函数lrt是尾递归函数lrt x xs =如果xs /= [ ]then lrt（n x（head xs））（tail xs）else x它可以被重写为命令式程序，我们可以用它来为LRT编写命令式程序。（算法4）算法4lrtixi i−1{Pre：gs=[gx，glocaly：Int; ys：[Int]beginx，.. . g x，x]}y：=头部gs; ys：=尾部 gs{Inv： ngs=n（y：ys）}whiley= []doy：= n y（headys）ys：=tail ys恩德{y=lrt x}结果：= y结束lrti4.2.2最终实施现在仍然需要的是一个计划，gs=[g i x，g i−1x，. . . gx，x]，其中表示法：i=（leastj·<$b（gjx））对于列表xs、ysxs++ys是列表的连接。末端符号以类似于实现\n gs的方式，我们考虑实现函数px xs =[g i-1x，. . . g x，x]++ xsa s foreac h 0≤j[Int]init_lrtx{Pre：（i）i=（l）eastj·<$b（g）jlocaly：Int; gs：[Int]beginy：=x;gs：=[]（x））}而（by）do{Inv：px[]=py gs}gs：= y：gsy：=gyend{y=gi x}gs：= y：gs{Post：gs= [g i x，g i−1x，. . . gx，x]}结果：= gsend init_lrt5结论本文根据Dijkstra对“奇整数的奇次方”问题的具体化，应用定义描述理论和函数式程序设计思想，首先开发出正确的函数式程序，然后再开发出正确的命令式程序如果终止的正确性不是一个问题，那么开发一个部分正确的命令式程序是很简单的。通过开发功能程序的许多属性的程序建立，而Dijkstra开发了一个完全正确的程序通过他自己的最弱的先决条件技术，目前还不清楚如何其他属性可以建立。这里示出了fp r k=fp（r mod2k）k并且因此r2k的限制是多余的，这是Dijkstra没有注意到的。完全正确的函数程序的开发是独立于DijstraH. Gibbons/Electronic Notes in Theoretical Computer Science 225（2009）83101更全面的发展呈现在这里。包括函数式程序的开发，阐明了命令式程序的开发，本文同意Manna和Waldinger的观点，他们指出，“Recursion在这篇文章中，递归也被用作开发命令式程序的循环不变量的工具，因此将命令式程序的开发与函数式程序的开发相引用[1] 鲍尔，F.和H.Wossner，[2] 伯德河列表理论导论，M。Broy，编辑，程序设计逻辑和离散设计演算，Springer-Verlag，1987。[3] Broy，M.和B. Krieg-Bruckner，Derivation of Invariant Assertions During Program Development byTransformation，ACM Transactions on Programming Languages and Systems2（1980）.[4] Claessen，K. 和j. Hughes，Specification-based testing with quickcheck，in：J. Gibbons和O. deMoor，editors，the fun of programming，Palgrave Macmillan，2003.[5] Dijkstra，E.，“A Discipline of Programming,” Prentice Hall,[6] Dijkstra，E.，[7] Gibbons，H.，“Integrating Relational and Imperative Programming via a Weakest Precondition 论文，都柏林三一学院（1990年）。[8] Gries，D.，[9] Kalish，D.，R. Montague和G. Mar，[10] Manna，Z.和R. Waldinger，Synthesis：Dreams => programs，Technical report，Stanford ResearchInstitute（SRI）（1977）.[11] 摩根，C.，[12] Quine，W.，[13] Russell，B.，在表示上，在：A. Martinich，editor，The Philosophy of Language，OxfordUniversity Press，1996.[14] Scott，D.，形式逻辑中的存在性和描述，在：K。兰伯特，编辑，自由逻辑的哲学应用，牛津大学出版社，1991年。