微信扫一扫,移动浏览光盘
简介
本书的主题为“程序设计方法学”,或称为“程序设计科学”,“程序设计逻辑”,“程序设计理论”,“程序开发形式化方法”,或“程序证明”,它涉及程序设计中经得起数学证明的那些方面。一个好的理论能帮助我们书写精确的规范,并设计出其执行可被证明满足规范的程序。本书介绍作者多年研究出的一套简单并且通用的程序设计理论,它可同时适用于终止和非终止计算,顺序和并行计算,以及独立和交互式计算,该理论的基础在于将规范表示成布尔表达式,而布尔表达式的变量可以是任何感兴趣的变量,包括只对其初值和终值感兴趣的变量、对其值始终感兴趣的变量、只知道其可能值的变量和用于计算时间和空间的变量等,其中还将考虑计算的状态、计算的时间、计算的空间以及计算的交互等。
目录
中译本序
第0章 绪言
0.0 引言
0.1 当前版本
0.2 快速浏览
0.3 致谢
第1章 基本理论
1.0 布尔理论
1.0.0 公理和证明规则
1.0.1 表达式和证明格式
1.0.2 单调性和反单调性
1.0.3 上下文
1.0.4 形式化
1.1 数论
1.2 字符理论
第2章 基本数据结构
2.0 束论
2.1 集合论
2.2 串论
2.3 表论
2.3.0 多维结构
第3章 函数理论
3.0 函数
3.0.0 简化的函数记号
3.0.1 作用域和置换
3.1 量词
3.2 函数若干点讨论
3.2.0 函数包含和相等
3.2.1 高阶函数
3.2.2 函数组合
3.3 表作为函数
3.4 极限与实数
第4章 程序理论
4.0 规范
4.0.0 规范记号
4.0.1 规范定律
4.0.2 精化
4.0.3 条件
4.0.4 程序
4.1 程序开发
4.1.0 精化定律
4.1.1 表求和
4.1.2 二的指数幂
4.2 时间
4.2.0 真实时间
4.2.1 递归时间
4.2.2 终止问题
4.2.3 可靠性与完备性
4.2.4 线性查找
4.2.5 二分查找
4.2.6 快速指数运算
4.2.7 斐波那契数
4.3 空间
4.3.0 最大空间
4.3.1 平均空间
第5章 程序设计语言
5.0 作用域
5.0.0 变量说明
5.0.1 变量悬挂
5.1 数据结构
5.1.0 数组
5.1.1 记录
5.2 控制结构
5.2.0 while循环
5.2.1 包含退出的循环
5.2.2 二维查找
5.2.3 for循环
5.2.4 转向
5.3 时间与空间依赖
5.4 断言
5.4.0 检查
5.4.1 回溯
5.5 子程序
5.5.0 result表达式
5.5.1 函数
5.5.2 过程
5.6 别名
5.7 概率程序设计
5.7.0 随机数产生器
5.7.1 信息
5.8 函数式程序设计
5.8.0 函数精化
第6章 递归定义
6.0 递归数据定义
6.0.0 构造和归纳
6.0.1 最小不动点
6.0.2 递归数据构造
6.1 递归程序定义
6.1.0 递归程序构造
6.1.1 循环定义
第7章 理论设计与实现
7.0 数据理论
7.0.0 数据-堆栈理论
7.0.1 数据-堆栈实现
7.0.2 简单数据-堆栈理论
7.0.3 数据-队列理论
7.0.4 数据-树理论
7.0.5 数据-树实现
7.1 程序理论
7.1.0 程序-堆栈理论
7.1.1 程序-堆栈实现
7.1.2 复杂程序-堆栈理论
7.1.3 弱程序-堆栈理论
7.1.4 程序-队列理论
7.1.5 程序-树理论
7.2 数据转换
7.2.0 安全开关
7.2.1 取一个数
7.2.2 语法分析
7.2.3 有界队列
7.2.4 可靠性与完备性
第8章 并发
8.0 独立组合
8.0.0 独立组合定律
8.0.1 表并发
8.1 顺序到并行的转换
8.1.0 缓冲区
8.1.1 插入排序
8.1.2 哲学家就餐问题
第9章 交互
9.0 交互变量
9.0.0 自动调温器
9.0.1 空间
9.1 通信
9.1.0 可实现性
9.1.1 输入和输出
9.1.2 通信计时
9.1.3 递归定义的通信
9.1.4 合并
9.1.5 监控器
9.1.6 反应控制器
9.1.7 信道声明
9.1.8 死锁
9.1.9 广播
第10章 练习
10.0 基本理论
10.1 基本数据结构
10.2 函数理论
10.3 程序理论
10.4 程序设计语言
10.5 递归定义
10.6 理论设计与实现
10.7 并发
10.8 交互
第11章 参考
11.0 释疑
11.0.0 记号
11.0.1 布尔理论
11.0.2 束论
11.0.3 串论
11.0.4 函数理论
11.0.5 程序理论
11.0.6 程序设计语言
11.0.7 递归定义
11.0.8 理论设计与实现
11.0.9 并发
11.0.10 交互
11.1 来源
11.2 参考文献
11.3 词语对照与索引
11.4 公理和定律
11.4.0 布尔
11.4.1 通用符号
11.4.2 数
11.4.3 束
11.4.4 集合
11.4.5 串
11.4.6 表
11.4.7 函数
11.4.8 量词
11.4.9 极限
11.4.10 规约与程序
11.4.11 置换
11.4.12 条件
11.4.13 精化
11.5 名字
11.6 符号
11.7 优先级
11.8 分配性
译后记
第0章 绪言
0.0 引言
0.1 当前版本
0.2 快速浏览
0.3 致谢
第1章 基本理论
1.0 布尔理论
1.0.0 公理和证明规则
1.0.1 表达式和证明格式
1.0.2 单调性和反单调性
1.0.3 上下文
1.0.4 形式化
1.1 数论
1.2 字符理论
第2章 基本数据结构
2.0 束论
2.1 集合论
2.2 串论
2.3 表论
2.3.0 多维结构
第3章 函数理论
3.0 函数
3.0.0 简化的函数记号
3.0.1 作用域和置换
3.1 量词
3.2 函数若干点讨论
3.2.0 函数包含和相等
3.2.1 高阶函数
3.2.2 函数组合
3.3 表作为函数
3.4 极限与实数
第4章 程序理论
4.0 规范
4.0.0 规范记号
4.0.1 规范定律
4.0.2 精化
4.0.3 条件
4.0.4 程序
4.1 程序开发
4.1.0 精化定律
4.1.1 表求和
4.1.2 二的指数幂
4.2 时间
4.2.0 真实时间
4.2.1 递归时间
4.2.2 终止问题
4.2.3 可靠性与完备性
4.2.4 线性查找
4.2.5 二分查找
4.2.6 快速指数运算
4.2.7 斐波那契数
4.3 空间
4.3.0 最大空间
4.3.1 平均空间
第5章 程序设计语言
5.0 作用域
5.0.0 变量说明
5.0.1 变量悬挂
5.1 数据结构
5.1.0 数组
5.1.1 记录
5.2 控制结构
5.2.0 while循环
5.2.1 包含退出的循环
5.2.2 二维查找
5.2.3 for循环
5.2.4 转向
5.3 时间与空间依赖
5.4 断言
5.4.0 检查
5.4.1 回溯
5.5 子程序
5.5.0 result表达式
5.5.1 函数
5.5.2 过程
5.6 别名
5.7 概率程序设计
5.7.0 随机数产生器
5.7.1 信息
5.8 函数式程序设计
5.8.0 函数精化
第6章 递归定义
6.0 递归数据定义
6.0.0 构造和归纳
6.0.1 最小不动点
6.0.2 递归数据构造
6.1 递归程序定义
6.1.0 递归程序构造
6.1.1 循环定义
第7章 理论设计与实现
7.0 数据理论
7.0.0 数据-堆栈理论
7.0.1 数据-堆栈实现
7.0.2 简单数据-堆栈理论
7.0.3 数据-队列理论
7.0.4 数据-树理论
7.0.5 数据-树实现
7.1 程序理论
7.1.0 程序-堆栈理论
7.1.1 程序-堆栈实现
7.1.2 复杂程序-堆栈理论
7.1.3 弱程序-堆栈理论
7.1.4 程序-队列理论
7.1.5 程序-树理论
7.2 数据转换
7.2.0 安全开关
7.2.1 取一个数
7.2.2 语法分析
7.2.3 有界队列
7.2.4 可靠性与完备性
第8章 并发
8.0 独立组合
8.0.0 独立组合定律
8.0.1 表并发
8.1 顺序到并行的转换
8.1.0 缓冲区
8.1.1 插入排序
8.1.2 哲学家就餐问题
第9章 交互
9.0 交互变量
9.0.0 自动调温器
9.0.1 空间
9.1 通信
9.1.0 可实现性
9.1.1 输入和输出
9.1.2 通信计时
9.1.3 递归定义的通信
9.1.4 合并
9.1.5 监控器
9.1.6 反应控制器
9.1.7 信道声明
9.1.8 死锁
9.1.9 广播
第10章 练习
10.0 基本理论
10.1 基本数据结构
10.2 函数理论
10.3 程序理论
10.4 程序设计语言
10.5 递归定义
10.6 理论设计与实现
10.7 并发
10.8 交互
第11章 参考
11.0 释疑
11.0.0 记号
11.0.1 布尔理论
11.0.2 束论
11.0.3 串论
11.0.4 函数理论
11.0.5 程序理论
11.0.6 程序设计语言
11.0.7 递归定义
11.0.8 理论设计与实现
11.0.9 并发
11.0.10 交互
11.1 来源
11.2 参考文献
11.3 词语对照与索引
11.4 公理和定律
11.4.0 布尔
11.4.1 通用符号
11.4.2 数
11.4.3 束
11.4.4 集合
11.4.5 串
11.4.6 表
11.4.7 函数
11.4.8 量词
11.4.9 极限
11.4.10 规约与程序
11.4.11 置换
11.4.12 条件
11.4.13 精化
11.5 名字
11.6 符号
11.7 优先级
11.8 分配性
译后记
Practical theory of programming
光盘服务联系方式: 020-38250260 客服QQ:4006604884
云图客服:
用户发送的提问,这种方式就需要有位在线客服来回答用户的问题,这种 就属于对话式的,问题是这种提问是否需要用户登录才能提问
Video Player
×
Audio Player
×
pdf Player
×