摘要 当前面向对象领域存在着众多的方法和语言。它们或高举统一建模方法的大旗，在软件开发的高端领域呼风唤雨；或在设计思想上独辟蹊径，拥有一大批狂热的社区信徒；或已经根深蒂固，用户群广泛，尤在吐故纳新，不断吸取众家之长。在这些方法和语言之中，由瑞士理工大学教授、计算机科学家Bertrand Meryer发明的Eiffel语言被誉为是最纯粹、理论性最强的面向对象语言，而Eiffel方法以严格而有灵活的Design By Contract™作为理论核心，提出了很多独特的基本思想和解决问题的思路。特别是在Eiffel中强调了对形式化方法的研究和运用。它山之石可以工玉。本文旨在对Eiffel方法、语言、开发环境进行概要的介绍，然后通过实例对Eiffel中形式化的运用——Design By Contract™作较深入的介绍，最后提出自己的一点浅见。
第一节 背景和历史
1986年10月，Eiffel 1在OOPSLA（Object-Oriented Programming Systems Language and Applications）大会上一举成名，由此踏上了商业化之路。随后几年中，Eiffel在美国、加拿大、欧洲和远东地区迅速传播，实施了一系列成功的工程项目。同时，学术界也认为Eiffel是教授各种软件概念的理想途径，世界上很多大学都已经采用Eiffel作为主要的教学语言。
1988年，Bertrand Meryer出版了《Object-Oriented Software Construction》，书中介绍了对象技术的概念和Design By Contract™，并用Eiffel作为描述语言进行了讲解。这本经典著作被称为“面向对象软件开发圣经”，极大地促进了人们对Eiffel的认可。
第二节 Eiffel的理论基础、语言特点和主要技术
Eiffel广义上被称为The Eiffel Development Framework™，该框架提供了一整套软件开发方法，包括以下三部分：一套贯穿构建健壮、可重用软件始终的方法学；Eiffel语言（无缝地支持和加强方法学）、一个称为EiffelStudio™的集成开发环境（包含Eiffel语言和一套提高开发效率和质量的工具集）。
Eiffel并不盲从于提高生产率，而是专注于质量，它认为“When quality is pursued，productivity follows”（K.Fujino in NEC）。Eiffel中的“质量”由五种因素组成：可靠性（Reliability）、重用性（Reusability）、扩展性（Extendibility）、移植性（Portability）、维护性（Maintainability）。Eiffel希望使它的可重用库像硬件、操作系统、编译器一样，成为人们充分信任的高可靠部件之一。
1． 理论基础
Design By Contract™
Design By Contract™（DBC，按契约设计）几乎是Eiffel方法的标志。对于DBC的直接支持是Eiffel最著名的特性。Bertrand Meyer以数学形式严格证明了DBC的合理性，并且通过require/ensure/invariant建立了严格而有灵活的契约体系。DBC理论和机制在软件开发的分析、设计、文档、调试、测试甚至项目管理中都扮演着关键角色，这使得Eiffel历来以长于开发高质量软件而著称。
DBC来源于对人类生活中契约的理解。
DBC认为软件系统是由许多相互交流的组件构造的，这些组件在交流时应该遵守彼此共有的约定（权利和义务），这些规约应该被精确定义。断言就是很好的规约表达工具。
假设要实现根据键值在表中插入元素。契约如下：
断言是DBC的核心。断言（assertion）是一个布尔陈述。除了有错情况，它恒有真；在有错时，它才为假。Eiffel只在调试/测试时才查核断言，在日常运行时不查核断言。
DBC使用了多种责任断言：后置断言（postcondition）、前置断言（precondition）、不变式（invariant）、变式、状态接受条件和状态结果条件。其中后置断言、前置断言和不变式是最主要的。这些断言只是用来捕获各种操作的语义，并不牵涉具体实现。
后置断言和前置断言用于操作。后置断言是操作执行后“事情就该如此”的描述，它区分了接口和实现。前置断言是在操作执行前，对“事情预备状态”的描述。DBC通过断言明确了调用者和服务者的职责（调用者负责前置断言的测试，服务者保证后置断言的实现），避免了核查过少或核查过多。在核查（排错和测试）时，若执行操作，其前置断言满足，后置断言不满足，则发生异常（exception）。
不变式是关于类的断言，是加在和类的所有公共操作相关的前后置断言上的。类的不变式描述了关于类的深层性质，即不变式所提供的约束适用于类的整个后续演进中。在方法执行中，不变式可以为假，但在其它对象调用它时应恢复为真。Eiffel中的不变式包括类不变式（class invariant）、循环不变式（loop invariant）和状态不变式。Meyer认为“只有当产生了不变式（所写的类）或理解了它，才能感觉到这个类的含义”。
Eiffel根据Dijkstra的“气球原理”使用断言——弱化前置断言或强化后置断言，有效地防止了子类构作时多态性可能引入的危险，确保了子类运行正常。
Eiffel认为用断言对软件进行证明的技术还不成熟，因此，它将断言应用到调试/测试中，来得到更可靠的质量保证。
但是Eiffel中并不提倡采用完全形式化规约。Eiffel认为尽管形式化规约很有吸引力，但全面引入形式化规约会造成语言不可执行，或即使能执行，也只能用于原型中。因此，Eiffel在语言中有选择地部分引入了形式化规约，从而使规约语言能嵌入到设计和编程语言中，运用到实际的商业开发中。
DBC并非Eiffel专用，它是一种可用于任何编程语言的重要技术。由于Bertrand Meyer参与了Microsoft公司VisualStudio.NET的设计，因此VisualStudio.NET也具有了DBC的特性。
无缝性和可逆性（Seamlessness & Reversibility）
Eiffel方法的一个美妙之处在于，它弥合了分析、设计和编程之间的差异，在全过程应用相同的工具和理念。也就是说，在项目之初，用Eiffel的精确、清晰和表达能力，高度抽象地进行分析和设计。在系统具体构造时，同样使用Eiffel进行实现和迭代。这被称为无缝性和可逆性，也称“单模型原则”。
这与当前主流的建模思想有所不同。目前流行的思想在分析、设计和实现之间使用了不同的表示法和工具——先用基于UML的CASE工具，再用编程语言环境。
Bertrand Meyer反对这种“人为地区分高贵的分析工作和粗鄙的编程工作”的思想。他认为，借鉴程序设计天然之优美、精致和理性力量，将其运用在设计和建模工具之中，运用在调整和扩展现有成果的工具之中，运用在最终的思考工具中。
Eiffel推崇一种叫做BON（Business Object Notation）的建模技术，提倡从建模、分析、设计到编程，统一使用Eiffel作为表达思想的工具，从而达到各个过程之间的无缝性。它的关键概念包括无缝性（Seamlessness）、可逆性（Reversibility）和契约性（Software contracting）。BON由Dr. Nerson（SOL in Paris）和Dr. Waldén（Enea Data in Stockholm）发明。它定义了一些简单的、直觉化图形的规则，在描述一个庞大而复杂的系统时，能让开发者在深入到组件内部细节时仍能在不同的抽象层次上把握住整体。
2． 语言特点
Eiffel提供了许多其它语言所不具备的特点：简洁的语法、可重用性、天生的Design By Contract™、支持整个软件生命周期、保证工程按期完成并提高各个开发阶段的生产率。
层次化的语言描述
Eiffel仔细区分了语言描述的三个层次：语法、有效性、语义。语法是最低层次，有效性是中间层次，语义是最高层次。高层次语言描述是应用在低层次语言描述上的。每个层次都提供了丰富的规则进行约束。在实现上，语法和有效性由编译器保证，语义则依赖于契约检查和调试工具。
一致的类型系统
Eiffel中所有的类型都是基于class的。从而被纳入到Eiffel整体类型体系中，因此，Eiffel与Smalltalk一样，都是最纯的面向对象语言。
丰富简洁的关键字
Eiffel中有五种关键字。类结构关键字（Class structure keywords），包括indexing、class、inherit、creation、feature等。特征结构关键字（Feature structure keywords），包括is、require、require else、local、do、once、defered、external、rescue、ensure、ensure then、alias等。控制结构关键字（Control structure keywords），包括if、then、elseif、else、inspect、when、from、variant、until、loop、debug、check等。继承子句关键字（Inherit structure keywords），包括rename、redefine、undefine、select、export等。其它关键字，包括precursor、create、obsolete、invariant、end等。Eiffel对关键字和语法结构力求简约，表达一种概念尽量只用一种结构，以免混淆开发者。这也便利了调试时的错误定位。
以下是Eiffel