7-基于契约编程-实践.ppt

DesignbyContract Practice LanguageSupportinC C 和其他语言相比 C C 特别注重效率 因此不受任何程序员控制的运行期内部检查机制如 指针检查 数组下标检查 运行期类型检查等断言的使用 非关键字 assertASSERT assert 用法 assert宏的原型定义在中 其作用是如果它的条件返回错误 则终止程序执行一般在Debug版有效 在Release版不起作用用法 在函数开始处检验传入参数的合法性每个assert最好只检验一个条件不要使用有副作用的语句assert和后面的语句应空一行 以形成逻辑和视觉上的一致感有的地方 assert不能代替条件过滤 例子 doublesqrt doublex assert x 0 pre condition assert fabs y y x eps post conditionreturny ASSERT和VERIFY 在VC环境下一般使用ASSERT和VERIFY在Debug模式下作用基本一致 二者都对表达式的值进行计算 如果值为非0 则什么事也不做 如果值为0 则输出诊断信息 在Release模式下效果完全不一样 ASSERT不计算表达式的值 也不会输出诊断信息 VERIFY计算表达式的值 但不管值为0还是非0都不会输出诊断信息 因为VERIFY 违反了断言的思想 不能使程序代码和调试代码完全分离 最终可能会带来很多麻烦 因此 建议尽量少用不用这个宏 Assert方式的缺点 不能直观地掌握出错地点不能被捕获和重新处理出错时不一定要中止 可能上层调用能够解决如打开文件在Debug版对性能有一定影响 LanguageSupportinJava assertExpression1 assertExpression1 Expression2 语法 Expression2canbeanyprimitivetype 从J2SE1 4之后 Java提供一些断言的支持 使用assert保留字 Expression1musthavetypebooleanoracompile timeerroroccurs enabledordisabled 两种形式的assert e g itcouldserveasauniqueintegercodefortheassertion Semantics Ifassertionsaredisabledinaclass theassertstatementscontainedinthatclasshavenoeffect Ifassertionsareenabled Expression1isevaluated Ifitevaluatestofalse anAssertionErroristhrown IfExpression1evaluatestotrue Expression2isnotevaluated IfExpression2ispresent thenthisisevaluatedandpassedtotheconstructoroftheAssertionError otherwisetheparameterlessconstructorisused assertExpression1 assertExpression1 Expression2 newAssertionError value returnsanassertionerrorthathasthestringrepresentationofthevalueastheerror sdetailmessage Ifanexceptionisthrownwhileeitherexpressionisbeingevaluated theassertstatementcompletesabruptly throwingthisexception Althoughtheassertconstructisnotafull blownDbCfacility itcanhelpsupportaninformalDbCstyleofprogramming Preconditions 按照Java的约定 public方法的前置条件通常通过显式的检查 explicitchecks 来明确 并抛出特定的 明确的异常 exceptions publicvoidsetRefreshRate intrate Enforcespecifiedpreconditioninpublicmethodif rateMAX REFRESH RATE thrownewIllegalArgumentException Illegalrate rate setRefreshInterval 1000 rate 不适合用assert 如 方法应该一直检查异常 不能被屏蔽 assert不能抛出制定的异常 它只能抛出AssertionError assertions可以被disable 对于nonpublic private 方法 使用assert表示前置条件比较合适 privatevoidsetRefreshInterval intinterval Confirmadherencetopreconditioninnonpublic methodassertinterval 0 Settherefreshinterval 如 Postconditions Postconditionsarebestimplementedasasserts whetherornottheyarespecifiedinpublicmethods ReturnsaBigIntegerofvalue this 1modm publicBigIntegermodInverse BigIntegerm if m signum 0 thrownewArithmeticException Modulusnotpositive m if this gcd m equals ONE thrownewArithmeticException this notinvertiblemod m Dothecomputationassertthis multiply result mod m equals ONE returnresult E g ClassInvariants Theassertionmechanismitselfdoesnotenforceanyparticularstylefordoingso Assertsareappropriateforcheckinginternalinvariants Onewayistocombinemanyconstraintchecksintoasingleinternalmethodthatcanthenbeinvokedbyassertions Returnstrueifthistreeisproperlybalancedprivatebooleanbalanced E g supposewewanttoimplementabalancedtreedatastructureofsomesort Thismethodisaclassinvariant Theinvariantshouldalwaysbetruebeforeandafteranymethodcompletes Tocheckthatthisisindeedthecase eachpublicmethodandconstructorshouldcontaintheline assertbalanced immediatelypriortoeachreturn Wecouldimplementaprivatemethodthatcheckedthatthetreewasindeedbalanced Invariants onclassesandonloops areindicatedwiththekeywordinvariant Pre andpost conditionsareindicatedbythekeywordsrequireandensurerespectively e g LanguageSupportin EiffelprovideslanguagesupportforDbC squareRoot x precisionRequired RealNumber RealNumberis requirex 0andprecisionRequired 10e 9 ensureabs answer answer x precisionRequiredend end invariantradius1 radius2 Variouslevelsofcheckingcanberequestedbycompileroptions e g checkall orcheckpreconditionsonly Eiffelevenenforcestheconstraintsonmaintainingthecontractoninheritance e g anoverriddenversionofsquareRootwhichacceptssmallervaluesofprecisionRequiredmighthavetheprecondition requireelseprecisionRequired 10e 15 keywordsrequireelseareusedforpreconditions andortheoriginalandthenewpreconditions keywordsensurethenareusedforpostconditions andandtheoriginalandthenewpostconditions Eiffel的例子 componentCUSTOMER MANAGERcount INTEGERid active an id CUSTOMER ID BOOLEANadd a customer BASIC CUSTOMER DETAILS requireid not already activenotid active a customer id ensurecount increasedcount oldcount 1customer id now activeid active a customer id name for an id CUSTOMER ID STRINGrequireid active id active anid set name an id CUSTOMER ID a name STRING requireid active id active anid ensurename set name for an id is equal a name invariantcount never negative count 0end Effiel运行时检查 Stoppedinobject 0 xE96978 Class CUSTOMER MANAGERFeature addProblem PreconditionviolatedTag id not already activeArguments a customer BASIC CUSTOMER DETAILS 0 xE9697C CallStack CUSTOMER MANAGER addWascalledbyCUSTOMER MANAGER UIFchange customer 提前崩溃原则 尽早在错误点崩溃便于发现错误便于定位错误不回避错误 避免鸵鸟态度前置条件和后置条件处进行检查断言与单元测试 错误和异常 错误Error应该预料到 一般能在调用的上一级解决函数调用返回值检查系统调用状态检查异常Exception不能预料原因如无法打开必须的文件网络传输错误通常无法在本地解决 以至于不能预计会在调用层次的哪一级 直到用户交互 解决严重失效Fault不能预料出现 而且可能在任何地点出现内存溢出外部硬件错误通常无法在程序内解决 异常处理 非结构化异常处理If then就地处理结构化异常处理throwtry catch可以以类的方式定义异常的类别和层次 重新审视DbC 调用者 应用程序等 和被调用者 库函数 组件库等 是平等的 都有权利和义务的说明