Abstract
Formal method is key approach in developing safety critical systems. Set, Bag, List, Tree, Graph are important reusable components in PAR platform. The paper tries to formally develop Set, Bag, List components which have linear structure. The formal development of those components involves formalization of specification, the recurrence relation of problem solving sequence and loop invariant. Specification language Radl of PAR platform was used to describe the specification, recurrence relation and loop invariants; Software modelling language Apla was used to describe the abstract model of those components. The abstract model denoted by Apla was transformed to concrete model written by executable language; such as C++, Java, VB and C#, etc., based on the program generating systems in PAR platform.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.R., Hayes, I.J., Hoare, T.: The Z Notation: A Reference Manual, 2nd edn. Oriel College, Oxford (1998)
Szyperski, C.: Component software: Beyond Object-oriented Programming, 2nd edn. Addison-Wesley, Reading (2002)
Tian, C., Duan, Z., Zhang, N.: An efficient approach for abstraction-refinement in model checking. Theoret. Comput. Sci. 461, 76–85 (2012)
Dijkstra, E.W.: A Discipline of Programming. Springer, New York (1994)
Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Springer, New York (1981)
He, J., Liu, Z., Li, X.: Component calculus. In: Workshop on Formal Aspects of Component Software (FACS 2003), Satellite Workshop of FME 2003, Pisa, Italy (2003)
Jifeng, H., Li, X., Liu, Z.: Component-based software engineering-the need to link methods and their theories. In: Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 70–95. Springer, Heidelberg (2005). doi:10.1007/11560647_5
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall, Engelwood Cliffs (1990)
Morgan, C.C.: Programming from Specification. Prentice Hall, Upper Saddle River (1994)
Schneider, S.: B-Method. Palgrave, Basingstoke (2001)
Sommerville, I.: Software Engineering, 9th edn. Pearson Education, Upper Saddle River (2011)
Smith, D.R.: Designware: software development by refinement. In: Proceedings of the Eight International Conference on Category Theory and Computer Science, Edinburgh, September 1999
Wu, G., Xue, J.: PAR method and PAR platform used in development process of software outsourcing. Comput. Mod. 11.042 (2013)
Xue, J.: A unified approach for developing efficient algorithmic programs. J. Comput. Sci. Technol. 12(4), 103–118 (1997)
Xue, J.: Two new strategies for developing loop invariants and their applications. J. Comput. Sci. Technol. 8(2), 95–102 (1993)
Xue, J.: Formal derivation of graph algorithmic programs using Partition-and-Recur. J. Comput. Sci. Technol. 13(6), 95–102 (1998)
Xue, J.: Methods of Programming. Higher Education Press, Beijing (2002)
Xue, J.: New concept of loop invariant and its application. In: Proceedings of the 3rd Colloquium on Logic in Engineering Dependable Software, Nanchang, China (2013)
Xue, J.: PAR method and its supporting platform. In: Proceedings of AWCVS 2006, Macao, 29–31 October 2006
Xue, J., Davis, R.: A simple program whose derivation and proof is also. In: Proceedings of The First IEEE International Conference on Formal Engineering Method (ICFEM 1997). IEEE CS Press, November 1997
Xue, J.: Implementation of model-driven development using PAR. In: Keynote Speech on the 6th International Workshop on Harnessing Theories for Tool Support in Software, Nanchang, China (2013)
Zuo, Z., You, Z., Xue, J.: Derivation and formal proof of non-recursive post-order binary tree traversal algorithm. Comput. Eng. Sci. 32(3) (2013)
Duan, Z.: Temporal logic and temporal logic programming. Science Press, Beijing (2005)
Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)
Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008)
Acknowledgments
The authors thank Professor David Gries for discussion about loop invariants in his tutorial lessons in FACS2013 hold in Jiangxi Normal University, Jiangxi Province, China.
This work was supported by the National Nature Science Foundation of China (Grant No. 61272075, No. 61462041, No. 61472167, No. 61662036), the Science and Technology Research Project of Jiangxi Province Educational Department (Grant No. 160329), and the Natural Science Foundation of Jiangxi Province.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Hu, Q., Xue, J., You, Z. (2017). Formal Development of Linear Structure Reusable Components in PAR Platform. In: Liu, S., Duan, Z., Tian, C., Nagoya, F. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2016. Lecture Notes in Computer Science(), vol 10189. Springer, Cham. https://doi.org/10.1007/978-3-319-57708-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-57708-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57707-4
Online ISBN: 978-3-319-57708-1
eBook Packages: Computer ScienceComputer Science (R0)