000			04000nam a2200481 i 4500
001			9781450399746
003			ACM
005			20260609133907.0
008			230111s2023 nyu 001 0deng d
020			_a3568325
020			_a9781450399746 _qebook
020			_a9781450399722 _qepub
020			_z9781450399739 _qhardcover
020			_z9781450399715 _qpaperback
024	7		_a10.1145/3568325 _2doi
100	0		_aMisra, Jayadev _eauthor.
245	1	0	_aEffective Theories in Programming Practice/ _cJayadev Misra.
250			_aFirst Edition
264		1	_a[New York, NY, USA] : _bAssociation for Computing Machinery; _c[2022].
300			_a1 PDF (xx, 542pages) _bLuaTEX
490	1		_aACM books, _x2374-6777 ; _v#47
505	8		_aPreface
505	8		_a1 Introduction -- 1.1 Motivation for This Book -- 1.2 Lessons from Programming Theory -- 1.3 Formalism: The Good, the Bad and the Ugly
505	8		_a2 Set Theory, Logic and Proofs -- 2.1 Set -- 2.2 Function -- 2.3 Relation -- 2.4 Order Relations: Totaland Partial -- 2.5 Propositional Logic -- 2.6 Predicate Calculus -- 2.7 Formal Proofs -- 2.8 Examples of Proof Construction -- 2.9 Exercises
505	8		_a3 Induction and Recursion -- 3.1 Introduction -- 3.2 Examples of Proof by Induction -- 3.3 Methodologies for Applying Induction -- 3.4 Advanced Examples -- 3.5 Noetherian or Well-founded Induction -- 3.6 Structural Induction -- 3.7 Exercises
505	8		_a4 Reasoning About Programs -- 4.1 Overview -- 4.2 Fundamental Ideas -- 4.3 Formal Treatment of Partial Correctness -- 4.4 A Modest Programming Language -- 4.5 Proof Rules -- 4.6 More on Invariant -- 4.7 Formal Treatment of Termination -- 4.8 Reasoning about Performance of Algorithms -- 4.9 Order of Functions -- 4.10 Recurrence Relations -- 4.11 Proving Programs in Practice -- 4.12 Exercises -- 4.A Appendix: Proof of Theorem -- 4.B Appendix: Termination in Chameleons Problem
505	8		_a5 Program Development -- 5.1 Binary Search -- 5.2 Saddleback Search -- 5.3 Dijkstra's Proof of the am-gm Inequality -- 5.4 Quicksort -- 5.5 Heapsort -- 5.6 Knuth-Morris-Pratt String-matching Algorithm -- 5.7 A Sieve Algorithm for Prime Numbers -- 5.8 Stable Matching -- 5.9 Heavy-hitters: A Streaming Algorithm -- 5.10 Exercises
505	8		_a6 Graph Algorithms -- 6.1 Introduction -- 6.2 Background -- 6.3 Specific Graph Structures -- 6.4 Combinatorial Applications of Graph Theory -- 6.5 Reachability in Graphs -- 6.6 Graph Traversal Algorithms -- 6.7 Connected Components of Graphs -- 6.8 Transitive Closure -- 6.9 Single Source Shortest Path -- 6.10 Minimum Spanning Tree -- 6.11 Maximum Flow -- 6.12 Goldberg-Tarjan Algorithm for Maximum Flow -- 6.13 Exercises -- 6.A Appendix: Proof of the Reachability Program -- 6.B Appendix: Depth-first Traversal
505	8		_a7 Recursive and Dynamic Programming -- 7.1 What is Recursive Programming -- 7.2 Programming Notation -- 7.3 Reasoning About Recursive Programs -- 7.4 Recursive Programming Methodology -- 7.5 Recursive Data Types -- 7.6 Dynamic Programming -- 7.7 Exercises -- 7.A Appendices
505	8		_a8 Parallel Recursion -- 8.1 Parallelism and Recursion -- 8.2 Powerlist -- 8.3 Pointwise Function Application -- 8.4 Proofs -- 8.5 Advanced Examples Using Powerlists -- 8.6 Multi-dimensional Powerlist -- 8.7 Other Work on Powerlist -- 8.8 Exercises -- 8.A Appendices
505	8		_aBibliography
505	8		_aAuthors' Biographies
505	8		_aIndex
506			_aAbstract freely available; full-text restricted to subscribers or individual document purchasers.
530			_aAlso available in print.
538			_aMode of access: World Wide Web
538			_aSystem requirements: Adobe Acrobat Reader
650		0	_aEffective Theories in Programming Practice(Computer Science)
655		0	_aElectronic books.
776	0	8	_iPrint version: _z9781450399739 _z9781450399715
830		0	_aACM books - Collection 2 ; _v#47.
856	4	0	_3Abstract with links to full text _uhttps://doi.org/10.1145/3568325
999			_c942 _d942