计算机科学 ›› 2016, Vol. 43 ›› Issue (Z6): 457-460.doi: 10.11896/j.issn.1002-137X.2016.6A.108

• 软件工程与数据库技术 • 上一篇    下一篇

基于抽象状态的类的行为规格化方法

王伟,丁二玉,骆斌   

  1. 南京大学软件学院 南京210093 计算机软件新技术国家重点实验室 南京210093,南京大学软件学院 南京210093 计算机软件新技术国家重点实验室 南京210093,南京大学软件学院 南京210093 计算机软件新技术国家重点实验室 南京210093
  • 出版日期:2018-11-14 发布日期:2018-11-14

Behavior Specification Method of Class Based on Abstract State

WANG Wei, DING Eryu and LUO Bin   

  • Online:2018-11-14 Published:2018-11-14

摘要: 为独立方法定义严谨的规格可以保证程序的正确性。但是在面向对象的程序中,方法之间因为共享属性而相互影响,这就需要能够反映方法间影响的规格化方法。研究者们使用抽象变量、状态抽象、堆、查询等多种方法进行了尝试。文中给出一种基于抽象状态的类的行为规格方法,该方法基于抽象状态解决了类方法间的共享依赖和相互影响,同时实现了规格与实现的独立描述与运行时自动化验证。

关键词: 抽象状态,共享依赖,规格化方法

Abstract: State WANG Wei DING Er-yu LUO Bin (Software Institute,Nanjing University,Nanjing 210093,China) (State Key Laboratory for Novel Software Technology,Nanjing 210093,China) Abstract Defining the specifications of the method can reduce the software error,and ensure the correctness of the program.But in object-oriented programs,methods influence each other,so better specifications methods are needed .The researchers try a variety of methods,such as abstract variable,state abstraction,heap, inspector methods and so on.In this paper,we gave a behavior specification method of class based on the abstract state.The method depends on abstract state to solute the shared dependency and influence between the class specification method,and realizes the independent description and validation runtime cohesion between specification and implementation.

Key words: Abstract state,Sharing dependency,Specification method

[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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!