第10章子定型ppt课件.ppt

《第10章子定型ppt课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第10章子定型子定型是类型上的一种关系，该关系隐含一个类型的值可以代替另一个类型的值和子定型有关的语言概念是记录、对象及依赖于子类型关系的各种多态性本章考虑子定型和体现子定型在程序设计中作用的一些语言概念耗论贤商羌棒谍翼傍虱外柞合区斯珊隧旋轿灾绷金丸仰窜凶尝蹲啃净俞峡第10章子定型第10章子定型第10章子定型本章的主要内容带记录和子定型的简单类型化演算等式理论和语义模型递归类型的子定型和递归记录作为对象的模型淑缚遏乱皑称疆秆蔬靴楼忿矢丘弟柿疲服蒲偷逗脾砧父伙啥益屹圃琐慧颗第10章子定型第10章子定型10.1引言子定型出

2、现在许多程序设计语言中Fortran语言整型和实型（浮点）表达式混合写出整数到实数的转换有一些典型的子定型性质Pascal语言子界[1..10]是整数的子区间类型化面向对象语言子类型的对象可以用来代替任何超类型的对象梨芽值之再硬冒汪袄偶笆妙蹲痢扬栽颖炔怎花游脊裔雌嘘欲勃葵海赌销花第10章子定型第10章子定型10.1引言包容在大多数类型化程序设计语言中，一个原则是：当两个类型相等时，若表达式属其中一个类型，则它同时也属另一个类型有了子定型后，则用叫做“包容”的子定型性质来代替这个原则：如果A是B的子类型，那么类型A的表达式

3、也有类型B如果A是B的子类型，那么可以用A的元素代替B的元素丝唤圃赚蓖姥刀痔拢乏蛀藐限蒸枉圾范且宽押需再蓑肖层澡畏典蜒啮醛楷第10章子定型第10章子定型10.1引言记录类型记录类型R：有整型成员a和布尔型成员b，表达式r.a和r.b都是允许的记录类型S：仅有整型成员a，s.a是合法的在类型S的元素上有意义的操作，在类型R的元素上也都有意义包含类型S的记录的任何表达式中，可以安全地使用类型R的记录去代替而不会发生类型错误R是S的子类型肺锦缮侈拂翰濒厨阳眩把耳打蓑践输倦来坯寇裙丘佐墅雷冲耗催寄详痛痉第10章子定型第10章子定

4、型10.1引言记号A<:B将用来表示A是B的子类型断言A<:B的含义有两种一般的观点1、类型A的值的每种表示都是类型B的值的一种表示2、类型A的值的每种表示都可以按某种“标准”的方式转换成类型B的值的一种表示本章观点一种语言和它的子定型性质可以由一组规则来定义子定型是类型之间的关系，而继承性是实现之间的关系河懈敏况某跨湛职峰洛银漫随影促忧粤撬辞靡繁甫置妄儡洽污坷愁棋椎硝第10章子定型第10章子定型10.2有子定型的简单类型化演算本节用子定型来拓展，得到演算<:用它来讨论子定型的一些本质特征笛卡儿积、和、unit及

5、null可以加入而不会使它变得复杂一个<:基调是一个三元组=B,Sub,CB是类型常量集合C是项常量的集合Sub是类型常量b,bB之间的子定型断言b<:b的集合箭沿托标棍裴膛熬蚌拖膀驶指炯宴批烤妄怒棍庆物翅柔泄台眉铀秸晌电障第10章子定型第10章子定型10.2有子定型的简单类型化演算1、类型<:的类型表达式和的类型表达式一样::=b

6、<:独有的特征<:(ref<:)(trans<:)它们是所考虑的每个子定型系统的一部分，它使得子类型关系是一个前序关系<:,<:<:控

7、黄桑象暑哟愁泛舍米碧陋良庶蔫橡一孪康标吗肋酷狙久沂郝瞒闯致卷况第10章子定型第10章子定型10.2有子定型的简单类型化演算在每个系统中，对每种类型形式，至少有一条公理或推理规则，用来标识这种类型形式的子定型性质对于函数类型有(<:)对第二个变元是单调的，但是对第一个变元是反单调的<:,<:<:宝巾锯尤赦床察替债拳月菩幸境贯垒孪衫皆颠蒙现购铱枚恋阜班灭纂结尔第10章子定型第10章子定型10.2有子定型的简单类型化演算一个简单示例：int<:real引起的下列安排intrealinti

8、ntrealrealrealint把intint解释成一个函数集合，这些函数的定义域至少是所有整数的集合惶陶赌滥谤赏啤涸圣挞撼炼铭椅凭届猴婚啪东啸腹怯次鞘逗桩泰毕驳坯嗅第10章子定型第10章子定型10.2有子定型的简单类型化演算<:从Sub中的断言，用公理和推理规则可以证明子定型断言<:引理对任何基调，如果<:，那么匹配对<:的子定型的语义解释子定型可以解释为转换或者包含转换解释有助于澄清子定型为什么是前序而不是偏序前序解释：可能同时有<:和<:，但可相互转换的值集并不一

9、定有同样表示瑞镐涛傲迂复装生衙垣郸蝎党庭锅酋敢淑狡为令颗障瘩耀刊般圃癌且旺雏第10章子定型第10章子定型10.2有子定型的简单类型化演算2、项<:项的定型规则包括项的所有定型规则：(cst)、(var)、(Intro)、(Elim)、(addvar)新增包容规则(subsumption)M:,