OPAC

検索結果一覧に戻る

Theories of Programming : The Life and Works of Tony Hoare / Cliff B. Jones, Jayadev Misra
(ACM books - Collection 2 ; #39)

データ種別	電子ブック
版	First Edition
出版者	([New York, NY, USA] : Association for Computing Machinery)
出版年	[2021]
大きさ	1 PDF (xx, 430 pages) : LuaTEX
著者標目	*Jones, Cliff B editor

所蔵情報を非表示

URL	巻　次	配架場所	請求記号	登録番号	コメント	刷　年	状　態	利用注記	ISBN	予約	請求メモ
URL		射水-電子	007	EB0005056	ACM Books Collection 2				3477355

書誌詳細を非表示

一般注記	Preface PART I INTRODUCTION 1 The 1980 ACM Turing Award Lecture 2 Finding Effective Abstractions -- 2.1 Programming Languages -- 2.2 Founding the Field of Axiomatic Semantics -- 2.3 Concurrency -- 2.4 Unifying Theories of Programming -- References PART II PROGRAM VERIFICATION 3 Assessing the Success and Impact of Hoare's Logic -- 3.1 Early Approaches to Program Verification -- 3.2 Hoare's Logic -- 3.3 Hoare's Initial Contributions -- 3.4 Termination -- 3.5 Influence on Programming Methodology -- 3.6 Hoare's Reasoning About Recursive Procedures -- 3.7 Research on Soundness and Completeness -- 3.8 Reasoning About Arbitrary Procedures -- 3.9 Parallel Programs -- 3.10 Distributed Programs -- 3.11 Object-orientated Programs -- 3.12 Competing Approaches to Program Verification -- 3.13 Concluding Remarks -- References 4 Preface to Special Issue on Software Verification 5 The Verified Software Initiative: A Manifesto -- 5.1 Introduction -- 5.2 Executive Summary -- 5.3 Manifesto -- 5.4 Assessment -- 5.5 Conclusions 6 The First Fifteen Years of the Verified Software Project -- 6.1 Introduction -- 6.2 The Roots of the Verified Software Initiative -- 6.3 Theory -- 6.4 Tools -- 6.5 Experiments -- 6.6 The Road Ahead -- References 7 Verification in the Grand Challenge -- 7.1 Introduction -- 7.2 Tokeneer -- 7.3 Research Based on Tokeneer -- 7.4 Pilot Project: Hypervisor -- 7.5 What's Next? PART III COMMUNICATING SEQUENTIAL PROCESSES 8 Communicating Sequential Processes -- 8.1 Introduction -- 8.2 Concepts and Notations -- 8.3 Coroutines -- 8.4 Subroutines and Data Representations -- 8.5 Monitors and Scheduling -- 8.6 Miscellaneous -- 8.7 Discussion -- 8.8 Conclusion -- References 9 CSP: A Practical Process Algebra -- 9.1 Introduction -- 9.2 Prehistory 1978-1991 -- 9.3 FDR1 1991-1996 : Communication, Fault Tolerance, and the Beginning of Time -- 9.4 FDR2 1994-2007 at FSEL: Protocols, Abstraction, and Industrial Applications -- 9.5 FDR2 into Academia: Exploring Implicit Checking and Timed CSP (2007-2012) -- 9.6 FDR3 and FDR4: Back to Basics and into the Cloud (2012-2019) -- 9.8 The Future: For CSP and Beyond (2019-) -- 9.9 Reflections on FDR -- References PART IV TEACHING AND INDUSTRIAL AFFILIATIONS 10 Teaching at Belfast and Oxford -- 10.1 Introduction -- 10.2 Queen's University Belfast -- 10.3 University of Oxford -- 10.4 Valediction -- References 11 Software Specification -- 11.1 Precondition-Postcondition Specifications -- 11.2 Specification of Data Types -- 11.3 The Role of Specification -- 11.4 Abstraction in Specification -- 11.5 Specifying Operations -- 11.6 Abstract Data Types -- 11.7 Structuring Specifications Via Aspects -- 11.8 The IBM/CICS Project -- 11.9 Industry Influence on Research -- 11.10 Conclusions -- References 12 CSP, Occam, and Inmos -- 12.1 Background -- 12.2 The Inmos System Language -- 12.3 Parallel Execution -- 12.4 Channels -- 12.5 Alternative -- 12.6 Timers -- 12.7 Subroutines -- 12.8 The Algebraic Specification -- 12.9 Formal Methods in Hardware Design -- 12.10 Hardware Design Languages -- 12.11 General Purpose Parallel Computers -- 12.12 Impact - 12.13 Tomorrow -- 12.14 Retrospect -- References PART V RECENT RESEARCH DIRECTIONS 13 Hoare and He's Unifying Theories of Programming -- 13.1 Origins of UTP -- 13.2 Retirement Symposium and UTP Book Launch -- 13.3 Introduction to UTP -- 13.4 Relational Calculus -- 13.5 Relational Semantics of a Programming Language -- 13.6 Designs -- 13.7 Galois Connections -- 13.8 Design Healthiness Conditions -- 13.9 The UTP School of Semantics -- References 14 Trimming the Hedges: An Algebra to Tame Concurrency -- 14.1 Prologue -- 14.2 Prehistory -- 14.3 Concurrent Kleene Algebra -- 14.4 Interchange in Context -- 14.5 Series-parallel Pomsets, Completeness, and Decidability -- 14.6 Weak Interchange and Compositional Concurrency -- 14.7 Other Developments -- 14.8 Epilogue -- References PART VI RETROSPECT AND PROSPECT 15 Envoi PART VII APPENDICES Appendix A ACM Interview Appendix B CV -- B.1 Early Years -- B.2 Professional Life -- B.3 Awards and Honours -- B.4 Other Professional Activities -- B.5 A Short Photo Album Appendix C Doctoral Students Appendix D List of Tony Hoare's Publications -- References Appendix E Online Resources Author's Biographies Index Abstract freely available; full-text restricted to subscribers or individual document purchasers Also available in print Mode of access: World Wide Web System requirements: Adobe Acrobat Reader HTTP:URL=https://doi.org/10.1145/3477355 Information=Abstract with links to full text
件　名	LCSH:Theories of Programming (Computer Programming) LCSH:Electronic books
書誌ID	EB00004444
ISBN	3477355