基本信息

编辑推荐
---------------------------8081330 - 计算机科学的逻辑基础---------------------------
完美实现逻辑与计算机的知识贯通,培养计算机学生数理逻辑思维
---------------------------8070104 - 计算机科学概论(原书第7版)---------------------------
全面介绍计算机科学领域的基础知识,内容翔实、覆盖面广
内容简介
计算机书籍
---------------------------8081330 - 计算机科学的逻辑基础---------------------------
介绍如何将谓词逻辑应用于软件和数字电路的测试和验证,重点是应用而不是理论。
---------------------------8070104 - 计算机科学概论(原书第7版)---------------------------
本书由当今该领域备受赞誉且经验丰富的教育家Nell Dale和John Lewis共同编写,全面介绍计算机科学领域的基础知识,为广大学生勾勒了一幅生动的画卷。就整体而言,全书内容翔实、覆盖面广,旨在向读者展示计算机科学的全貌;从细节上看,本书层次清晰、描述生动,基于计算机系统的洋葱式结构,分别介绍信息层、硬件层、程序设计层、操作系统层、应用程序层和通信层,涉及计算机科学的各个层面。
本书贯穿了计算机系统的各个方面,非常适合作为计算机专业的计算机导论课程教材,为后续专业课程打下坚实的基础;同时还适合作为非计算机专业的计算机总论课程教材,提供计算机系统全面完整的介绍。
作译者
---------------------------8070104 - 计算机科学概论(原书第7版)---------------------------
[美] 内尔·黛尔(Nell Dale)/得克萨斯大学奥斯汀分校约翰·路易斯(John Lewis)/弗吉尼亚理工大学著:内尔•黛尔(Nell Dale) 计算机科学领域广受推崇的教育家。在得克萨斯大学奥斯汀分校执教的二十多年中,她编写了四十多本计算机科学方面的本科生教材。她于得克萨斯大学奥斯汀分校获得了硕士学位和计算机科学博士学位。由于在计算机科学领域做出了卓越贡献,她于1996年获得了ACM SIGCSE计算机科学教育杰出贡献奖,于2001年获得了ACM Karl Karlston杰出教师奖。她于2010年被选为ACM会士。
约翰•路易斯(John Lewis) 计算机科学领域著名的教育家和作家。他编写的Java软件及程序设计教材十分畅销。他于弗吉尼亚理工大学获得博士学位,并曾在维拉诺瓦大学计算机科学系执教14年,现任教于弗吉尼亚理工大学。执教期间,他获奖无数,包括大学卓越教学奖和Goff杰出教学奖。他的研究兴趣包括面向对象技术、多媒体和软件工程。
目录
8070104 - 计算机科学概论(原书第7版) - 9787111654629 - 机械工业出版社 - 定价 99
8081330 - 计算机科学的逻辑基础 - 9787111682226 - 机械工业出版社 - 定价 99
---------------------------8081330 - 计算机科学的逻辑基础---------------------------
出版者的话
译者序
前言
第一部分 逻辑与等式
第1章 计算机系统:原理简单,行为复杂 2
1.1 硬件与软件 2
1.2 程序的结构 4
1.3 深蓝与归纳定义 7
习题 10
第2章 布尔公式和等式 11
2.1 利用等式推理 11
前言
---------------------------8081330 - 计算机科学的逻辑基础---------------------------
计算机是一种行为逻辑。计算机组件归根到底就是公式的逻辑实现方式,当这些组件被布尔信号激活时,就会计算其所表示公式的实际取值。软件也是一种逻辑体现。一个软件组件就是一种具有逻辑支撑的形式语言编写规范,某些软件组件其实就是代数公式。公式系统无论多么庞大复杂,也只是一些公式而已。
因此,学习计算机科学的人们可以从逻辑学习中获益,并且大多数计算机科学专业的学生在接受教育时都会接触到逻辑。这种接触通常以离散数学课程中的若干讲座和问题集的形式出现。学生看到的逻辑应用通常与传统数学的关系更加紧密,与计算机科学的关系则较为松散。即使对于“计算机科学中的离散数学”这样的课程而言,计算机科学部分也通常与编写解决传统数学问题的程序有关,而不是与计算机科学的概念有关。我们认为,如果计算机科学专业的学生对逻辑以及他们所选择的学习领域中的逻辑应用有更广泛、更严谨、更充分的认识,他们将会受益匪浅。因此,本书中的所有例子都来自计算机科学中的问题。
本书直接关注与计算机科学相关的中心主题。本书以逻辑为框架,对这些主题展开讨论,并将逻辑用于解决计算机科学领域的问题,包括硬件组件、软件组件、测试和验证以及算法分析。我们从归纳证明连接列表的软件组件的重要性质开始,然后继续验证许多其他软件和硬件组件的性质,而不是通过证明数列求和公式的方式来阐述数学归纳法。这是同样古老的数学归纳法,但是它呈现在计算机科学专业学生感兴趣的主题背景下。归纳逻辑属于前沿领域,数值代数的诀窍揭示了归纳逻辑的奥秘,许多归纳法的练习则需要以数学家深感兴趣的研究主题为基础进行讨论。
我们希望读者愿意付出大量努力,按顺序学习大学几十个课时的课程内容,理解计算机科学中的一些重要问题,并通过形式推理的方式尝试解决很多这样的问题。形式主义是本书的标语,甚至可以使用基于半自动化证明引擎ACL2的机械化逻辑。ACL2可以检查证明过程中的每个细节,有时可以补充传统数学证明,甚至严格数学证明留下的空白。
本书采用三种形式化表示法:传统的命题和谓词逻辑代数公式(偶尔有一些数值代数)表示法、数字电路图表示法以及在语法上类似于编程语言Lisp的ACL2表示法(ACL2被嵌入在可辅助生成一阶逻辑形式证明的机械化逻辑之中)。ACL2是一种数学符号,所有材料都可以通过传统的手工推理方式来理解,而无须将模型输入计算机系统。对于想要了解形式化操作的读者,本书还介绍了Proof Pad(简化版ACL2)环境。ACL2专家使用emacs或ACL2 Sedan作为界面,读者可以根据需要使用这些工具。本书还说明了Proof Pad框架中的过程,根据我们的经验,这对初学者而言也不是负担。在任何情况下,Proof Pad都足以支持对本书的学习。
我们选择了ACL2作为这本书的证明引擎,因为根据我们的判断,ACL2提供了比任何其他工具更容易理解的机械化逻辑证明形式。我们不指望每个读者都能成为有经验的ACL2用户,更不用说成为ACL2专家了。我们将ACL2引入讨论中,以显示软件和硬件工程师是如何从逻辑(包括机械化逻辑)中受益的。想要在大型项目中运用ACL2优势的读者,则需要在本书介绍的内容之外更为深入地了解ACL2或其他机械化逻辑。在前些年,我们在课堂上讲授逻辑时并未介绍机械化逻辑,然而根据经验,我们发现当使用能够检查证明和帮助处理细节的工具来支持这些形式化方法时,大多数学生都会感到更顺利且更有动力。
逻辑是本书的中心主题,但不是唯一的主题。对计算机科学更多主题感兴趣的读者会发现很多有用的资料。本书可以为认真学习计算机科学的学生和其他领域想要了解计算机科学的学生打下坚实的基础。本书的早期版本已被作者和其他讲师多次用作面向计算机科学以及其他专业学生的两门课程“计算机科学逻辑”和“计算机科学导论”的主要教材。本书也被用作计算机科学专业学生的离散数学课程的补充教材。本书在上述三个教学方面都发挥了很好的作用。
学习本书不需要大学预科课程或高中数学课程之外的预备知识。当然,如果了解一些高等代数知识会有所帮助,但不需要有几何、三角学或微积分方面的知识。编程经验也不是必需的,基于等式的方法可以为演示提供信息,让有或没有编程经验的人都可以学习本书内容。目标是证明自己已经知道这些知识的学生会惊讶地发现,其实自己以前并不知道这些知识,而那些背景知识较少的学生则从一开始就应当进行必要的努力。
学习本书的内容绝非易事。学生将需要进行很多艰苦的思考才能完成几十个练习,而且他们还需要再完成几十个练习才能掌握这些概念。仅仅看书是不够的,全书练习(总共超过180题)为学生提供了解决问题的机会。幸运的是,如果过往学生的学习体会是一个可靠的衡量标准,那么无论是从即刻满足感,还是从长期收益来看,学习本书都有回报。希望读者能够心情愉悦地阅读本书,并希望他们在后续做其他项目时发现自己所学的内容会对手头上的工作有所启发。
预备知识和章节相关性在整个演示过程中,公式为严谨、形式化的方法提供了基础。理解等式只需要有高中代数基础,不需要其他预备知识。另外,有等式编程基础对理解本书十分有利。有关计算实践的章节更侧重于描述性,而不是严谨的形式化分析、讨论。读者可以对这些主题进行任意排列,并且可以延缓将挑战性概念引入等式和推理的进程。下图阐明了本书相关章节的关联路径。
致谢作者想要感谢Caleb Eggensperger开发的Proof Pad环境,学生可以通过该环境获得机械化逻辑的早期经验,从而减轻了许多负担。感谢Carl Eastland、Dale Vaillancourt和Matthias Felleisen 建立了ACL2环境,其中一位作者在许多课程中都使用该环境,其中包括DoubleCheck——它是基于谓词的自动测试设备,是John Hughes和Koen Claessen基于QuickCheck(此类工具的祖先)中的理念而发明的,该设备后来被合并到Proof Pad中。我们感谢他们的开拓性工作。Qi Cheng在应用逻辑课程中使用了本书的原型版本,并提出了改进建议,使本书更加完善。作者还想要感谢1000多名学生,他们投身于本书的早期版本中,并提供了反馈。谢谢大家。
Rex Page和Ruben Gamboa
2018年1月
媒体评论
---------------------------8081330 - 计算机科学的逻辑基础---------------------------
数理逻辑之于计算机科学就像微积分之于物理。如果你真的想了解计算机科学,让这本书成为你的指南。
—— J. Strother Moore,得克萨斯大学奥斯汀分校荣休讲席教授
许多其他书将逻辑作为研究对象。相反,这本书以引人入胜的语言说明了逻辑如何在计算机科学中发挥作用,涵盖了从计算基础到程序设计、测试和验证的各种逻辑的使用。作为奖励,这本书使用了一个机械化逻辑系统,允许读者用形式化的方法进行实验。
——Veronica Gaspes,哈尔姆斯塔德大学副教授
你有没有想过逻辑和数学为什么会如此重要? Page和Gamboa通过生动地说明计算机科学如何基于逻辑进行工作的基本过程,带你踏上一段奇妙的学习旅程。你可以了解到数据结构、数字电路、排序、分片和MapReduce如何工作以及为什么工作,并且可以使用机械化逻辑证明这些工作的正确性。这是信息时代人们的基本知识。
—— Marco T. Morazán,西东大学教授
Page和Gamboa提供了一本优美、清晰、优雅的教材,向有抱负的软件开发人员介绍了软件背后的基础数学。基于本书开设一门课程将有助于学生进行学习。
—— Robby Findler,西北大学教授
---------------------------8070104 - 计算机科学概论(原书第7版)---------------------------