“形式化方法”课堂幻灯片PDF文件
幻灯片文件将随着课程的进展逐步上传
目录 上载时间 附注
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

本页及相关页面(除另声明者外)由裘宗燕创建维护,可自由用于各种学习活动。 其他使用需得到作者许可。