目录 |
上载时间 |
附注 |
0,引言 | 2015-11-28 | 软件开发过程,本质、现状和问题,形式化方法在软件(计算机系统)开发中的作用,人们已经和正在做些什么 |
1,B 方法概述 | 2015-11-28 | 简单介绍 B 方法和 B 语言的基本情况 |
2,抽象机和规范 | 2015-11-28 | 通过一些例子介绍 B 抽象机,也介绍了 Atelier B 系统的使用 |
3,集合论和逻辑 | 2015-11-28 | 与 B 方法有关的逻辑和集合论基础, 以及它们在描述软件规范时的使用 |
4,代换、抽象机和证明义务 | 2015-11-28 | 代换的广义代换,抽象机结构,不变式、初始化和操作带来的证明义务 |
5,非确定性 | 2015-11-28 | 非确定性代换 CHOICE, ANY 和一些其他结构,包括 LET, DEFINITIONS 等 |
6,非确定性和其他 | 2015-11-28 | 非确定性代换 SELECT,:(),以及一些其他结构,包括 VAR, CASE等,还介绍了数组的概念和数组验证 |
7,抽象机组织:INCLUDES | 2015-11-28 | 抽象机组织的重要性, INCLUDES(抽象机包含), PROMOTES(操作提升)和 EXTENDS(抽象机扩充) |
8,抽象机组织(2) | 2015-11-28 | 并行代换, 模拟外部环境, SEES 和 USES |
9,精化,数据精化(2) | 2015-11-28 | 精化的概念, 数据精化, 数据精化的使用 |
10,精化和证明义务 | 2015-11-28 | 消除非确定性,非确定性的重新安排,精化的证明义务 |
11,循环代换,B语言重温 | 2015-11-28 | 循环代换的结构,B类型系统、表达式、记录类型、树和二叉树等 |
12,实现 | 2015-11-28 | B模块,实现模块,组合和参考,通过分层模块构造大型软件 |
13,系统结构和实现 | 2015-11-28 | 模块之间的连接关系,简单的精化实现,用IMPORTS封装脆弱模块,实现中的数据精化 |
14,实现中的一些问题 | 2015-11-28 | 实现中的循环,用独立抽象机实现循环体,集合和常量的实现,STRING类型 |
15,B 方法,形式化方法和课程总结 | 2015-11-28 | |