小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2006年
7期
1285-1288
,共4页
操作语义%类型理论%类型系统%程序验证
操作語義%類型理論%類型繫統%程序驗證
조작어의%류형이론%류형계통%정서험증
类型系统建立在一个小的规则集合基础上,易于实现,可理解性好,且具有计算完全性和足够的表达能力.在类型系统中可以重述推导规则,将其形式化为一些归纳关系,从而直接表示了命令的操作语义.类型理论不仅适合于函数式程序的证明,也是刻画和证明命令式程序的合适的框架.
類型繫統建立在一箇小的規則集閤基礎上,易于實現,可理解性好,且具有計算完全性和足夠的錶達能力.在類型繫統中可以重述推導規則,將其形式化為一些歸納關繫,從而直接錶示瞭命令的操作語義.類型理論不僅適閤于函數式程序的證明,也是刻畫和證明命令式程序的閤適的框架.
류형계통건립재일개소적규칙집합기출상,역우실현,가리해성호,차구유계산완전성화족구적표체능력.재류형계통중가이중술추도규칙,장기형식화위일사귀납관계,종이직접표시료명령적조작어의.류형이론불부괄합우함수식정서적증명,야시각화화증명명령식정서적합괄적광가.
