- 用TLA+定义系统(TLA+语言与工具在软硬件设计中的应用)/中兴通讯技术丛书/计算机科学丛书
- - 作者：(美)莱斯利·兰伯特|责编:王春华//孙榕舒|译者:董路明//贺志平
  - 出版社：机械工业
  - ISBN：9787111678229
  - 出版日期：2021/04/01
  - 页数：314
- 售价：55.6

内容大纲
本书系统介绍了形式化建模语言TLA+以及模型检查工具TLC，并结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。本书分为五个部分。第一部分包含大多数程序员和工程师需要了解的有关编写系统规约（即建立模型）的所有信息；第二部分包含更高级的示例与材料，供需要进阶的读者使用；第三部分和第四部分为TLA+的参考手册，包括语言本身的数学定义及工具的原理与使用；第五部分介绍在基础TLA+上所演进出的TLA+版本2的新特性和少许变更。
本书适合高级软硬件开发设计人员、测试人员、架构师以及相关学术研究人员阅读。
作者介绍
莱斯利·兰伯特（Lesie Lampot）微软研究院的首席研究员，2013年图灵奖得主，美国国家科学院和国家工程院院士，LaTeX系统刨始人。他是拥有杰出贡献和辉煌成就的计算机大师、分布式系统领域的先锋人物，他的分布式计算理论奠定了计算机学科的基础。他于1978年发表的论文“Time, Clocks, and the Ordering of Events in a Distributed System”至今仍保持着计算机科学史上的被引用量纪录。
目录
出版者的话
译者序
前言
致谢
第一部分  入门
  第1章  简单数学基础
    1.1  命题逻辑
    1.2  集合
    1.3  谓词逻辑
    1.4  公式与陈述句
  第2章  定义一个简单时钟
    2.1  行为
    2.2  时钟
    2.3  解读规约
    2.4  TLA+规约
    2.5  规约的另一种写法
  第3章  异步接口示例
    3.1  第一个规约
    3.2  另一个规约
    3.3  类型回顾
    3.4  定义
    3.5  注释
  第4章  FIFO接口示例
    4.1  内部规约
    4.2  剖析实例化
      4.2.1  实例化是一种代换
      4.2.2  参数化的实例化
      4.2.3  隐式代换
      4.2.4  不需重命名的实例化
    4.3  隐藏内部变量
    4.4  有界FIFO
    4.5  我们在定义什么
  第5章  缓存示例
    5.1  内存接口
    5.2  函数
    5.3  可线性化内存系统
    5.4  元组也是函数
    5.5  递归函数定义
    5.6  直写式缓存
    5.7  不变式
    5.8  证明实现
  第6章  数学基础拓展
    6.1  集合
    6.2  “笨表达式”
    6.3  递归回顾
    6.4  函数与运算符
    6.5  函数使用
    6.6  CHOOSE
  第7章  编写规约：一些建议
    7.1  为什么要编写规约

    7.2  我们要定义什么
    7.3  原子粒度
    7.4  数据结构
    7.5  编写规约的步骤
    7.6  进一步提示
    7.7  定义系统的时机和方法
第二部分  更多高级主题
  第8章  活性和公平性
    8.1  时态公式
    8.2  时态重言式
  ……
第三部分  工具
第四部分  TLA+语言
第五部分  TLA+版本2基础

内容大纲

作者介绍

目录

同类热销排行榜

推荐书目