函數(shù)式編程語(yǔ)言、編程和程序驗(yàn)證-資料下載頁(yè)
2024-10-19 21:04本頁(yè)面
【導(dǎo)讀】學(xué)習(xí)函數(shù)式語(yǔ)言是因?yàn)檎n程實(shí)踐所用工具中，需要用函數(shù)式風(fēng)格編程。函數(shù)式語(yǔ)言SML的模塊系統(tǒng)。函數(shù)式程序的驗(yàn)證。函數(shù)式編程是一種編程范型。演算是1930年代在調(diào)查函數(shù)定義、函數(shù)應(yīng)用和遞。函數(shù)式與命令式的比較。表示法的主要特征。true不是良形的表達(dá)式。.M和謂詞演算公式?–x是一個(gè)占位符，約束變?cè)梢灾匦旅?5/*應(yīng)用下頁(yè)介紹的?表達(dá)式的一個(gè)推理系統(tǒng)，下面用。M表示M中自由出現(xiàn)的x用表達(dá)式N代換的結(jié)果。自反公理、對(duì)稱(chēng)性規(guī)則、傳遞性規(guī)則。等式證明規(guī)則允許推導(dǎo)任何一組等式前提的邏。演算的操作語(yǔ)義和指稱(chēng)語(yǔ)義。例1（整型）：輾轉(zhuǎn)相除法求最大公約數(shù)。程序都可以翻譯成類(lèi)型化的?例2（積類(lèi)型）：把分?jǐn)?shù)n/d約分到最簡(jiǎn)分式。例4取二元組的第1元和第2元
【正文】 是中綴的函數(shù)名 */ | (x::xs) @ ys = x :: (xs@ys)。 要證的性質(zhì)是 length(xs@ys) = length(xs) + length(ys) 基本情況 length([ ]@ys) = length ys [@] = 0 + length ys [算術(shù) ] = length [ ] + length ys [length] 成立 函數(shù)式程序的驗(yàn)證 ? 例 11：用結(jié)構(gòu)歸納驗(yàn)證表并置前后的表長(zhǎng)關(guān)系 fun length [ ] = 0 | length(x::xs) = 1 + length xs。 fun [ ] @ ys = ys | (x::xs) @ ys = x :: (xs@ys)。 要證的性質(zhì)是 length(xs@ys) = length(xs) + length(ys) 歸納步驟 length((x::xs)@ys) = length(x::(xs@ys)) [@] = 1 + length(xs@ys) [length] = 1 + length xs + length ys [歸納假設(shè) ] = (1 + length xs) + length ys [結(jié)合律 ] = length(x::xs) + length ys [length] 成立 函數(shù)式程序的驗(yàn)證 ? 良基關(guān)系 – 集合 A的良基關(guān)系是 A上的二元關(guān)系 ?，它具有這樣的性質(zhì)： A上不存在無(wú)窮遞減序列 a0 ? a1 ? a2 ? … ? 例：在自然數(shù)上，如果 j ? i +1， 則 i ? j， 則這個(gè)關(guān)系是一個(gè)良基關(guān)系 ? 良基關(guān)系的一些特點(diǎn) – 良基關(guān)系不一定有傳遞性 – 良基關(guān)系都是非自反的，即對(duì)任何 a?A， a ? a不成立 ；否則會(huì)出現(xiàn) 無(wú)窮遞減序列 a ? a ? a ? … – 每個(gè)非空子集都有一個(gè)極小元 函數(shù)式程序的驗(yàn)證 ? 良基歸納 令 ?是集合 A上的一個(gè)良基關(guān)系， 令 P是 A上的某個(gè)性質(zhì)， 若每當(dāng)所有的 P(b) (b ? a)為真則 P(a)為真，即 ?a.( ?b. (b ? a ? P(b)) ? P(a) ) 那么，對(duì)所有的 a?A， P(a)為真 函數(shù)式程序的驗(yàn)證 ? 例 12：用良基歸納法 ?y. facti(n, p) = fact(n) ? p 其中 fun facti(n, p) = if n = 0 then p else facti(n 1, n ? p)。 fun fact(n) = if n = 0 then 1 else fact(n 1) ? n。 自然數(shù)集合，使用的良基關(guān)系是： 若 i = j – 1，則 i ? j 按良基歸納的概念進(jìn)行證明 函數(shù)式程序的驗(yàn)證 fun facti(n, p) = if n = 0 then p else facti(n 1, n ? p)。 fun fact(n) = if n = 0 then 1 else fact(n 1) ? n。 待證： ?y. facti(n, p) = fact(n) ? p 證明： 若 n=0，則 facti(n, p) = p = 1 ? p = fact(n) ? p 若 n0，則 facti(n, p) = facti(n 1, n ? p) [facti] = fact(n1) ? (n ? p) [歸納假設(shè) ] = (fact(n1) ? n) ? p [結(jié)合律 ] = fact(n) ? p [fact]
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1