函数式编程语言编程和程序验证.ppt

函数式编程语言、编程和程序验证 计计算机科学与技术术学院 陈陈意云 2010.7内 容 提 要学习函数式语言是因为课程实践所用工具中， 需要用函数式风格编程另外，需要对比函数式 程序和命令式程序在程序验证上的区别 • 函数式编程语言概述 • 演算简介 • 函数式语言SML及编程简介 • 函数式语言SML的模块系统• 函数式程序的验证函数式编程语言概述• 函数式编程是一种编程范型 – 它把计算看作是对数学函数的求值，避免了状态和 易变数据结构 – 函数是构造程序的基本成分，语言还提供构造更为 复杂的函数的机制，语言禁止使用赋值语句 – 函数式编程的根基是演算 – 演算是1930年代在调查函数定义、函数应用和递 归时研发的一个形式系统，是等价于图灵机的一种 抽象的计算模型 – 许多函数式编程语言都可看成是在演算基础上精 心制作出的结果函数式编程语言概述• 函数式与命令式的比较 – 函数式编程强调函数应用，而命令式编程风格强调 状态的改变 – 命令式程序的“函数”有副作用，如改变全局变量 – 命令式程序缺乏引用透明性，副作用是其根源 引用透明性：可自由地将（子）表达式替换为它的 值而不改变程序（表达式） – 函数式程序中，函数的结果仅依赖于提供给它的参 数 – 没有副作用使得理解程序和预测程序的行为变得容 易，这是研究函数式语言的一个关键动机函数式编程语言概述• 函数式语言的用途 – 历史上，（纯）函数式语言一直被学术界（而不是 商用软件研发）重视 – 现在，Scheme, OCaml和Haskell等函数式语言已经 出现在工业和商业应用中 – 通过领域专用编程语言，函数式编程有更广阔的天 地，如Mathematica（符号数学）、R（统计）、J 和K（金融分析）– 函数式编程的风格也可用于不是专为函数式编程设 计的语言中，如Javascript融入了函数式编程的功 能，类似的还有Perl语言 演 算 简 介1、表示法 • 表示法的主要特征 – 抽象：用于定义函数 – 应用：将所定义的函数作用于变元 • 抽象的例子 （自然数类型上的几个例子） –恒等函数：x : nat.x // 命令式表示Id(x : nat) = x –后继函数：x : nat.x  1 // 函数式无需给函数命名 –常函数：x : nat.10 – x : nat.x  true 不是良形的表达式 • 表示法写出的表达式叫做表达式或项 演 算 简 介• 项x : .M 和谓词演算公式x : A. 的比较 – 是一个约束算子 – x是一个占位符，约束变元，可以重新命名约束变 元而不改变表达式的含义 – 在x:.x + y中，x的出现是约束的， y的出现是自 由的 –不含自由变元的表达式称为闭表达式 • 应用：用项的并置来表示函数应用，例： – (x : nat.x) 5 – (x : nat.x) 5  5 /*应用下页介绍的公理*/ 演 算 简 介2、演算 演算是关于表达式的一个推理系统，下面用 等式公理系统（公理语义）来描述 • 约束变元改名公理（公理） – x:.M  y:.yxM，M中无自由出现的y – NxM表示M中自由出现的x用表达式N代换的结果 –例如 x:.x  y:.y • 函数应用公理（公理） – (x:.M)N  [N/x]M –例如 (x:nat.x+4) 4  [4/x](x+4)  4 + 4  演 算 简 介• 自反公理、对称性规则、传递性规则 • 同余规则 –相等的函数作用于相等的变元产生相等的结果• 等式证明规则允许推导任何一组等式前提的逻 辑推论还可以定义演算的操作语义和指称语义M1 = M2, N1 = N2M1 N1 = M2 N2 演 算 简 介• 简单例子( x. ( y. z. ( x + y ) + z ) 3 ) 4 5 = ( x. z. ( x + 3 ) + z ) 4 5 = ( z. ( 4 + 3 ) + z ) 5 = ( 4 + 3 ) + 5 = 12 演 算 简 介• 复杂例子：高阶函数应用到函数，得到函数 Curry,  f :  . x:. y:. f x, y add  p:nat  nat. (Proj1 p) + (Proj2 p) Curry(add) = x:nat. y:nat. x + y 演算过程在下页，给Curry加上角标是避免引入多态该例体现函数式语言区别命令式语言的优点– 函数作为编程语言的第一类实体，即对它们的使用 没有限制 – 可以动态地构造新函数 演 算 简 介• 复杂例子：高阶函数应用到函数，得到函数 Curry(add) (f:nat  nat  nat. x:nat. y:nat. f x, y) add= x:nat. y:nat. add x, y x:nat. y:nat. (p:nat  nat. (Proj1 p) +(Proj2 p)) x, y= x:nat. y:nat. Proj1x, y + Proj2 x, y= x:nat. y:nat. x + y函数式语言SML及编程简介使用Standard ML语言，简称SML • 例1（整型）： 辗转相除法求最大公约数 fun gcd(m, n) = /*函数声明表达式 */if m = 0 then nelse gcd(n mod m, m); > val gcd = fn : int  int -> int /* SML的回应 */ gcd(13, 78) /*函数应用表达式*/ > 13 : int程序由一个或多个表达式构成程序都可以翻译成类型化的表达式，在此不介绍SML还有其他基本类型：real, bool, string等函数式语言SML及编程简介• 例2（积类型）：把分数n/d约分到最简分式 fun fraction(n, d) = /*(n, d)是int  int的元素 */let val com = gcd(n, d)in (n div com, d div com) end; > val fraction = fn : int  int -> int  int 引入let后，表达式的一般形式是 let D1 D2 … Dn in E end let 引入的声明相当于命令式语言的局部声明，let声 明可以嵌套，联立的let可用来声明相互递归的函数 使用let可使程序简洁，免去重复计算公共子表达式函数式语言SML及编程简介• 例3（记录类型） type student = { name : string; age : int; score : real } > type student记录是具有标签的元组函数式语言SML及编程简介• 例4（多态类型） fun gcd(m, n) =if m = 0 then nelse gcd(n mod m, m);其中的if … then …else 是一个内部定义的多态函数 if … then …else = fn : bool  a  a  a 其中a是类型变量，类型变量以撇号开始函数式语言SML及编程简介• 例4（多态函数）取二元组的第1元和第2元 fun fst(x, y) = x; > val fst = fn : a  b  afun snd(x, y) = y; > val snd = fn : a  b  b函数式语言SML及编程简介• 表的简介 – 表（list）是相同类型元素的有限序列 – 如：[3, 5, 9], [ (1, “one”), (2, “two”), (3, “three”) ]– 表的构造符 空表：[ ]在已有的表前加入一个元素：:: 9 :: [ ] = [9], 5 :: [9] = [5, 9]– 基本的表函数 null（测试空表）、hd（返回表头元素）、tl（返 回非空表的表尾）、length（返回表长）函数式语言SML及编程简介• 例5（表类型）计算表的长度 fun length [ ] = 0 | length (x :: xs) = 1 + length xs; > val length = fn : a list -> int length [3, 5, 9]length [“one”, “two”, “three”] > 3 : int> 3 : int – 竖线“ | ”将函数声明分成两子句，各处理一个模式 – length是一个多态类型的函数 – list相当于一个类型构造符函数式语言SML及编程简介• 例6（表类型）插入排序 fun insert(x, [ ]) : real list = [ x ] | insert(x, y :: ys) =if x val insert = fn : real  real list -> real list – 排序需要用到两个变元的比较运算，关系运算“ val map = fn : (a -> b) -> (a list -> b list) – 算子map把函数 f 应用到表的每个元素上，即 map f [x1, …, xn] = [f x1, …, f xn] – map f的结果是一个新函数函数式语言SML及编程简介• 例8 静态作用域（静态绑定） let val x = 2fun f y = x + y/* x是函数f的非局部变量*/fun F (g, x) = g 2 in F(f, 1) – 按静态作用域和动态作用域，结果分别为4和3 – f函数所引用的x绑定到2，这样的绑定成为f的环境 – 在计算F(f, 1)时，必须把f和它的环境ef一起传递， 以保证f不管在何处计算都有正确的计算环境 – 二元组(f, ef) 称为闭包，是语言实现中的概念函数式语言SML的模块系统模块化关心的是程序的组织，而不是计算本身，模块 化结构使得程序易于理解、编写和维护等 – SML模块所涉及的主要构造是结构、基调和函子 – 结构：由一组类型、值和结构的声明组成 – 基调：是结构的“类型”或“界面”，规范结构必须包 含的声明 – 函子：从结构到结构的函数 – 类比：（模块化） 结构 ～（核心语言） 值 基调 ～类型 函子 ～函数函数式语言SML的模块系统• 例9：使用模块系统的一个简单例子 signature SIG = /* 描述有类型t和值x的结构类 */ sigtype tval x : t end; structure S : SIG = /* 符合上述基调的一个结构*/ structtype t = intval x : t = 3 end; – 可以用基调来规范结构的部分成员函数式语言SML的模块系统• 例9：使用模块系统的一个简单例子 structure S : SIG = /* 符合上页基调的一个结构*/ structtype t = intval x : t = 3 end; functor F(S : SIG) : SIG = structtype t = S.t  S.tval x : t = (S.x, S.x) end函数式程序的验证• 程序验证就是证明程序具有所期望的性质，它 是提高软件可信程度的重要方法 1、模型检测– 通过遍历系统所有状态空间，能够对有穷状态系统 进行自动验证，并自动构造不满足验证性质的反例 – 问题：难以解决状态空间爆炸问题，不能输出显式 的证据 2、形式。