计算机科学 ›› 2016, Vol. 43 ›› Issue (Z6): 457-460.doi: 10.11896/j.issn.1002-137X.2016.6A.108
王伟,丁二玉,骆斌
WANG Wei, DING Eryu and LUO Bin
摘要: 为独立方法定义严谨的规格可以保证程序的正确性。但是在面向对象的程序中,方法之间因为共享属性而相互影响,这就需要能够反映方法间影响的规格化方法。研究者们使用抽象变量、状态抽象、堆、查询等多种方法进行了尝试。文中给出一种基于抽象状态的类的行为规格方法,该方法基于抽象状态解决了类方法间的共享依赖和相互影响,同时实现了规格与实现的独立描述与运行时自动化验证。
[1] Hoare C A R.An Axiomatic Basis for Computer Programming[J].Communications of the ACM,1959,2(10):576-580 [2] Guttag J V,Horowitz E,Musser D R.Abstract Data Types and Software Validation[J].Communication of the ACM,1978:21(1):1048-1064 [3] Goguen J A,Thatcher J W,Wagner E G,et al.Abstract data-types as initial algebras and correctness of data representations[C]∥Proc.Conf.on Comptr.Graphics,Pattern Recognition and Data Structure.1975 [4] Zilles S N.Abstract specifications for data types[R].IBM Res.Lab.,San Jose,Calif.,1975 [5] Meyer B.Applying “Design by Contract”[J].Computer,1992,5(10):40-51 [6] Findler R B,Felleisen M.Behavioral Interface Contracts for Java.http://www.researchtate.net/publication/2245179_Behavioral_Interface_Contracts_for_Java [7] Findle R B,Felleisen M.Contracts for Higher-Order Functions[J].ACM Sigplan.Notices,2002,7(9):48-59 [8] Cheon Y,Leavens G T,Sitaraman M,et al.Model Variables:Cleanly Supporting Abstraction in Design By Contract[J].Software-practice &Experience,2003,5(6):583-599 [9] Hoffman D,Strooper P.State Abstraction and Modular Soft-ware Development[M]∥SIGSOFT 95.Washington,DC,USA,1995 [10] Hatcliff J,Leavens G T.Behavioral Interface Specification Language[J].ACM Computing Surverys,2012,4(3):1-58 [11] Jacobs B,Piessens F.Inspector Methods for State Abstraction:Soundness Proof[J].Journal of Object Technology,2007,6(5):55-75 [12] Dallmeier V,Wasylkowski A,Bettenburg N.Identifying Inspectors to Mine Models of Object Behavior[C]∥ICFEM.2004 [13] Jacobs B,Piessens F.Inspector Methods for State Abstraction:Soundness Proof[R].CW Reports,2007 [14] Grunwald D,Gladisch C.Generating JML Specifications from Alloy Expressions[M]∥Hardware and Software:Verification and Testing.2014 [15] Agostinho S,Moreira A.Contracts for Aspect-Oriented Design[C]∥SPLAT 2008.ACM,2008 [16] Kumar A,Bandyopadhyay.Modeling of State Transition Rules and its Application[J].ACM SIGSOFT Software Engineering Notes,2010,35(2):1-7 [17] Polikarpova N,Furia C A.What Good Are StrongSpecifications?[C]∥ICSE 2013.San Francisco,CA,USA,2013 [18] Polikarpova N,Furia C A,Meyer B.Specifying reusable components[C]∥VSTTE.LNCS,vol.6217,0:127-141 [19] Wei Y,Furia C A,Kazmi N,et al.Inferring better contracts[C]∥ICSE.2011:191-200 [20] Wei Y,Roth H,Furia C A,et al.Stateful testing:Finding more errors in codeand contracts[C]∥ASE.2011:440-443 |
No related articles found! |
|