Deductive Synthesis of Algorithms in Human-Computer Interaction

Abstract:

Deductive synthesis is a method of software development where an algorithm is derived from a formal problem specification which guarantees the reliability of final product. The paper introduces a program synthesis method PAR most of whose synthesis steps are mechanical and some of them can be done interactively by human-computer interaction, and formally synthesizes a dependable algorithm for a selection problem supported by PAR method and PAR platform. Program synthesis based on PAR covers a number of classical algorithm design tactics, develops algorithmic programs together with their proof of correctness, and makes the algorithm more reliable and solving idea more understandable.

• Periodical: Applied Mechanics and Materials (Volume 610)
• Pages: 312-315
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.610.312
• Online since: August 2014
• Authors: Hai He Shi*, Hai Peng Shi
• Keywords: Deductive Synthesis, Dependable Algorithms, Human-Computer Interaction (HCI)

References

[1] C. Kreitz, Program synthesis, in: Automated Deduction-A Basis for Application, Academic Publishers, Netherlands, 1998, pp.105-134.

[2] C. George, A.E. Haxthausen, S. Hughes, the RAISE Development Method, Prentice Hall, New York, (1995).

[3] J.R. Abrial, the B-Book: Assigning Programs to Meanings, Cambridge University Press, Cambridge, (1996).

[4] J.Y. Xue, Two new strategies for developing loop invariants and their applications, J. Comput. Sci. Tech. 8 (2), 1993, 147-154.

[5] J.Y. Xue, A unified approach for developing efficient algorithmic programs, J. Comput. Sci. Tech. 12 (4), 1997, 314-329.

[6] J.Y. Xue, B. Yang, Z.K. Zuo, A linear in-situ algorithm for the power of cyclic permutation, in: Proc. 2nd International Frontiers of Algorithmics Workshop (FAW'08), Springer-Verlag, Heidelberg, 2008, pp.113-123.

DOI: 10.1007/978-3-540-69311-6_14

[7] H.H. Shi, J.Y. Xue, PAR-based formal development of algorithms, Chinese J. Comput. 32 (5), 2009, 982-991.

DOI: 10.3724/sp.j.1016.2009.00982

[8] M. H. Alsuwaiyel, Algorithms: Design Techniques and Analysis, World Scientific, 1999, pp.172-176.

[9] T. H. Cormen, Introduction to Algorithms, second ed., MIT Press, Cambridge, (2001).

[10] D.R. Smith, M.R. Lowry, Algorithm theories and design tactics, Sci. Comput. Program. 14 (2-3), 1990, 305-321.

[11] D.R. Smith, Generating programs plus proofs by refinement, in: B. Meyer, J. Woodcock (Eds. ), Verified Software: Theories, Tools, Experiments, LNCS 4171, Springer-Verlag, Heidelberg, 2008, pp.182-188.

DOI: 10.1007/978-3-540-69149-5_20

[12] L. Meertens, Algorithmics-towards programming as a mathematical activity, Math. Comput. Sci. 1 (1986) 289-334.

[13] R.S. Bird, An introduction to the theory of lists, in: Logic of Programming and Calculi of Discrete Design (NATO ASI Series F), 1987, pp.5-42.

DOI: 10.1007/978-3-642-87374-4_1

[14] R.C. Backhouse, An exploration of the Bird-Meertens formalism, TR CS 8810, Department of Computing Science, Groningen University, (1988).

[15] D. Cansell, D. Mery, Proved-patterns-based development for structured programs, in: Proc. 2nd International Symposium on Computer Science in Russia, LNCS 4649, 2007, pp.104-114.