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

函数式编程语言、、编程和程序验证函数式编程语言、编程和程序验证内容提要学****函数式语言是因为课程实践所用工具中,需要用函数式风格编程。另外,需要对比函数式程序和命令式程序在程序验证上的区别函数式编程语言概述演算简介函数式语言SML及编程简介函数式语言SML的模块系统函数式程序的验证柠归煌***噬歇款榨恬豢瘩柿屉甘汇池擅郑住狱洁毒迄嘘躲革破限减残磺甥函数式编程语言、编程和程序验证函数式编程语言、编程和程序验证函数式编程语言概述函数式编程是一种编程范型它把计算看作是对数学函数的求值,避免了状态和易变数据结构函数是构造程序的基本成分,语言还提供构造更为复杂的函数的机制,语言禁止使用赋值语句函数式编程的根基是演算演算是1930年代在调查函数定义、函数应用和递归时研发的一个形式系统,是等价于图灵机的一种抽象的计算模型许多函数式编程语言都可看成是在演算基础上精心制作出的结果椒拢吟层志兹汤翔秩回霉岸墙台张锁安捉码辗尚腋懒贮尘篷郸搂阜琳羹沃函数式编程语言、编程和程序验证函数式编程语言、编程和程序验证函数式编程语言概述函数式与命令式的比较函数式编程强调函数应用,而命令式编程风格强调状态的改变命令式程序的“函数”有副作用,如改变全局变量命令式程序缺乏引用透明性,副作用是其根源 引用透明性:可自由地将(子)表达式替换为它的值而不改变程序(表达式)函数式程序中,函数的结果仅依赖于提供给它的参数没有副作用使得理解程序和预测程序的行为变得容易,这是研究函数式语言的一个关键动机去姥疚槐盲正筷蟹界棕绎消迢炊矫鞭途擅丈融傲京次松链杆爱剃禾纤喀熏函数式编程语言、编程和程序验证函数式编程语言、编程和程序验证函数式编程语言概述函数式语言的用途历史上,(纯)函数式语言一直被学术界(而不是商用软件研发)重视现在,Scheme,OCaml和Haskell等函数式语言已经出现在工业和商业应用中通过领域专用编程语言,函数式编程有更广阔的天地,如Mathematica(符号数学)、R(统计)、J和K(金融分析)函数式编程的风格也可用于不是专为函数式编程设计的语言中,如Javascript融入了函数式编程的功能,类似的还有Perl语言谆酣凳荐得妊骡逊灌协敦韶瑞刺砂果母愁官积约驾挪颊日搞衡智兽陆金狐函数式编程语言、编程和程序验证函数式编程语言、编程和程序验证演算简介1、表示法表示法的主要特征抽象:用于定义函数应用:将所定义的函数作用于变元抽象的例子(自然数类型上的几个例子)恒等函数:x://命令式表示Id(x:nat)=x后继函数:x:1//函数式无需给函数命名常函数:x:x:true不是良形的表达式表示法写出的表达式叫做表达式或项递状龋佰款跪骸睬耪穴找添会吨谍师袄聂法重瀑缴漏缔圈侮撞壁毡征疑闷函数式编程语言、编程和程序验证函数式编程语言、编程和程序验证演算简介项x:.M和谓词演算公式x:A.的比较是一个约束算子x是一个占位符,约束变元,可以重新命名约束变元而不改变表达式的含义在x:.x+y中,x的出现是约束的,y的出现是自由的不含自由变元的表达式称为闭表达式应用:用项的并置来表示函数应用,例:(x:)5(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:+4)4[4/x](x+4)4+4那购宝樟疽郭司囤眉菲逝舌晰返普馆字构廉***悉柞范入遥戴镑袁沃抹义想函数式编程语言、编程和程序验证函数式编程语言、编程和程序验证演算简介自反公理、对称性规则、传递性规则同余规则相等的函数作用于相等的变元产生相等的结果等式证明规则允许推导任何一组等式前提的逻辑推论还可以定义演算的操作语义和指称语义M1=M2,N1=N2M1N1=M2N2回蜘初读嗜熔库糜狡居辆骚霜聂稍鸳撼授貉厅诣贺冀挺滁屯糠近蒸例炕态函数式编程语言、编程和程序验证函数式编程语言、编程和程序验证演算简介简单例子(x.(y.z.(x+y)+z)3)45=(x.z.(x+3)+z)45=(z.(4+3)+z)5=(4+3)+5=12挠境