Abstract
It has been suggested that the notion of reuse be introduced to the formal process of generating algorithms from their specifications so that the programs can be developed automatically with low costs. Through studying algorithm generation under guidance of formal method we develop reuse-based techniques for reliable algorithm generation by reusing subsets of formal processes. We formalize the concepts and definitions for the approach via the language of category theory. The proposed method minimizes the process for the generation of a series of reliable algorithms for problems with linear structures, and transfers algorithm design tasks into routine work that can be implemented automatically. Furthermore, under the proposed framework, a series of algorithm variants for an ordered searching problem and a new sorting algorithm are generated, which demonstrate the effectiveness of the technique as well as its capacity to produce new advanced algorithms that have different structures from existing ones.
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
Similar content being viewed by others
References
Hoare, T.: The verifying compiler: a grand challenge for computing research. J. ACM. 50(1), 63–69 (2003)
Harel, D., Feldman, Y.: Algorithmics: The Spirit of Computing, 3rd edn. Addison-Wesley, Upper Saddle River (2004)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–585 (1969)
Dijkstra, E.W.: A Discipline of Programmin. Prentice-Hall Inc, Upper Saddle River (1976)
Milner, R.: Fully abstract models of typed lambda-calculi. Theor. Comput. Sci. 4(1), 1–22 (1977)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE. FOCS, pp. 46–57 (1977)
Gries, D.: The Science of Programming. Springer, New York (1981). https://doi.org/10.1007/978-1-4612-5983-1
Gray, J.: What next? a dozen information-technology research goals. J. ACM. 50(1), 41–57 (2003)
Selby, R.W.: Enabling reuse-based software development of large-scale systems. IEEE T. Software Eng. 31(6), 495–510 (2005)
Franssen, M.: Cocktail: a Tool for Deriving Correct Programs. Ph.D. diss., Eindhoven University of Technology (2000)
Smith, D.R.: Generating Programs plus Proofs by Refinement. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments, pp. 182–188. Springer-Verlag, New York (2008). https://doi.org/10.1007/978-3-540-69149-5_20
Yakhnis, V.R., Farrell, J.A., Shultz, S.S.: Deriving programs using generic algorithms. IBM Syst. J. 33(1), 158–181 (1994)
Novak, G.: Software reuse by specialization of generic procedures through views. IEEE T. Software Eng. 23(7), 401–417 (1997)
Zheng, Y., Xu, C., Xue, J.: A simple greedy algorithm for a class of shuttle transportation problems. Optim. Lett. 3(4), 491–497 (2009)
Gonçalves, J., Storer, R., Gondzio, J.: A family of linear programming algorithms based on an algorithm by von Neumann. Optim. Method. Softw. 24(3), 461–478 (2009)
Breitenreichera, D., Lellmanna, J., Schnörra, C.: COAL: a generic modelling and prototyping framework for convex optimization problems of variational image analysis. Optim. Method. Softw. 28(5), 1081–1094 (2013)
Idate, S., Patil, S.H., Mali, D.J.: Automated code generation using generative programming approach for a mathematical expression. In: Proceedings of the International Conference Systemics, Cybernetics and Informatics, pp. 134–137 (2008)
Nedunuri, S., Cook, W.R.: Synthesis of fast programs for maximum segment sum problems. In: Proceedings of the 8th International Conference on Generative Programming and Component Engineering, pp. 117–126 (2009)
Robidoux, R., Xu, H., Xing, L., Zhou, M.: Automated modeling of dynamic reliability block diagrams using colored petri nets. IEEE Trans. Syst. Man Cybern. A Syst. Hum. 40(2), 337–351 (2010)
Bolton, M.L., Siminiceanu, R.I., Bass, E.J.: A systematic approach to model checking human-automation interaction using task-analytic models. IEEE Trans. Syst. Man Cybern. A Syst. Hum. 41(5), 961–976 (2011)
Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: Using formal verification to evaluate human-automation interaction: a review. IEEE Trans. Syst. Man Cybern. Syst. 43(3), 488–503 (2013)
Liu, Y.A.: Systematic Program Design— from Clarity to Efficiency. Cambridge University Press, Cambridge (2013)
Knuth, D.: The Art of Computer Programming, vol. 3: Sorting and Searching, third ed. Addison-Wesley, Massachusetts (1998)
Clark, K., Darlington, J.: Algorithm classification through synthesis. Comput. J. 23(1), 61–65 (1980)
Xue, J.: A unified approach for developing efficient algorithmic programs. J. Comput. Sci. Tech-CH. 12(4), 314–329 (1997)
Xue, J., Davis, R.: A derivation and proof of Knuth’s binary to decimal program. Software-Conc. Tool 18, 149–156 (1997)
Xue, J.: Formal derivation of graph algorithmic programs using partition-and-recur. J. Comput. Sci. Tech-CH. 13(6), 553–561 (1998)
Xue, J., Yang, B., Zuo, Z.: A linear in-situ algorithm for the power of cyclic permutation. In: Proceeding of the s 2nd International Frontiers. Algorithmics, pp. 113–123 (2008)
Xue, J., Zheng, Y., Hu, Q., et al.: PAR: a practicable formal method and its supporting platform. In: Sun, J., Sun, M. (eds.), ICFEM 2018. LNCS, vol. 11232. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02450-5_5
Asperti, A., Longo, G.: Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press, Cambridge (1991)
Goguen, J.A.: A categorical manifesto. Math. Struct. Comput. Sci. 1, 49–67 (1991)
Acknowledgments
This work was funded by the National Natural Science Foundation of China under Grant No.62062039, and the Natural Science Foundation of Jiangxi Province under Grant No.20202BAB202024.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Shi, H., Shi, H., Xu, S. (2021). Algorithm Design Through the Optimization of Reuse-Based Generation. In: He, K., Zhong, C., Cai, Z., Yin, Y. (eds) Theoretical Computer Science. NCTCS 2020. Communications in Computer and Information Science, vol 1352. Springer, Singapore. https://doi.org/10.1007/978-981-16-1877-2_2
Download citation
DOI: https://doi.org/10.1007/978-981-16-1877-2_2
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-16-1876-5
Online ISBN: 978-981-16-1877-2
eBook Packages: Computer ScienceComputer Science (R0)