新書推薦：
《
《中国版画史》
》
售價：NT$
493.0
《
最后一章
》
售價：NT$
381.0
《
20世纪中国工艺美术史（上下卷）
》
售價：NT$
2789.0
《
为何只有我们：语言与演化（语言学及应用语言学名著译丛）
》
售價：NT$
325.0
《
巴西史（区域国别史丛书）
》
售價：NT$
549.0
《
科学实验与编程（Python版）
》
售價：NT$
330.0
《
直升机突击：美国陆军航空兵：1962—1973
》
售價：NT$
783.0
《
东方美学口袋书 中国颜色
》
售價：NT$
223.0
|
| 編輯推薦： |
|
本书全面介绍了时序逻辑和作者开发的反应式程序的计算模型，是该领域的经典和权威著作。
|
| 內容簡介： |
|
反应式和并发系统指实时运行的计算系统，如操作系统、控制系统、交互系统和并发系统。这些系统很难规约、实现和验证，主要原因是系统与其环境之间及系统本身的并行进程之间交互的复杂性，在交互时间上的微小变化可能导致完全不同的行为。 时序逻辑是一种形式化规约语言，可用于刻画和分析反应式系统中有关时间和行为方面的属性。它提供了一种简单、自然但精确的方式来讨论交互发生的顺序，而无须采用绝对时间度量。 本书全面介绍了时序逻辑和作者开发的反应式程序的计算模型。 本书是国际著名计算机科学家Zohar Manna和Amir Pnueli（图灵奖得主）的代表作，适合作为计算机、软件工程、人工智能、自动化等专业高年级本科生、研究生的教材或参考书，也可供相关领域的研究人员和技术开发人员参考。
|
| 目錄：
|
第Ⅰ部分并 发 模 型
第1章基本模型
1.1通用模型
1.1.1基础语言
1.1.2基本转换系统
1.1.3转换关系ρτ
1.1.4使能与非使能转换
1.1.5空转换与勤勉转换
1.1.6计算
1.1.7具体模型
1.2模型1： 转换图
1.2.1声明
1.2.2进程
1.2.3基本转换系统图
1.2.4用交错表示并发性
1.2.5调度
1.3模型2： 共享变量文本
1.3.1简单语句
1.3.2复合语句
1.3.3程序
1.3.4文本程序中的标记
1.3.5标记等价关系
1.3.6文本语言中的位置
1.4共享变量文本语义
1.4.1状态变量和状态
1.4.2转换
1.4.3初始条件
1.4.4计算
1.4.5下标变量
1.5语句间的结构关系
1.5.1子语句
1.5.2控制谓词at、after和in
1.5.3语句的使能性
1.5.4进程和并行语句
1.5.5竞争语句
1.6行为等价
1.6.1初步近似
1.6.2可观测和可简化的行为
1.6.3转换系统的等价性
1.6.4语句一致性
1.6.5例子
1.6.6模拟与实现
1.7分组语句
1.7.1分组语句
1.7.2与分组语句关联的转换
1.8信号量语句
1.8.1信号量需求
1.8.2信号量语句
1.8.3互斥信号量的应用
1.8.4信号量的其他应用
1.9区域语句
1.9.1比较信号量和区域语句
1.9.2选择语句中的同步
1.10模型3： 消息传递文本
1.10.1通信语句
1.10.2缓冲能力
1.10.3例子
1.10.4条件通信语句
1.10.5同步模型和异步模型的比较
1.10.6公平服务器
1.11模型4： Petri网
1.11.1网
1.11.2标记
1.11.3图形化表示
1.11.4点火
1.11.5Petri系统
1.11.6例子
问题
文献注释
第2章真并发模型
2.1交错和并发
2.1.1重叠执行
2.1.2交错计算
2.1.3细粒度
2.2限制临界引用
2.2.1临界引用
2.2.2语句的LCR约束
2.2.3LCR程序
2.2.4需要额外保护
2.2.5每个程序都有一个LCR精化
2.2.6每个程序都有一个LCR等价
2.2.7语义临界引用
2.2.8合并语句
2.2.9with语句
2.3弱公平性
2.3.1公平性需求
2.3.2不公平计算
2.3.3弱公平性
2.3.4弱公平性需求
2.4弱公平性需求的含义
2.4.1不能保证选择公平性
2.4.2转换弱公平性与进程弱公平性
2.4.3弱公平性调度
2.4.4不能检测弱公平性
2.4.5非公平转换
2.5强公平性
2.5.1弱公平性不足
2.5.2强公平性需求
2.5.3强公平性调度
2.6同步语句
2.7通信语句
2.7.1同步通信互斥
2.7.2异步通信互斥
2.8总结: 公平转换系统
2.9Petri网公平性
2.9.1弱公平性
2.9.2非一元网转换的强公平性
2.9.3互斥
2.10公平性语义
2.10.1公平性防止有限区分
2.10.2公平性和随机选择
问题
文献注释
第Ⅱ部分规约
第3章时序逻辑
3.1状态公式
3.1.1状态语言
3.1.2状态公式语义
3.2时序公式： 将来算子
3.3时序公式： 过去算子
3.3.1简单例子
3.3.2可满足性和有效性
3.3.3等价性、一致性和蕴涵性
3.3.4可替换性
3.3.5过去公式和将来公式
3.3.6的较弱形式
3.3.7算子的基本集合
3.3.8限制型算子
3.4时序算子的基本属性
3.4.1模式及其有效性
3.4.2单调性
3.4.3自反性
3.4.4限制性
3.4.5扩展性
3.4.6对偶性
3.4.7强算子和弱算子
3.4.8幂等性
3.4.9吸收性
3.4.10上一时刻和下一时刻的交换性
3.4.11全称算子和存在算子
3.4.12引用变量的下一个值和前一个值
3.4.13语义弱公平性
3.5证明系统
3.6证明系统公理
3.6.1将来公理
3.6.2过去公理
3.6.3混合公理
3.6.4状态重言式公理
3.7基本推理规则
3.7.1泛化规则和特指规则
3.7.2替换规则
3.7.3分离规则
3.8导出规则
3.8.1指定规则
3.8.2命题推理规则
3.8.3蕴涵分离规则
3.8.4蕴涵命题推理规则
3.8.5从蕴涵到规则
3.8.6证明举例
3.9等词和量词
3.9.1参数化的句子符号
3.9.2带参数模式的规则GEN
3.9.3带量词公式的规则INST
3.9.4变量替换
3.9.5等词公理
3.9.6框架公理
3.9.7证明举例
3.9.8变量的下一个值和前一个值
3.9.9量词公理
3.9.10量词规则
3.9.11证明举例
3.10从一般有效性到程序有效性
3.10.1计算对应的模型
3.10.2程序有效性和状态有效性
3.10.3扩展演绎系统
3.10.4建立P状态有效性
3.10.5建立P有效性
3.10.6程序依赖规则
3.10.7导出规则
3.10.8时序语义公理
问题
文献注释
第4章程序属性
4.1局部语言
4.1.1位置谓词
4.1.2转换的使能性
4.1.3终止谓词
4.1.4转换谓词
4.1.5通信谓词
4.1.6规约变量
4.2属性分类
4.2.1安全性
4.2.2保证性
4.2.3义务性
4.2.4响应性
4.2.5持续性
4.2.6反应性
4.2.7反应性类是最大的类
4.2.8分类
4.2.9标准公式
4.2.10安全性活性分类
4.3安全性例子： 状态不变性
4.3.1全局不变性
4.3.2部分正确性
4.3.3无死锁性
4.3.4局部无死锁性
4.3.5容错性
4.3.6互斥性
4.3.7通信事件的不变性
4.4安全性例子： 过去不变性
4.4.1单调性
4.4.2缺乏主动响应
4.4.3无重复输出
4.4.4先进先出
4.4.5严格优先性
4.4.6有界超越
4.5进展性例子： 从保证性到反应性
4.5.1终止性和完全正确性
4.5.2保证性事件
4.5.3间歇断言
4.5.4无个体饥荒和无活锁
4.5.5可访问性
4.5.6确保响应
4.5.7最终有界性
4.5.8表示公平性需求
4.5.9最终可靠性
4.6例子： 资源分配
4.6.1消息传递方式
4.6.2消息传递方式的安全性
4.6.3消息传递方式的进展性
4.6.4共享变量方式
4.6.5共享变量方式的安全性
4.6.6共享变量方式的进展性
4.7规约语言表达能力
4.7.1观察奇偶性
4.7.2量词公式描述奇偶性
4.7.3有重复输入的缓冲
4.7.4量词公式描述缓冲
4.7.5通信历史变量
4.8反应模块规约
4.8.1模块语句
4.8.2模块规约
4.8.3执行模块的任务
4.8.4模块实现的障碍
4.8.5模块的计算
4.9复合模块规约
4.9.1层次分解
4.9.2更改超越一次的变量
4.9.3分解安全性规约
4.9.4异步通信模块
4.9.5同步通信模块
4.9.6资源重新分配
问题
文献注释
参考文献
|
| 內容試閱：
|
本书的一些图示、符号、黑体、斜体沿用了英文原书的排版风格，特此声明。
本书是关于反应式程序及其控制的系统，以及应用时序逻辑工具对此类程序进行形式规约、验证和开发的方法学。
反应式程序与其环境保持不断的交互作用，而不是在计算终止时产生一些最终结果。反应式程序包括大多数在正确性和可靠性方面特别具有挑战性的程序，如并发和实时程序、嵌入式和过程控制程序、操作系统等。
并发性是反应式程序的一个基本特征。根据定义，反应式程序与其环境并发运行，本书研究的大多数示例程序都是由几个并发执行的进程组成的并发程序。提出的技术通常用于描述和分析此类程序的并发元素间的交互。因此，本书的主题是对交互的研究和分析，既包括程序与其环境之间的交互，也包括程序中并发进程之间的交互。
许多案例已经充分证明，构造正确、可靠的反应式程序是非常具有挑战性的。看似无关紧要的小型并发程序往往会表现出完全意想不到的行为，在某些情况下，这些行为可能导致关键系统崩溃。这就是为什么说本书提倡的形式化方法对于反应式程序领域正确程序的开发如此重要。
形式化方法通常包含两方面： 其一是规约语言，用于形式描述程序的预期需求； 其二是一系列证明方法，通过这些方法，可以形式验证程序相对于其规约的正确性。形式化方法的优势是显而易见的。形式规约要求程序设计者对程序的主要功能尽早做出精确的决定，并消除对其预期行为描述中的歧义。对所需属性的形式验证保证了该属性在程序的所有可能执行中均成立。
本书选择时序逻辑作为规约语言，因为它能够有效描述反应式程序的动态行为，并刻画其属性。时序语言的主要优点是通过使用一组特殊算子，为程序属性提供有效和自然的表达方式。
本书采用大量篇幅对时序逻辑进行全面和自含的介绍，并阐述如何用它来刻画反应式系统的属性。
面向读者和预备知识
本书面向对反应式系统的设计、构造和分析感兴趣，以及希望学习时序逻辑语言和如何将其应用于反应式系统的规约、验证和开发的人员。
假定读者具备下列基础： 熟悉编程和编程语言并有一定的经验，特别是对程序并发执行的基本概念有一定的了解； 理解一阶逻辑及演绎系统的有效性和可证明性的概念。本书不需要预先了解时序逻辑的预备知识，也不需要详细了解任何特定编程语言，因为本书将介绍这两个主题。
主要内容
本书共4章，介绍反应式程序的计算模型和编程语言，以及时序逻辑规约语言。
第1章介绍计算模型和编程语言。在编程语言中，尽可能全面给出并发进程之间通信和同步的主要机制表示。语言允许进程通过共享变量和消息传递进行通信。本书的目的是提出一个统一的方法来实现反应式程序中的通信，这种方法独立于采用的特定通信机制。因此，将给出并发编程中的一些核心范例（如互斥或生产者消费者）是如何根据共享变量或不同形式的消息传递来编程的。
第2章进一步阐述计算模型。书中使用的计算模型通过交错执行从并行进程中一次执行一个原子操作来表示并发性。这一章将考查这种表示与程序的真并发执行（几个并行语句同时执行）是否相符的问题。通过对研究的程序施加语法限制并引入公平性需求，确保程序的交错并发执行与真并发执行之间的准确对应。
第3章介绍时序逻辑，给出其语法和语义。时序语言包含两组对称的时序算子，一组处理将来，另一组处理过去。列出并讨论时序算子的许多属性。演绎证明系统提供了时序属性推导的形式化方法。
第4章探讨时序逻辑作为一种描述反应式程序属性语言的实用性。程序属性根据它们在时序逻辑中的表示被划分为不同层次的类。最重要的类是安全性、响应性和反应性。对每一类都提供了一组常见的程序属性示例。此外，还探讨了模块规约，其中程序的每个模块（进程）是独立描述的。
第1、2章构成第Ⅰ部分，第3、4章构成第Ⅱ部分。
本书的教学
本书的内容可作为不同层次的计算机科学基础课程，适合一学期的教学，该课程可在本科高年级或研究生阶段开设。
快速阅读
本书中有部分章节对于理解主要内容不是必要的，如果想精简课程内容，那么下列章节可以先忽略或作为扩展阅读： 1.2节、1.6节、1.11节； 2.9节、2.10节； 4.7节~4.9节。
问题
每一章结尾都有一组问题作为练习。有些问题是为了测试读者对这一章内容的理解程度，有些问题介绍了这一章没有涉及的材料，还有一些问题探索了一些主题的介绍和发展方式的替代方案。
这些问题按难易程度分级。困难问题标注*，研究级问题标注**。
为了指出这些问题属于书中的哪些部分，在书中对应位置进行了注释。在解决问题时，读者可以使用在注释之前出现在正文中的任何结果，也可以使用该问题前任何问题的结果及同一问题的前面部分的结果。
文献注释
每章之后有一个简短的文献注释，提及一些与这一章涵盖的主题相关的研究贡献。尽管我们认真地参考了所有重要的相关工作，但仍可能有遗漏，对此我们表示歉意并欢迎任何批评和指正。
支持系统
向读者推荐Macintosh上的一个程序，该程序用于检验命题时序公式的有效性，对有关时序逻辑的练习很有帮助。有关获取系统的信息可以写信到以下地址：
Temporal Prover
Box 9215
Stanford， CA 94309
致谢
许多同事和学生阅读了本书的初稿和多个（几乎不计其数）版本，并给出有益的意见和建议，对此我们十分感谢。特别感谢Rajeev Alur、Eddie Chang、Avraham Ginzburg、David Gries、Tom Henzinger、Daphne Koler、Narciso MartiOliet、Roni Rosner、Richard Waldinger 和Liz Wolf的帮助和建议。
也非常感谢斯坦福大学和以色列魏茨曼学院的学生提出的具体意见和有益的批评。
感谢空军科研办公室、先进防御研究项目机构、国家科学基金和欧洲共同体Esprit项目对本书中的研究提供的经费支持。
Sarah Fliegelman对本书的排版工作做得非常出色。Joe Weening提供了TEX排版方面非常宝贵的详细技术知识和专业技能。
Eric Muller花费了大量时间耐心地准备了所有计算机生成的图表。Yehuda Barbut提供了手工绘图。
Rajeev Alur为问题的编写提供了特别协助。
Roni Rosner为文献注释的准备给予大量的帮助。
特别感谢Carron Kirkwood为本书设计的封面。
斯坦福大学Zohar Manna
以色列魏茨曼学院Amir Pnueli
|
|
購物車/收銀台(
0
) | 在線留言板
| 付款方式
| 聯絡我們
| 運費計算
| 幫助中心 |
加入書簽
HOME
新書上架
