文件名称:
LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems
开发工具:
文件大小: 2mb
下载次数: 0
上传时间: 2017-10-18
详细说明： 英文原版 Preface to the second edition Our motivation for (re)writing this book One of the leitmotifs of writing the first edition of our book was the observation that most logics used in the design, specification and verification of computersystems fundamentally de al with a satisfaction relation M φ where M is some sort of situation or model of a system, and φ is a specification, a formula of that logic, expressing what should be true in situation M. At the heart of this set-up is that one can often specify and implement algorithms for computing . We developed this theme forpr opositional, first-order, temporal, modal, and program logics. Based on the encouraging feedback received from five continents we are pleased to hereby present the second edition of this text which means to preserve and improve on the original intent of the first edition. What’s new and what’s gone Chapter1 now discusses the design, correctness, and complexity of a SAT solver (a marking algorithm similar to St˚almarck’s method [SS90]) for full propositional logic. Chapter 2 now contains basic results from model theory (Compactness Theorem and L¨owenheim–Skolem Theorem); a section on the transitive closure and the expressiveness of existential and universal second-order logic; and a section on the use of the object modelling language Alloy and its analyserforsp ecifying and exploring under-specified first-orderlogic models with respect to properties written in first-order logic with transitive closure. The Alloy language is executable which makes such exploration interactive and formal. Chapter 3 has been completely restructured. It now begins with a discussion of linear-time temporal logic; features the open-source NuSMV modelchecking tool throughout; and includes a discussion on planning problems, more material on the expressiveness of temporal logics, and new modelling examples. Chapter 4 contains more material on total correctness proofs and a new section on the programming-by-contract paradigm of verifying program correctness. Chapters 5 and 6 have also been revised, with many small alterations and corrections. The interdependence of chapters and prerequisites The book requires that students know the basics of elementary arithmetic and naive set theoretic concepts and notation. The core material of Chapter1 (everything except Sections 1.4.3 to 1.6.2) is essential forall of the chapters that follow. Otherthan that, only Chapter6 depends on Chapter3 and a basic understanding of the static scoping rules covered in Chapter 2 – although one may easily coverSections 6.1 and 6.2 without having done Chapter 3 at all. Roughly, the interdependence diagram of chapters is 1 2 3 4 5 6 WWW page This book is supported by a Web page, which contains a list of errata; text files for all the program code; ancillary technical material and links; all the figures; an interactive tutor based on multiple-choice questions; and details of how instructors can obtain the solutions to exercises in this book which are marked with a ∗. The URL forthe book’s page is www.cs.bham.ac.uk/research/lics/. See also www.cambridge.org/ 052154310x ...展开收缩
(系统自动生成,下载前可以参看下载内容)
下载文件列表
相关说明
- 本站资源为会员上传分享交流与学习,如有侵犯您的权益,请联系我们删除.
- 本站是交换下载平台，提供交流渠道，下载内容来自于网络，除下载问题外，其它问题请自行百度。
- 本站已设置防盗链，请勿用迅雷、QQ旋风等多线程下载软件下载资源，下载后用WinRAR最新版进行解压.
- 如果您发现内容无法下载，请稍后再次尝试；或者到消费记录里找到下载记录反馈给我们.
- 下载后发现下载的内容跟说明不相乎，请到消费记录里找到下载记录反馈给我们，经确认后退回积分.
- 如下载前有疑问，可以通过点击"提供者"的名字，查看对方的联系方式，联系对方咨询.
