函數(shù)式編程語(yǔ)言、編程和程序驗(yàn)證(參考版)
2024-10-23 21:04本頁(yè)面
【正文】 fun fact(n) = if n = 0 then 1 else fact(n 1) ? n。 fun fact(n) = if n = 0 then 1 else fact(n 1) ? n。 fun [ ] ys = ys | (x::xs) ys = x :: (xsys)。 fun [ ] ys = ys /*是中綴的函數(shù)名 */ | (x::xs) ys = x :: (xsys)。 functor F(S : SIG) : SIG = struct type t = ? val x : t = (, ) end 函數(shù)式程序的驗(yàn)證 ? 程序驗(yàn)證就是證明程序具有所期望的性質(zhì)，它是提高軟件可信程度的重要方法 模型檢測(cè) – 通過(guò)遍歷系統(tǒng)所有狀態(tài)空間，能夠?qū)τ懈F狀態(tài)系統(tǒng)進(jìn)行自動(dòng)驗(yàn)證，并自動(dòng)構(gòu)造不滿足驗(yàn)證性質(zhì)的反例 – 問(wèn)題：難以解決狀態(tài)空間爆炸問(wèn)題，不能輸出顯式的證據(jù) 形式程序驗(yàn)證（ formal program verification） – 命令式語(yǔ)言的程序驗(yàn)證起源于 Hoare邏輯 – 函數(shù)式程序驗(yàn)證因不涉及程序狀態(tài)，要簡(jiǎn)單得多 函數(shù)式程序的驗(yàn)證 ? 例 10：用數(shù)學(xué)歸納法驗(yàn)證計(jì)算階乘的函數(shù) fun facti(n, p) = if n = 0 then p else facti(n 1, n * p)。 structure S : SIG = /* 符合上述基調(diào)的一個(gè)結(jié)構(gòu) */ struct type t = int val x : t = 3 end。 val insert = fn : real ? real list real list – 排序需要用到兩個(gè)變?cè)谋容^運(yùn)算，關(guān)系運(yùn)算“ =”不是多態(tài)的，因此 insert不是多態(tài)函數(shù) – 在第 1行上給出函數(shù)的結(jié)果類型就是為了避免類型推斷出現(xiàn)錯(cuò)誤 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 ? 例 7（表類型）基于表的一個(gè)高階函數(shù) fun map f [ ] = [ ] | map f (x :: xs) = (f x) :: map f xs。 val snd = fn : ?a ? ?b ? ?b 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 ? 表的簡(jiǎn)介 – 表（ list）是相同類型元素的有限序列 – 如： [3, 5, 9], [ (1, “one”), (2, “two”), (3, “three”) ] – 表的構(gòu)造符 空表： [ ] 在已有的表前加入一個(gè)元素： :: 9 :: [ ] = [9], 5 :: [9] = [5, 9] – 基本的表函數(shù) null（測(cè)試空表）、 hd（返回表頭元素）、 tl（返回非空表的表尾）、 length（返回表長(zhǎng)） 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 ? 例 5（表類型）計(jì)算表的長(zhǎng)度 fun length [ ] = 0 | length (x :: xs) = 1 + length xs。 其中的 if … then …else 是一個(gè)內(nèi)部定義的多態(tài)函數(shù) if … then …else = fn : bool ? ?a ? ?a ? ?a 其中 a是類型變量，類型變量以撇號(hào)開始 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 ? 例 4（多態(tài)函數(shù)）取二元組的第 1元和第 2元 fun fst(x, y) = x。 age : int。 val gcd = fn : int ? int int /* SML的回應(yīng) */ gcd(13, 78) /*函數(shù)應(yīng)用表達(dá)式 */ 13
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1