Eiffel初探（基于合約的程式設計方式）

摘要

      目前面向對象領域存在着衆多的方法和語言。它們或高舉統一模組化方法的大旗，在軟體開發的高端領域呼風喚雨；或在設計思想上獨辟蹊徑，擁有一大批狂熱的社群信徒；或已經根深蒂固，使用者群廣泛，尤在吐故納新，不斷吸取衆家之長。在這些方法和語言之中，由瑞士理工大學教授、計算機科學家Bertrand Meryer發明的Eiffel語言被譽為是最純粹、理論性最強的面向對象語言，而Eiffel方法以嚴格而有靈活的Design By Contract™作為理論核心，提出了很多獨特的基本思想和解決問題的思路。特别是在Eiffel中強調了對形式化方法的研究和運用。它山之石可以工玉。本文旨在對Eiffel方法、語言、開發環境進行概要的介紹，然後通過執行個體對Eiffel中形式化的運用——Design By Contract™作較深入的介紹，最後提出自己的一點淺見。

關鍵字

Eiffel，Bertrand Meyer，Design By Contract™，EiffelStudio™

正文 第一節 背景和曆史

          Eiffel是由Eiffiel公司（現在被稱為ISE—Interactive Software Engineering）在1985年設計的。最初ISE在項目開發中，需要一種能展現現代軟體工程學思想、現代的、面向對象的開發環境，但ISE認為當時沒有這樣的工具。是以，ISE開發了Eiffel作為開發産品的内部工具。Eiffel的名字來自工程師Gastave Eiffel，他為1889年世界博覽會設計了著名的艾菲爾鐵塔，并在計劃的工期和預算内完成了這個工程。ISE希望用Eiffel所建構的軟體工程項目也能達到這樣的目标。

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的63個保留字。

Eiffel類的基本結構如下：

class <class declaration>

feature

        <routine interface declaration> is

        require <precondition predicate>

        local <local declaration>

              do <routine body>

        ensure <postcondition predicate>

        rescue <exception expression>

        end

feature

        ---

invariant <invariant predicate>

end

靜态編譯型語言

通常純粹的面向對象語言，有的是動态語言（如Smalltalk），有的運作在虛拟機上（如Java和C#），而Eiffel是極少數的幾個直接運作在硬體上的靜态編譯型純面向對象語言。Eiffel編譯器一般産生ANSI C代碼，是以理論上可以在任何平台上運作。

斷言

Eiffel語言中引入了斷言（Assertion），這從根本上改變了軟體開發的本質：

其一，使用Design By Contract™作為輔助設計工具，你可以在建立軟體的同時，加入驗證正确性的參數，有助于生産bug-free軟體。

其二，使用Eiffel編譯器作為測試和調試工具，開發者可以選擇在運作時要監視的斷言。開發者可以分别為每個類設定不同的監視級别（不檢查、隻檢查前置斷言、檢查前置斷言和後置斷言、檢查全部）。如果在運作時發現某個斷言不成立，則意味着存在Bug，這時就會抛出異常中斷運作。這不僅增強了測試和調試的針對性，而且有軟體應作什麼（斷言）和作了什麼（do子句中的可執行部分）的精确描述，是以能使軟體盡快調試到正确狀态。

其三，Eiffel類的簡短形式可以作為文檔自動化的實作基礎，包含類的特性頭、注釋和斷言。斷言中提供了類功能的精确描述而不涉及實作細節。

異常處理（ Exception handling ）

異常處理的目的不是系統的正确性，而在于保持系統的強壯性。Eiffel認為，成功是指能夠履行契約，即使經過了多次重試；失敗是指調用時總是觸發異常。Eiffel為異常處理提供了關鍵字rescue、retry。

泛型（ Genericity ）

泛型是支援類型參數化的類模闆。在面向對象社群，這些類被稱為泛型類。在設計時，這些類使用泛型參數。隻有在運作時，委托類使用它時，才用真正的參數替換泛型參數。這種技術對容器類（如數組和連結清單）特别有用。

針對“泛型純屬多餘”和“泛型先于（Ada）/平行于（C++）面向對象”的看法，Bertrand Meyer認為泛型是對象技術的自然擴充和必要補充。既不能對泛型嗤之以鼻，也不能讓泛型喧賓奪主，掩蓋了面向對象的光芒，破壞語言的一緻性。

在Eiffel中提供了對泛型的支援。

多重繼承（ Multiple Inheritance ）和重複繼承（ Repeated Inheritance ）

多重繼承，又稱為the “Holy Grail” of OO programming，是指一個程式單元可以同時繼承多個其它類的特性。多重繼承的好處很多，它有助于改善重用，優化整個系統結構設計，更加靈活，維護和調試也更加友善。不少面向對象流派都在警告開發者“警惕多重繼承”。但在Eiffel中，多重繼承是面向對象密不可分的特性之一。Paul Dubois認為“别人沒有做好的，Eiffel做好了的事有兩件：支援Design By Contract和多繼承”。Eiffel通過重命名等巧妙的技術，消除了命名沖突，并使用了一個選擇工具來消除因重複聲明而導緻的二義性。

重複繼承是指一個類通過兩個以上路徑繼承到同一祖先類。它的難點在于子孫類如何對待祖先類的特性，是作為一個特性還是作為多個特性來繼承。許多面向對象語言視重複繼承為“死亡菱形”，不敢越雷池一步。Eiffel對重複繼承的特性，明确規定了哪些特性需要共享，哪些特性需要複制，進而靈活地繞過了這塊暗礁。

一般來說，Eiffel中的繼承必須遵守以下的規則：

規則一，Type Conformance rule。在指派語句中的x:=y，或在函數調用中對應形參x的實參y，y的類型都必須和x的類型一緻。

規則二，Final Name rule。同一個類中的兩個不同特性不能擁有同樣的終結名。

規則三，Invariant Accumulation rule。一個類的所有父類的不變式都需應用于類自身。

規則四，Assertion Redeclaration rule。對過程重聲明時，不允許再使用require和ensure。在前置斷言改用require else表示增加析取分量，在後置斷言改用ensure then表示增加合取分量。

規則五，Repeated Inheritance rule。以同一名稱被多次繼承的特性采用共享方式，在子類中被認為是一個特性；以不同名稱被多次繼承的特性采用複制方式，在子類中被認為是多個特性。

規則六，Covariance rule。在特性重聲明中，不論是函數傳回的結果類型，還是過程的參數類型，都必須和原特性的類型一緻。

代理（ Agent ）

在對象技術發展之初，就嚴格區分了對象和操作，每一個操作都是和類聯系在一起的。但在一些應用中，需要用對象來表達操作，比如“操作復原”。是以提出了代理，也稱“操作包裝”。Eiffel中提供了對代理的支援。

多線程和分布式開發（ Multithreading & Distribution ）

在Eiffel中，把每個計算單元看作一個Processor。Processor可以是一台計算機、一個程序或一個線程。通過這種思路就把多線程開發、Client/Server開發、分布式開發統一到了一起。

Eiffel在聲明類執行個體時，加上separate關鍵字，就為該執行個體配置設定了一個Processor，支援并發/并行操作。在實作中，通過配置CCF（Concurrency Configuration File）來決定Processor資源的實際配置設定。

同時，Eiffel也為同步和競争機制提供了獨特的政策。例如，為了處理多線程的資源競争，Eiffel明确劃分了query和command。

EiffelNet和EiffelThread類庫就既可以用于嵌入式開發，又可以用于大型分布式系統開發。

垃圾收集（ Garbage Collection ）

盡管GC往往被認為是一種具體技術，但Eiffel對其給予了相當的關注。Bertrand Meyer認為，單獨的GC線程隻有在得到硬體支援之後才是可行的。在Eiffel中為每一個線程配置設定一個獨立的GC（這給多線程程式的并行性能和效率帶來了很大的改進），并可以控制GC的立刻運作、部分運作、暫停和完全禁止。

一緻的編碼風格

Eiffel認為，作為工業級語言，編碼風格應當作為語言規範規定下來，而不應該任由個人肆意發揮。是以，Eiffel編譯器對于辨別符大小寫、下劃線格式等進行了嚴格的檢查，甚至連注釋都作檢查。這種近乎嚴苛的規則，使得世界上幾乎所有Eiffel程式員寫出來的Eiffel程式都像是一個模子裡出來的。

不支援的特性

Eiffel為了完整準确地表達“品質至上”的設計開發理念，舍棄了一些設計概念。如全局變量、union類型、類内重載（in-class overloading）、goto及類似的控制結構（break、exit等）、類型規則特例（exceptions to the type rules）、副作用表達運算符、底層指針和指針算法等。

3．  開發平台和主要技術 IDE

Eiffel的主要技術主要展現在專為Eiffel面向對象語言設計的內建開發環境EiffelStudio™中。EiffelStudio™是一個完全的圖形環境，包含了有回溯功能的分析設計平台、快速重編譯、編輯、浏覽工具、自動生成文檔、先進的調試機制等衆多功能。整個IDE的設計都展現了Eiffel對開發環境建構的獨特見解。

Eiffel本身就是用Eiffel語言開發的。目前最新的EiffelStudio™版本是ISE Eiffel 5。下面是EiffeStudio5.2 Free Version的界面。

其産品族包括EiffelStudio for Windows、EiffelStudio for Unix、EiffelStudio for Linux、EiffelStudio for VMS等，EiffelStudio for MacOS也正在開發中。這極大地提高了Eiffel代碼在各種作業系統平台上的可移植性。

類庫

類的容易重用和通過繼承友善地定制是面向對象技術最吸引人的地方。是以，每一個程式語言設計者都希望能提供豐富可靠的類庫，“使開發者不再需要重新設計輪子”，進而為開發組織節省大量的時間和金錢。Eiffel擁有龐大而高品質的類庫資源。Meyer在《Eiffel：The Language》一書中定義的EiffelBase庫是所有Eiffel實作都提供的高品質标準庫，包括了語言核心、作業系統功能、記憶體管理、事件機制、容器、算法等元件。同時，ISE還提供了網絡通信庫EiffelNet（通過sockets傳送對象）、編譯器開發EiffelLex和EiffelParse（支援詞法分析和句法分析）、線程庫EiffelThread（映射到C線程标準庫）、Web開發庫EiffelWeb（支援CGI—Common Gateway Interface技術，使Eiffel能直接和WEB互動）、資料庫通路庫EiffelStore（支援各種對象—關系接口，能映射到ODBC、Oracle、Sybase和Ingres等關系資料庫；也提供了到Matisse、Versant和O2等面向對象資料庫的接口）、GUI庫WEL（Windows Eiffel Library，針對Windows平台的圖形庫，包含幾乎所有的Windows圖形API）、GEL（GTK Eiffel Library，針對Unix、Linux和VMS平台）和EiffelVision2（為移植開發而設計的進階圖形庫，包括使用者界面元件和各種幾何圖形，可運作于Eiffel支援的所有平台）、COM元件庫EiffelCOM（封裝了标準COM資料類型）、時間日期庫EiffelTime（基于三種時間概念：絕對時間、始末時間、持續時間）、Java接口庫Eiffel2Java（使Eiffel能調用Java例程和特性。）。

調試和測試

斷言是Eiffel中調試和測試的重要組成部分，是一種簡單而有效的将自檢代碼嵌入實作的方式，它可以避免和揭示錯誤。

斷言提供了對與繼承相關概念的控制，例如重命名、多态、動态綁定，使它們能根據合适的語義限制進行正常地使用。

開啟斷言檢查時，自動計算不變式的時機是：

1．完成對象執行個體化之後

2．在routine的入口，且在檢查前置條件之前

3．檢查後置條件之後，且出去之前

模組化圖形表示法

EiffelStudio™中的Diagram Tool分析設計平台直接支援BON（Business Object Notation），能在系統設計時自動生成BON圖，以便進行整體規劃和互動設計。

文檔自動化

Eiffel中的文檔由直接來自開發環境的，一般由類名、斷言、注釋等類描述組成，是以抽象而又精确。Eiffel支援以下的文檔格式：ASCII、eiffel、MML、postscript、COM、RTF、TeX1、TeX2、troff、html-classic、html-stylesheet，并且通過EFF（Eiffel Filter Format）能夠定義新的文檔格式。

Metric 統計

對軟體工程實踐來說，統計資料的積累和分析是過程持續改進的必要前提。Eiffel能夠對項目産品及其運作狀态進行數字化記錄。開發者可以直接擷取預定義的原始值（如類數目、特征數目等），也可以根據原始值來手工定義新的組合值（如每個類中平均的特征數等）。

融冰技術（ Melting Ice Technology ）

随着大型複雜軟體系統在其生命周期中增量疊代開發的需求日益突出（微軟甚至提出了“日建構（Daily Build）”的概念），這就要求開發工具能夠迅速适應軟體系統的重構和更新。Eiffel為适應這種形勢，提出了四種編譯模式：Melt（快速增量編譯，不優化變化代碼）、Freeze（增量編譯，優化變化代碼）、Finalize（全面編譯，高度優化）、Precompile（預編譯項目重用庫）。其中的關鍵技術是融冰技術。

融冰技術是Eiffel獨特的增量編譯理念——對變化系統重編譯的時間應決定于系統中變化的影響範圍，而不應決定于系統的整個規模——的技術實作。它把編譯（生成優化的代碼）和位元組碼解釋（快速響應變化）結合在一起。在這裡，Eiffel程式分為兩部分，包括預編譯庫（處于“當機”狀态），和剛剛改變的（處于“融解”狀态，即編譯器快速生成了一些可執行的位元組碼，然後停下來），在需要時兩者能互相調用。

與其它設計開發語言和平台的協作

Eiffel語言保留了一個開發的架構，可以和UML-CASE工具、C/C++、Java、COM元件、.NET元件協同合作。

與UML-CASE工具的協作。EiffelStudio™能為任何Eiffel系統生成XMI（XML Metadata Interchange）資訊。XMI符号能在任何支援其标準的不同産品（如Rational Rose）間交換系統資訊。是以，Eiffel生成的XMI能被導入支援XMI的UML-CASE産品中，得到UML資訊。

與C/C++及其編譯器的協作。在C/C++方面，Eiffel有一個精妙的接口，它支援：Eiffel調用C函數、C++類及其成員；通過Cecil（C-Eiffel Call-In Library）庫，C/C++能使用Eiffel的機制；将C++類轉化成Eiffel類的“包裝器”。在編譯器方面，Eiffel編譯器先生成的是位元組碼（這些位元組碼能被直接解釋執行），其後位元組碼被優化并被翻譯成C，最後利用各個平台上的C編譯器進一步優化編譯成可執行碼。

與Java的協作。通過JDK（Java Development Kit）提供的JNI（Java Native Interface），Eiffel能調用Java例程和特性。

與COM元件的協作。Eiffel對标準COM資料類型進行了包裝，形成了EiffelCOM類。

與.NET元件的協作。Eiffel for .NET編寫的代碼被自動編譯成.NET中間語言（IL），是以與Visual Studio.NET完全內建，能和其它任何.NET語言協同工作、共享代碼，并在.NET中支援多重繼承。

第三節   應用執行個體

以下是兩個執行個體。第一個是List類的實作，引自EiffelBase的base.structures.list。第二個是經典範例“Hello World”的實作。

1．List

indexing

       description:

              "Sequential lists, without commitment to a particular representation"

       status: "See notice at end of class"

       names: list, sequence;

       access: index, cursor, membership;

       contents: generic;

       date: "$Date: 2002/01/07 23:04:29 $"

       revision: "$Revision: 1.16 $"

deferred class LIST [G] inherit

       CHAIN [G]

              export

                     {ANY} remove

              redefine

                     forth, is_equal

              end

feature -- Comparison

       is_equal (other: like Current): BOOLEAN is

                     -- Does `other' contain the same elements?

              local

                     c1, c2: CURSOR

              do

                     if Current = other then

                            Result := True

                     else

                            Result := (is_empty = other.is_empty) and

                                          (object_comparison = other.object_comparison)

                            if Result and not is_empty then

                                   c1 ?= cursor

                                   c2 ?= other.cursor

                                   check

                                          cursors_exist: c1 /= Void and c2 /= Void

                                                 -- Because every list contains a cursor object

                                   end

                                   from

                                          start

                                          other.start

                                   until

                                          after or not Result

                                   loop

                                          if object_comparison then

                                                 Result := equal (item, other.item)

                                          else

                                                 Result := (item = other.item)

                                          end

                                          forth

                                          other.forth

                                   end

                                   go_to (c1)

                                   other.go_to (c2)

                            elseif is_empty and other.is_empty and

                                   object_comparison = other.object_comparison then

                                   Result := True

                            end

                     end

              ensure then

                     indices_unchanged:

                            index = old index and other.index = old other.index

                     true_implies_same_size: Result implies count = other.count

              end

feature -- Status report

       after: BOOLEAN is

                     -- Is there no valid cursor position to the right of cursor?

              do

                     Result := (index = count + 1)

              end

       before: BOOLEAN is

                     -- Is there no valid cursor position to the left of cursor?

              do

                     Result := (index = 0)

              end

feature -- Cursor movement

       forth is

                     -- Move to next position; if no next position,

                     -- ensure that `exhausted' will be true.

              deferred

              ensure then

                     moved_forth: index = old index + 1

              end

invariant

       before_definition: before = (index = 0)

       after_definition: after = (index = count + 1)

indexing

       library: "[

                     EiffelBase: Library of reusable components for Eiffel.

                     ]"

       status: "[

                     Copyright 1986-2001 Interactive Software Engineering (ISE).

                     For ISE customers the original versions are an ISE product

                     covered by the ISE Eiffel license and support agreements.

                     ]"

       license: "[

                     EiffelBase may now be used by anyone as FREE SOFTWARE to

                     develop any product, public-domain or commercial, without

                     payment to ISE, under the terms of the ISE Free Eiffel Library

                     License (IFELL) at http://eiffel.com/products/base/license.html.

                     ]"

       source: "[

                     Interactive Software Engineering Inc.

                     ISE Building

                     360 Storke Road, Goleta, CA 93117 USA

                     Telephone [phone], Fax [phone]

                     Electronic mail <[email protected]>

                     Customer support http://support.eiffel.com

                     ]"

       info: "[

                     For latest info see award-winning pages: http://eiffel.com

                     ]"

end -- class LIST

2．Hello World

indexing

       description      : "display hello"

       note        : "Initial version automatically generated"

class

       ROOT_HELLO

creation

       make

feature -- Initialization

       make is

                     -- Creation procedure.

              do

                     --| Add your code here

                     io.put_string (" Hello World ")

               io.new_line

              end

end -- class ROOT_HELLO

第四節   目前發展的現狀

Eiffel語言目前主要研究的領域包括以下兩方面。其一，并行和分布式開發（Concurrency & Distribution）；其二，對斷言集的拓展。

Eiffel的開源社群也十分活躍。ISE之外的GOBO就是Eiffel社群中一套著名的開源跨平台類庫。

Eiffel目前涉及的領域包括金融機構、機械制造、政府機關、保安部門、醫療保健機構等等。HP、Boeing、ENEA、Chicago Board of Trade、Lockheed Martin、Environmental Protection Agency等都是ISE的客戶。

第五節   總結與評論—— No Silver Bullet

在Eiffel中運用了面向對象、圖形化程式設計、程式驗證、環境工具等技術思想，Frederick Brooks認為這些技術思想都無法解決軟體系統“概念上的複雜性”，因而不能根本上解決軟體危機。對于重用的思想，Brooks認為是解決軟體根本困難的一種方法，但目前重用的形式和變化仍然不能令人滿意。

Robert V. Binder認為，Meyer的DBC模型未考慮順序限制（sequential constraints），雖然這對非模态類不是問題，但給模态類留下了明顯的缺口。

根據我們目前對Eiffel的使用，發現了以下問題：

1．編譯後的可執行檔案龐大。一個“Hello World”的console程式有2290K。

參考文獻

1．ISE。Eiffel FAQ。

2．ISE。An Eiffel Tutorial。Eiffel Developer Help Center。

3．ISE。EiffelStudio：A Guided Tour。Eiffel Developer Help Center。

4．ISE。Building bug-free O-O software：An introduction to Design by Contract™。

5．ISE。The BON：The analysis and design method。

6．ISE。Multithreading, Distribution, Internet programming。

7．InformIT。Bertrand Meyer——The Founder Of The Eiffel Language。Programmer2003.02。

8．Martin Fowler、Kendall Scott。UML Distilled 2rd Edtion。Addison Wesley 2000。

9．  Robert V. Binder。Testing Object-Oriented System:Models,Patterns,and Tools。Addison Wesley 2000。

10．    Frederick Brooks。The Mythical Man-Month：The Essays on Software Engineering。Addison Wesley 1995。