基于C++STL技术实现Z形式规格说明求精变换的研究
|
摘要
软件开发的形式化方法被当今软件工程领域誉为克服“软件危机”,提高软件可靠性和生产效率的革命性途径。为了克服自然语言和程序设计语言描述规格说明的模糊性和歧义性缺陷,人们提出了形式化开发范型,即通过形式化、规范化的数学理论,用描述“做什么”来取代“怎么做”。
Z语言就是形式化方法中具有代表性的一种形式规格说明,它语言精确、无二义性,可以用于推理和对需求规格说明求精。求精是规格说明实现可执行化的重要过程,实现规格说明求精,可以为Z语言应用于更广泛的领域奠定基础。本文重点研究Z形式规格说明的求精方法,以Z的数据型求精为基础,对Z形式规格说明进行自顶向下,逐步求精,结合C++语言、数据结构以及C++标准模板库技术,探讨Z规格说明的求精方法。
Z是一个类型化的语言,有丰富的数据类型,其数据类型分为简单类型与复合类型。由于Z语言的数据类型相当复杂,现有的高级语言不支持Z语言数据类型的直接转换。但是,C++语言的标准模板库中定义的容器类型却为Z语言数据类型的转换提供了良好的支持,本文先对Z语言的各种数据类型进行分析,然后研究了将其转换为C++代码或C++容器类型,将类型的各种操作算子转换成C++函数的方法,为Z规格说明的进一步求精变换奠定了基础。
本文研究的内容为软件工程设计阶段提供新思路,有助于推进形式化软件工程方法应用于软件开发实践,使软件开发过程更加合理,软件设计更加周密,软件开发的资金分配更加明确,进而达到降低软件开发成本和减少软件后期维护的目的。
Formal software development method is praised as the revolutionary way of software engineering to overcome the "software crisis", and to improve the reliability and the productivity of software. In order to overcome the ambiguities of natural languages and programming languages, people proposed formal models, which describe "what to do" to replace "how to do" by using mathematical theories of formalization and standardization.
Z language is a representative specification language with the qualities of exactness and unambiguity. It can be used for reasoning and refinement of requirment specification. Refinement is an important process of implementing specification to execution. To implement refinement can make the application of Z language wider. This article focuses on the refinement methods of Z formal specification. Based on the refinement of data types, we refine Z formal specification by top-down and stepwise methods. Combined with C++ language, data structure, as well as C++ Standard Template Library technology, the refinement methods of Z specification are explored.
Z is a typed language and has a wealth of data types. Its data types include simple types and composite types. Because of the complexity of data types in Z language, there is no direct way to transform the data types of Z specification to the existing high-level languages. However, the standard template library container types defined in C++ language provides a good support for the transformation of Z language data types. This article first analyzed the data types of Z language, and then researched the methods to transform them to C++ codes or C++ container types, and their operators into C++ functions. The foundation for further transformation and refinement of the Z specification is set up.
The researched content of this paper provides some new ideas for the design phase of software engineering and helps to promote the application of formal methods in software engineering practice of software development. It makes software development process more rational, software design more careful, and the allocation of funds for software development more definite, thus the costs of software development can be depressed and the latter maintenance can be reduced.
Z语言就是形式化方法中具有代表性的一种形式规格说明,它语言精确、无二义性,可以用于推理和对需求规格说明求精。求精是规格说明实现可执行化的重要过程,实现规格说明求精,可以为Z语言应用于更广泛的领域奠定基础。本文重点研究Z形式规格说明的求精方法,以Z的数据型求精为基础,对Z形式规格说明进行自顶向下,逐步求精,结合C++语言、数据结构以及C++标准模板库技术,探讨Z规格说明的求精方法。
Z是一个类型化的语言,有丰富的数据类型,其数据类型分为简单类型与复合类型。由于Z语言的数据类型相当复杂,现有的高级语言不支持Z语言数据类型的直接转换。但是,C++语言的标准模板库中定义的容器类型却为Z语言数据类型的转换提供了良好的支持,本文先对Z语言的各种数据类型进行分析,然后研究了将其转换为C++代码或C++容器类型,将类型的各种操作算子转换成C++函数的方法,为Z规格说明的进一步求精变换奠定了基础。
本文研究的内容为软件工程设计阶段提供新思路,有助于推进形式化软件工程方法应用于软件开发实践,使软件开发过程更加合理,软件设计更加周密,软件开发的资金分配更加明确,进而达到降低软件开发成本和减少软件后期维护的目的。
Formal software development method is praised as the revolutionary way of software engineering to overcome the "software crisis", and to improve the reliability and the productivity of software. In order to overcome the ambiguities of natural languages and programming languages, people proposed formal models, which describe "what to do" to replace "how to do" by using mathematical theories of formalization and standardization.
Z language is a representative specification language with the qualities of exactness and unambiguity. It can be used for reasoning and refinement of requirment specification. Refinement is an important process of implementing specification to execution. To implement refinement can make the application of Z language wider. This article focuses on the refinement methods of Z formal specification. Based on the refinement of data types, we refine Z formal specification by top-down and stepwise methods. Combined with C++ language, data structure, as well as C++ Standard Template Library technology, the refinement methods of Z specification are explored.
Z is a typed language and has a wealth of data types. Its data types include simple types and composite types. Because of the complexity of data types in Z language, there is no direct way to transform the data types of Z specification to the existing high-level languages. However, the standard template library container types defined in C++ language provides a good support for the transformation of Z language data types. This article first analyzed the data types of Z language, and then researched the methods to transform them to C++ codes or C++ container types, and their operators into C++ functions. The foundation for further transformation and refinement of the Z specification is set up.
The researched content of this paper provides some new ideas for the design phase of software engineering and helps to promote the application of formal methods in software engineering practice of software development. It makes software development process more rational, software design more careful, and the allocation of funds for software development more definite, thus the costs of software development can be depressed and the latter maintenance can be reduced.
引文
[1]张海藩.软件工程导论(第4版)[M].北京:清华大学出版社.2003:89-136.
[2]John C.K & D.Ph.Formal Mehtods Specification and Analysis Guidebook for the Verification of Software and Computer Systems[M].Washington:Practitioner's Companion.1997:48-50.
[3]Steen,M.&W.A.Consistency and composition of process specifications[D].United Kingdom:University of Kent at Canterbury,1998.50-52
[4]ISO.Information processing systems open systems interconnection-LOTOS.A formal description technique based on the temporal ordering of observational behavior [S].ISO 8807,1989.102-104.
[5]Michal.J.The Z notation:2nd edition[M].Prentiee Hall,1992:146-148.
[6]Vandevoorde,D.&N.Josuttis著,陈伟柱译.C++Templates 中文版[M].北京:人民邮电出版社,2003:206-322.
[7]Stanley,B.＆H.Lippman,侯捷译Essential C++中文版[M].武汉:华中科技大学出版社,2001:250-256.
[8]Matthew H.Austern著.侯捷译,泛型编程与STL[M].北京:中国电力出版社,2003:132-150.
[9]缪淮扣,李刚,朱关铭.软件工程语言一Z[M].上海:上海科学技术文献出社,1999:99-156.
[10]International Standard ISO/IEC 13568.Information Technology-Z Formal Specification Notation-Syntax,Type System and Semantics[S].1st ed.2002:95-101.
[11]缪淮扣,高晓雷,李刚著.结构化方法、面向对象方法和形式化方法的比较与结合[J].上海:计算机工程,1999,21(4):27-31.
[12]严蔚敏,吴伟民著.数据结构(C语言版).北京:清华大学出版社,2005:85-92.
[13]刘静.基于形式规格说明的统一软件建模系统的研究[D].上海:上海大学,2005:48-54.
[14]Jonathan B.Formal Specification and Documentation using Z:A Case Study Approach[J].The Computer Journal.1996,39(7):643.
[15]Petra,M.& M.Utting.CZT:A Framework for Z Tools[J].Lecture Notes in Computer Science,2005,3455:65-84.
[16]Bruckner,I.& H.Wehrheim.Slicing Object-Z Specifications for Verification[Z].Lecture Notes in Computer Science,2005,3455:414-433.
[17]Bowen,J.& R.Steve.Including Design Guidelines in the Formal Specification of Interface in Z[Z].Lecture Notes in Computer Science,2005,3455:454-471.
[18]缪淮扣.Z规格说明中初始状态存在性证明[J].北京:软件学报,1995,(12):75-79.
[19]袁晓东,郑国梁.Z的面向对象扩充COOZ的设计[J].北京:软件学报,1997,(9):694-700.
[20]王晓龙.Z规格说明中一阶逻辑算子自动求精的研究与实现[D].沈阳:沈阳工业大学,2004:22-25.
[21]李巍巍.Z规格说明中集合论算子自动求精的研究与实现[D].沈阳:沈阳工业大学,2004:32-38
[22]谢茂方.基于Object-Z的软件体系结构描述到JAVA的实现的研究[D].长沙:湖南师范大学,2006,(3):45-47.
[23]文欣.Z规格说明中笛卡尔积算子自动求精的研究与实现[D].沈阳:沈阳工业大学,2003:27-30.
[24]高晓雷,缪淮扣,李勇.基于C++模板的Z规格说明的数据类型的实现[J].上海:计算机工程,第11期,2006,(6):45-48.
[25]李赣生,王华民著.编译原理技术[M],第1版.北京:清华大学出版社,1997:122-148.
[26]王宏生,王晓龙,李巍巍.基于C++STL的Z规格说明数据类型的表示[J].沈阳:辽宁大学学报,自然科学版,2005,(1):59-62.
[27]Stephen,P.孙建春,韦强译.C++Primer Plus(第五版)中文版[M].北京:人民邮电出版社,2005.(5):478-512.
[28]王宏生,李巍巍,王晓龙.一种Z规格说明到C++STL自动转换方法[J].沈阳:小型微型计算机系统(增刊).2004,25(8):184-185.
[29]王昕译.C++STL中文版[M].北京:中国电力出版社,2002:265-284.
[30]于云赫.Z规格说明中关系和函数到C_STL的自动转换.[D].沈阳:沈阳工业大学,2003:24-27.
[31]Diller.Z An Introuduce to Formal Methods[M],Lond -on:John Wiley,1990:186-212.
[32]Luckham,D.C.&J.Vera.An event-based architectured efinition language IS].IEEE Transactions on Software Engineering,1995,21(9):717-734.
[33]Allen,R.& D.Garlan.A formal basis for architectural connection[J].ACM Transactions on Software Engineering and Methodology,1997,6(3):213-249.
[34]Bass,L.& R.Kazman.Architecture-Based development [R].Technical Report CMU/SEI-99-TR-007,Carnegie Mellon University,1999:25-29.
[35]张广泉.关于软件形式化方法[J].重庆:重庆师范学院学报(自然科学版),2002,19(2):21-24.
[36]Zhou,Y.X.& A.Bo.Research on modeling software architecture.Journal of Software,1998,9(11):866-872(in Chinese).
[2]John C.K & D.Ph.Formal Mehtods Specification and Analysis Guidebook for the Verification of Software and Computer Systems[M].Washington:Practitioner's Companion.1997:48-50.
[3]Steen,M.&W.A.Consistency and composition of process specifications[D].United Kingdom:University of Kent at Canterbury,1998.50-52
[4]ISO.Information processing systems open systems interconnection-LOTOS.A formal description technique based on the temporal ordering of observational behavior [S].ISO 8807,1989.102-104.
[5]Michal.J.The Z notation:2nd edition[M].Prentiee Hall,1992:146-148.
[6]Vandevoorde,D.&N.Josuttis著,陈伟柱译.C++Templates 中文版[M].北京:人民邮电出版社,2003:206-322.
[7]Stanley,B.＆H.Lippman,侯捷译Essential C++中文版[M].武汉:华中科技大学出版社,2001:250-256.
[8]Matthew H.Austern著.侯捷译,泛型编程与STL[M].北京:中国电力出版社,2003:132-150.
[9]缪淮扣,李刚,朱关铭.软件工程语言一Z[M].上海:上海科学技术文献出社,1999:99-156.
[10]International Standard ISO/IEC 13568.Information Technology-Z Formal Specification Notation-Syntax,Type System and Semantics[S].1st ed.2002:95-101.
[11]缪淮扣,高晓雷,李刚著.结构化方法、面向对象方法和形式化方法的比较与结合[J].上海:计算机工程,1999,21(4):27-31.
[12]严蔚敏,吴伟民著.数据结构(C语言版).北京:清华大学出版社,2005:85-92.
[13]刘静.基于形式规格说明的统一软件建模系统的研究[D].上海:上海大学,2005:48-54.
[14]Jonathan B.Formal Specification and Documentation using Z:A Case Study Approach[J].The Computer Journal.1996,39(7):643.
[15]Petra,M.& M.Utting.CZT:A Framework for Z Tools[J].Lecture Notes in Computer Science,2005,3455:65-84.
[16]Bruckner,I.& H.Wehrheim.Slicing Object-Z Specifications for Verification[Z].Lecture Notes in Computer Science,2005,3455:414-433.
[17]Bowen,J.& R.Steve.Including Design Guidelines in the Formal Specification of Interface in Z[Z].Lecture Notes in Computer Science,2005,3455:454-471.
[18]缪淮扣.Z规格说明中初始状态存在性证明[J].北京:软件学报,1995,(12):75-79.
[19]袁晓东,郑国梁.Z的面向对象扩充COOZ的设计[J].北京:软件学报,1997,(9):694-700.
[20]王晓龙.Z规格说明中一阶逻辑算子自动求精的研究与实现[D].沈阳:沈阳工业大学,2004:22-25.
[21]李巍巍.Z规格说明中集合论算子自动求精的研究与实现[D].沈阳:沈阳工业大学,2004:32-38
[22]谢茂方.基于Object-Z的软件体系结构描述到JAVA的实现的研究[D].长沙:湖南师范大学,2006,(3):45-47.
[23]文欣.Z规格说明中笛卡尔积算子自动求精的研究与实现[D].沈阳:沈阳工业大学,2003:27-30.
[24]高晓雷,缪淮扣,李勇.基于C++模板的Z规格说明的数据类型的实现[J].上海:计算机工程,第11期,2006,(6):45-48.
[25]李赣生,王华民著.编译原理技术[M],第1版.北京:清华大学出版社,1997:122-148.
[26]王宏生,王晓龙,李巍巍.基于C++STL的Z规格说明数据类型的表示[J].沈阳:辽宁大学学报,自然科学版,2005,(1):59-62.
[27]Stephen,P.孙建春,韦强译.C++Primer Plus(第五版)中文版[M].北京:人民邮电出版社,2005.(5):478-512.
[28]王宏生,李巍巍,王晓龙.一种Z规格说明到C++STL自动转换方法[J].沈阳:小型微型计算机系统(增刊).2004,25(8):184-185.
[29]王昕译.C++STL中文版[M].北京:中国电力出版社,2002:265-284.
[30]于云赫.Z规格说明中关系和函数到C_STL的自动转换.[D].沈阳:沈阳工业大学,2003:24-27.
[31]Diller.Z An Introuduce to Formal Methods[M],Lond -on:John Wiley,1990:186-212.
[32]Luckham,D.C.&J.Vera.An event-based architectured efinition language IS].IEEE Transactions on Software Engineering,1995,21(9):717-734.
[33]Allen,R.& D.Garlan.A formal basis for architectural connection[J].ACM Transactions on Software Engineering and Methodology,1997,6(3):213-249.
[34]Bass,L.& R.Kazman.Architecture-Based development [R].Technical Report CMU/SEI-99-TR-007,Carnegie Mellon University,1999:25-29.
[35]张广泉.关于软件形式化方法[J].重庆:重庆师范学院学报(自然科学版),2002,19(2):21-24.
[36]Zhou,Y.X.& A.Bo.Research on modeling software architecture.Journal of Software,1998,9(11):866-872(in Chinese).
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |