ACM Digital Library home
ACM home
Advanced Search
10.1145/3568325acmbooksBook PagePublication PagesBookacm-pubtype
Skip header Section
Effective Theories in Programming PracticeJanuary 2023
Publisher:
  • Association for Computing Machinery
  • New York
  • NY
  • United States
ISBN:978-1-4503-9973-9
Published:11 January 2023
Pages:
562
Appears In:
ACMACM Books
Purchase this BookRecommend ACM DL
ALREADY A SUBSCRIBER?SIGN IN
Skip Bibliometrics Section
Bibliometrics
Citation count
0
Downloads (6 weeks)
45
Downloads (12 months)
168
Downloads (cumulative)
168
Skip Abstract Section
Abstract

Set theory, logic, discrete mathematics, and fundamental algorithms (along with their correctness and complexity analysis) will always remain useful for computing professionals and need to be understood by students who want to succeed. This textbook explains a number of those fundamental algorithms to programming students in a concise, yet precise, manner. The book includes the background material needed to understand the explanations and to develop such explanations for other algorithms. The author demonstrates that clarity and simplicity are achieved not by avoiding formalism, but by using it properly.

The book is self-contained, assuming only a background in high school mathematics and elementary program writing skills. It does not assume familiarity with any specific programming language. Starting with basic concepts of sets, functions, relations, logic, and proof techniques including induction, the necessary mathematical framework for reasoning about the correctness, termination and efficiency of programs is introduced with examples at each stage. The book contains the systematic development, from appropriate theories, of a variety of fundamental algorithms related to search, sorting, matching, graph-related problems, recursive programming methodology and dynamic programming techniques, culminating in parallel recursive structures.

Book Downloads

PDFFront matter (Title page, ACM Books, Contents, Preface, Bibliography, Author’s Biography, Index)

Bibliography

  1. K. Achatz and W. Schulte. 1996. Massive parallelization of divide-and-conquer algorithms over powerlists. Sci. Comput. Program. 26, 1, 59–78. .Google ScholarGoogle Scholar
  2. W. Adams. 1994. Verifying Adder Circuits Using Powerlists. Technical Report TR 94-02. Department of Computer Science, University of Texas at Austin.Google ScholarGoogle Scholar
  3. B. Aspvall, M. F. Plass, and R. E. Tarjan. 1979. A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8, 3, 121–123. DOI: .Google ScholarGoogle Scholar
  4. S. K. Basu and J. Misra. 1975. Proving loop programs. IEEE Trans. Softw. Eng. SE-1, 1, 76–86. DOI: .Google ScholarGoogle Scholar
  5. K. Batcher. 1968. Sorting networks and their applications. In Proc. AFIPS Spring Joint Computer Conference, Vol. 32. AFIPS Press, Reston, VA, 307–314. DOI: .Google ScholarGoogle Scholar
  6. E. Beckenbach and R. Bellman. 1961. An Introduction to Inequalities. Mathematical Association of America.Google ScholarGoogle Scholar
  7. R. Bellman. 1957. Dynamic Programming. Princeton University Press, Princeton, NJ.Google ScholarGoogle Scholar
  8. R. Bellman. 1958. On a routing problem. Q. Appl. Math. 16, 1, 87–90. DOI: .Google ScholarGoogle Scholar
  9. J. L. Bentley and M. D. McIlroy. 1993. Engineering a sort function. Softw. Pract. Exp. 23, 11, 1249–1265. DOI: .Google ScholarGoogle Scholar
  10. R. S. Bird. 2006. Improving saddleback search: A lesson in algorithm design. In Mathematics of Program Construction, MPC 2006. Lecture Notes in Computer Science, Vol. 4014. Springer, Berlin, 82–89. DOI: .Google ScholarGoogle Scholar
  11. B. H. Bloom. 1970. Space/time trade-offs in hash coding with allowable errors. Commun. ACM 13, 7, 422–426. DOI: .Google ScholarGoogle Scholar
  12. M. Blum, R. W. Floyd, V. R. Pratt, R. L. Rivest, and R. E. Tarjan. 1973. Time bounds for selection. J. Comput. Syst. Sci. 7, 4, 448–461. DOI: .Google ScholarGoogle Scholar
  13. R. Boyer and J. Moore. 1991. MJRTY—A fast majority vote algorithm. In R. Boyer (Ed.), Automated Reasoning: Essays in Honor of Woody Bledsoe. Automated Reasoning Series, Vol. 1. Kluwer Academic Publishers, Dordrecht, The Netherlands, 105–117. DOI: .Google ScholarGoogle Scholar
  14. R. S. Boyer and J. S. Moore. 1977. A fast string searching algorithm. Commun. ACM 20, 10, 762–772. DOI: .Google ScholarGoogle Scholar
  15. R. E. Bryant. 1992. Symbolic boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv. 24, 3, 293–318. DOI: .Google ScholarGoogle Scholar
  16. R. M. Burstall. 1969. Proving properties of programs by structural induction. Comput. J. 12, 1, 41–48. The British Computer Society. DOI: .Google ScholarGoogle Scholar
  17. K. M. Chandy and J. Misra. 1984. The drinking philosophers problem. ACM Trans. Program. Lang. Syst. 6, 4, 632–646.Google ScholarGoogle Scholar
  18. M. Charikar, K. Chen, and M. Farach-Colton. 2004. Finding frequent items in data streams. Theor. Comput. Sci. 312, 1, 3–15. DOI: .Google ScholarGoogle Scholar
  19. A. Church. 1941. The Calculi of Lambda Conversion. Princeton University Press.Google ScholarGoogle Scholar
  20. E. Clarke and E. Emerson. 1982. Design and synthesis of synchronization skeletons using branching time temporal logic. In D. Kozen (Ed.), Logics of Programs. Lecture Notes in Computer Science, Vol. 131. Springer-Verlag, 52–71. DOI: .Google ScholarGoogle Scholar
  21. S. Cook. 1970. Linear Time Simulation of Deterministic Two-Way Pushdown Automata. Technical report. Department of Computer Science, University of Toronto.Google ScholarGoogle Scholar
  22. J. M. Cooley and J. W. Tukey. 1965. An algorithm for the machine calculation of complex Fourier series. Math. Comput. 19, 90, 297–301. DOI: .Google ScholarGoogle Scholar
  23. D. Coppersmith and S. Winograd. 1990. Matrix multiplication via arithmetic progressions. J. Symb. Comput. 9, 3, 251–280. DOI: .Google ScholarGoogle Scholar
  24. H. S. M. Coxeter. 1961. Introduction to Geometry. John Wiley & Sons, New York.Google ScholarGoogle Scholar
  25. O. Dahl, E. Dijkstra, and C. Hoare. 1972. Structured Programming. Academic Press.Google ScholarGoogle Scholar
  26. M. Davis and H. Putnam. 1960. A computing procedure for quantification theory. J. ACM 7, 3, 201–215. DOI: .Google ScholarGoogle Scholar
  27. M. Davis, G. Logemann, and D. Loveland. 1962. A machine program for theorem-proving. Commun. ACM 5, 7, 394–397. DOI: .Google ScholarGoogle Scholar
  28. N. Dershowitz and Z. Manna. 1979. Proving termination with multiset ordering. Commun. ACM 22, 8, 465–476. DOI: .Google ScholarGoogle Scholar
  29. E. W. Dijkstra. 1959. A note on two problems in connexion with graphs. Numer. Math. 1, 1, 269–271. DOI: .Google ScholarGoogle Scholar
  30. E. W. Dijkstra. 1975. Guarded commands, nondeterminacy and the formal derivation of programs. Commun. ACM 18, 8, 453–457. DOI: .Google ScholarGoogle Scholar
  31. E. W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall.Google ScholarGoogle Scholar
  32. E. W. Dijkstra. May. 1980. A short proof of one of Fermat’s theorems. EWD740: Circulated privately. http://www.cs.utexas.edu/users/EWD/ewd07xx/EWD740.PDF.Google ScholarGoogle Scholar
  33. E. W. Dijkstra. March. 1991. The undeserved status of the pigeon-hole principle. EWD 1094: Circulated privately. http://www.cs.utexas.edu/users/EWD/ewd10xx/EWD1094.PDF.Google ScholarGoogle Scholar
  34. E. W. Dijkstra. September. 1993. A bagatelle on Euclid’s algorithm. EWD1158: Circulated privately. https://www.cs.utexas.edu/users/EWD/ewd11xx/EWD1158.PDF.Google ScholarGoogle Scholar
  35. E. W. Dijkstra. August. 1995. For the record: Painting the squared plane. EWD 1212: Circulated privately. https://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EWD1212.html.Google ScholarGoogle Scholar
  36. E. W. Dijkstra. February. 1996a. The arithmetic and geometric means once more. EWD1231: Circulated privately. https://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EWD1231.html.Google ScholarGoogle Scholar
  37. E. W. Dijkstra. October. 1996b. Homework #1. EWD1248: Circulated privately. http://www.cs.utexas.edu/users/EWD/ewd12xx/EWD1248.PDF.Google ScholarGoogle Scholar
  38. E. W. Dijkstra. November. 1999. Constructing the binary search once more. EWD1293: Circulated privately. https://www.cs.utexas.edu/users/EWD/ewd12xx/EWD1293.PDF.Google ScholarGoogle Scholar
  39. E. W. Dijkstra. April. 2002. Coxeter’s rabbit. EWD1318: Circulated privately. https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1318.html.Google ScholarGoogle Scholar
  40. E. W. Dijkstra. June. 2003. A problem solved in my head. EWD666: Circulated privately. https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD666.html.Google ScholarGoogle Scholar
  41. E. W. Dijkstra and J. Misra. 2001. Designing a calculational proof of Cantor’s theorem. Am. Math. Mon. 108, 5, 440–443. DOI: .Google ScholarGoogle Scholar
  42. E. W. Dijkstra and C. S. Scholten. 1989. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag.Google ScholarGoogle Scholar
  43. M. Fitting. 1990. First-order logic. In First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 97–125. DOI: .Google ScholarGoogle Scholar
  44. R. W. Floyd. 1962. Algorithm 97: Shortest path. Commun. ACM 5, 6, 345. DOI: .Google ScholarGoogle Scholar
  45. R. W. Floyd. 1964. Algorithm 245: Treesort. Commun. ACM 7, 12, 701. DOI: .Google ScholarGoogle Scholar
  46. R. W. Floyd. 1967. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics XIX. American Mathematical Society, 19–32.Google ScholarGoogle Scholar
  47. L. R. Ford Jr. 1956. Network Flow Theory. Technical report. RAND Corporation, Santa Monica, CA. https://www.rand.org/pubs/papers/P923.Google ScholarGoogle Scholar
  48. L. Ford, Jr and D. Fulkerson. 1962. Flows in Networks. Princeton University Press.Google ScholarGoogle Scholar
  49. M. Fredman and M. Saks. 1989. The cell probe complexity of dynamic data structures. In Proc. of the Twenty-First Annual ACM Symposium on Theory of Computing. ACM, 345–354. DOI: .Google ScholarGoogle Scholar
  50. M. Fürer. 2007. Faster integer multiplication. In Proceedings of the Thirty-ninth Annual ACM Symposium on Theory of Computing, STOC’07. ACM, 57–66. DOI: .Google ScholarGoogle Scholar
  51. M. Gardner. 2001. The Colossal Book of Mathematics: Classic Puzzles, Paradoxes, and Problems: Number Theory, Algebra, Geometry, Probability, Topology, Game Theory, Infinity, and Other Topics of Recreational Mathematics. WW Norton & Company.Google ScholarGoogle Scholar
  52. D. Gale and L. S. Shapley. 1962. College admissions and the stability of marriage. Am. Math. Monthly 69, 1, 9–15. DOI: .Google ScholarGoogle Scholar
  53. A. V. Goldberg and R. E. Tarjan. 1988. A new approach to the maximum-flow problem. J. ACM 35, 4, 921–940. DOI: .Google ScholarGoogle Scholar
  54. D. Gries. 1981. The Science of Programming. Texts and Monographs in Computer Science. Springer-Verlag. DOI: .Google ScholarGoogle Scholar
  55. D. Gries and F. B. Schneider. 1994. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer-Verlag. DOI: .Google ScholarGoogle Scholar
  56. A. Gupta and J. Misra. 2003. Synthesizing Programs Over Recursive Data Structures. Technical Report TR03-38. Computer Science Dept., University of Texas at Austin.Google ScholarGoogle Scholar
  57. P. Hall. 1935. On representatives of subsets. J. Lond. Math. Soc. 10, 1, 26–30. DOI: .Google ScholarGoogle Scholar
  58. E. C. R. Hehner. 1984. The Logic of Programming. Prentice-Hall. Series in Computer Science, C.A.R. Hoare, series editor.Google ScholarGoogle Scholar
  59. E. C. Hehner. 1993. A Practical Theory of Programming. Springer-Verlag.Google ScholarGoogle Scholar
  60. E. C. R. Hehner. 2022. A Practical Theory of Programming. http://www.cs.utoronto.ca/∼hehner/aPToP. Manuscript available for online access and download.Google ScholarGoogle Scholar
  61. J. Hendrix, D. Kapur, and J. Meseguer. 2010. Coverset induction with partiality and subsorts: A powerlist case study. In M. Kaufmann and L. C. Paulson (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science, Vol. 6172. Springer, Berlin, 275–290. ISBN 978-3-642-14052-5. DOI: .Google ScholarGoogle Scholar
  62. M. J. H. Heule, O. Kullmann, and V. W. Marek. 2016. Solving and verifying the Boolean Pythagorean Triples problem via cube-and-conquer. In Proceedings of SAT 2016. Springer. 228–245. DOI: .Google ScholarGoogle Scholar
  63. A. Hinkis. 2013. Proofs of the Cantor-Bernstein Theorem. Springer. DOI: .Google ScholarGoogle Scholar
  64. C. A. R. Hoare. 1961. Partition: Algorithm 63, Quicksort: Algorithm 64, and Find: Algorithm 65. Commun. ACM 4, 7, 321–322.Google ScholarGoogle Scholar
  65. C. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 576–580, 583. DOI: .Google ScholarGoogle Scholar
  66. C. A. R. Hoare and J. Misra. 2009. Preface to the special issue on software verification. ACM Comput. Surv. 41, 4, 1–3. DOI: .Google ScholarGoogle Scholar
  67. P. Hudak, J. Peterson, and J. Fasel. 2000. A Gentle Introduction to Haskell, Version 98. http://www.haskell.org/tutorial/.Google ScholarGoogle Scholar
  68. D. Kapur and M. Subramaniam. 1995. Automated reasoning about parallel algorithms using powerlists. In International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, Vol. 936. Springer, 416–430. DOI: .Google ScholarGoogle Scholar
  69. D. Kapur and M. Subramaniam. 1998. Mechanical verification of adder circuits using rewrite rule laboratory. Form. Methods Syst. Des. 13, 2, 127–158. DOI: .Google ScholarGoogle Scholar
  70. V. King, S. Rao, and R. Tarjan. 1994. A faster deterministic maximum flow algorithm.J. Algorithms 17, 3, 447–474. DOI: .Google ScholarGoogle Scholar
  71. D. Kitchin, A. Quark, and J. Misra. 2010. Quicksort: Combining concurrency, recursion, and mutable data structures. In A. W. Roscoe, C. B. Jones, and K. Wood (Eds.), Reflections on the Work of C.A.R. Hoare, History of Computing. Written in honor of Sir Tony Hoare’s 75th birthday. Springer, 229–254. DOI: .Google ScholarGoogle Scholar
  72. D. E. Knuth. 1998. The Art of Computer Programming (2nd ed.) Sorting and Searching, Vol. 3. Addison Wesley Longman Publishing.Google ScholarGoogle Scholar
  73. D. E. Knuth. 2014. Art of Computer Programming, Vol. 2. Seminumerical Algorithms. Addison-Wesley Professional.Google ScholarGoogle Scholar
  74. D. E. Knuth, J. H. Morris Jr, and V. R. Pratt. 1977. Fast pattern matching in strings. SIAM J. Comput. 6, 2, 323–350. DOI: .Google ScholarGoogle Scholar
  75. J. Kornerup. 1997a. Data Structures for Parallel Recursion. Ph.D. thesis. University of Texas at Austin.Google ScholarGoogle Scholar
  76. J. Kornerup. 1997b. Parlists—A generalization of powerlists. In C. Lengauer, M. Griebl, and S. Gorlatch (Eds.), Proceedings of Euro-Par’97, Lecture Notes in Computer Science, Vol. 1300. Springer-Verlag, 614–618. DOI: .Google ScholarGoogle Scholar
  77. J. B. Kruskal. 1956. On the shortest spanning subtree of a graph and the traveling salesman problem. Proc. Am. Math. Soc. 7, 1, 48–50. DOI: .Google ScholarGoogle Scholar
  78. R. E. Ladner and M. J. Fischer. 1980. Parallel prefix computation. J. ACM 27, 4, 831–838. DOI: .Google ScholarGoogle Scholar
  79. W. J. LeVeque. 1956. Topics in Number Theory, Vol. 1. Addison-Wesley, Reading, MA.Google ScholarGoogle Scholar
  80. S. Marlow (Ed.). 2010. Haskell 2010 Language Report. https://www.haskell.org/onlinereport/haskell2010/.Google ScholarGoogle Scholar
  81. K. L. McMillan. 2005. Applications of Craig interpolants in model checking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 3440. Springer, 1–12. DOI: .Google ScholarGoogle Scholar
  82. E. Mendelson. 1987. Introduction to Mathematical Logic (3rd. ed.). Wadsworth & Brooks.Google ScholarGoogle Scholar
  83. J. Misra. 1977. Prospects and limitations of automatic assertion generation for loop programs. SIAM J. Comput. 6, 4, 718–729. DOI: .Google ScholarGoogle Scholar
  84. J. Misra. 1978. A technique of algorithm construction on sequences. IEEE Trans. Softw. Eng. SE-4, 1, 65–69. DOI: .Google ScholarGoogle Scholar
  85. J. Misra. 1979. Space-time trade off in implementing certain set operations. Inf. Process. Lett. 8, 2, 81–85. DOI: .Google ScholarGoogle Scholar
  86. J. Misra. 1981. An exercise in program explanation. ACM Trans. Program. Lang. Syst. 3, 1, 104–109. DOI: .Google ScholarGoogle Scholar
  87. J. Misra. 1994. Powerlist: A structure for parallel recursion. ACM Trans. Program. Lang. Syst. 16, 6, 1737–1767. DOI: .Google ScholarGoogle Scholar
  88. J. Misra. 2000. Generating-functions of interconnection networks. In J. Davies, B. Roscoe, and J. Woodcock (Eds.), Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare, Cornerstones of Computing. Macmillan Education UK.Google ScholarGoogle Scholar
  89. J. Misra. September. 2021. A proof of Fermat’s little theorem. http://www.cs.utexas.edu/users/misra/Fermat.pdf.Google ScholarGoogle Scholar
  90. J. Misra and D. Gries. 1982. Finding repeated elements. Sci. Comput. Program 2, 2, 143–152. DOI: .Google ScholarGoogle Scholar
  91. C. Morgan. 1990. Programming from Specifications. Prentice-Hall, Inc.Google ScholarGoogle Scholar
  92. J. B. Orlin. 2013. Max flows in 𝒪(n ⋅ m) time, or better. In Proceedings of the Forty-fifth Annual ACM Symposium on Theory of Computing. 765–774.Google ScholarGoogle Scholar
  93. S. Owicki and D. Gries. 1976. An axiomatic proof technique for parallel programs I. Acta Inform. 6, 1, 319–340. DOI: .Google ScholarGoogle Scholar
  94. S. Pettie and V. Ramachandran. 2002. An optimal minimum spanning tree algorithm. J. ACM 49, 1, 16–34. DOI: .Google ScholarGoogle Scholar
  95. B. Pope. 2001. A tour of the Haskell Prelude. https://cs.fit.edu/∼ryan/cse4250/tourofprelude.html. Unpublished manuscript.Google ScholarGoogle Scholar
  96. E. Price. 2021. Sparse recovery. In T. Roughgarden (Ed.), Beyond the Worst-Case Analysis of Algorithms. Cambridge University Press, 140–164. DOI: .Google ScholarGoogle Scholar
  97. R. C. Prim. 1957. Shortest connection networks and some generalizations. Bell Syst. Tech. J. 36, 6, 1389–1401. DOI: .Google ScholarGoogle Scholar
  98. J. Queille and J. Sifakis. 1982. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, Vol. 137. Springer, 337–351. DOI: .Google ScholarGoogle Scholar
  99. J. A. Robinson. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1, 23–41. DOI: .Google ScholarGoogle Scholar
  100. C. Rocha and J. Meseguer. 2008. Theorem proving modulo based on boolean equational procedures. In Proc. RelMiCS 2008. Lecture Notes in Computer Science, Vol. 4988. Springer, 337–351. DOI: .Google ScholarGoogle Scholar
  101. T. Roughgarden and G. Valiant. 2015. CS168: The modern algorithmic toolbox, lecture 2: Approximate heavy hitters and the count-min sketch. https://web.stanford.edu/class/cs168/l/l2.pdf.Google ScholarGoogle Scholar
  102. A. Schönhage and V. Strassen. 1971. Schnelle multiplikation großer zahlen. Computing 7, 3, 281–292. DOI: .Google ScholarGoogle Scholar
  103. M. Sharir. 1981. A strong-connectivity algorithm and its applications to data flow analysis. Comput. Math. Appl. 7, 1, 67–72. DOI: .Google ScholarGoogle Scholar
  104. M. Sollin. 1965. La tracé de canalisation. Programming, Games, and Transportation Networks. Wiley.Google ScholarGoogle Scholar
  105. V. Strassen. 1969. Gaussian elimination is not optimal. Numer. Math. 13, 4, 354–356. DOI: .Google ScholarGoogle Scholar
  106. R. Tarjan. 1972. Depth-first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146–160. DOI: .Google ScholarGoogle Scholar
  107. R. E. Tarjan and J. van Leeuwen. 1984. Worst-case analysis of set union algorithms. J. ACM 31, 2, 245–281. DOI: .Google ScholarGoogle Scholar
  108. A. Tarski. 1955. A lattice-theoretical fixpoint theorem and its application. Pac. J. Math. 5, 2, 285–309. DOI: .Google ScholarGoogle Scholar
  109. J. van Heijenoort. 2002. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Source Books in the History of the Sciences. Harvard University Press.Google ScholarGoogle Scholar
  110. S. Warshall. 1962. A theorem on boolean matrices. J. ACM 9, 1, 11–12. .Google ScholarGoogle Scholar
  111. J. W. J. Williams. 1964. Algorithm 232: Heapsort. Commu. ACM 7, 347–348.Google ScholarGoogle Scholar
Contributors
  • Jayadev Misra
    The University of Texas at Austin

Index Terms

(auto-classified)
  1. Effective Theories in Programming Practice
            Comments
            About Cookies On This Site

            We use cookies to ensure that we give you the best experience on our website.

            Learn more

            Got it!