Spec#语言中的形式化特性
作者单位：中国科学院软件研究所 中国科学院软件研究所 中国科学院软件研究所
会议名称：《2005年全国理论计算机科学学术年会》
会议日期：2005年
学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家自然科学基金项目(60273092) 科技部973重大基础研究前期专项(2003CCA02800)
关 键 词：Formal methods Contracts Exception Object invariants
摘 要：正 1 引言Spec#是Microsoft正在研发的一种程序设计语言,其意图是为面向对象的语言引入形式化机制,从而使软件的可靠性和可维护性水平产生一个质的飞跃。其主要特性包括基于前置和后置条件的方法契约、基于对象不变式的类契约、增强的异常处理机制等。Spec#语言的出现将对软件形式化方法研究产生重要影响。本文从形式化方法的基础——程序正确性的概念出发,分析了Spec#语言中的形式化机制,简要