目 录
第一部分：Ada及其规格说明语言Anna
1引言
2Ada典型特征
3Anna基本概念
3.1虚拟Ada行文
3.2标注
3.3新增运算与属性
3.4带量词表达式
4标注种类
4.1对象标注
4.2（子）类型标注
4.3语句标注
4.4子程序标注
4.5异常传播标注
4.6上下文标注
5程序包标注
5.1可见标注与隐藏标注
5.2程序包状态
5.3程序包公理
6语义、实现及工具
6.1公理语义
6.2转换语义与实现
6.3基本工具
7结束语
附录 Ada语法
第二部分：Anna语言参考手册
0作者前言
1Anna基本概念
1.1虚拟Ada行文
1.2标注
1.3标注的语义
1.3.1程序状态
1.3.2断言与Anna核
1.3.3Anna程序的一致性
1.3.4标注的定义性
1.4一致性检查
1.5手册结构
1.6错误分类
2词法元素
2.1字符集
2.2词法元素、分隔符与定界符
2.7形式注解
2.9保留字
2.10 允许的字符替换
3声明与类型标注
3.1声明标注
3.2对象标注
3.2.1 对象约束转换
3.3类型与子类型声明标注
3.3.3适用于所有类型的运算
3.4派生类型标注
3.5纯量类型运算
3.6数组类型标注
3.6.2数组类型运算
3.6.4数组状态
3.7记录类型标注
3.7.4记录类型运算
3.7.5记录状态
3.8 访问类型标注
3.8.2访问类型运算
3.8.3访问类型约束
3.8.4集团状态
3.9 声明部分
4标注中名字与表达式
4.1标注中名字
4.1.4 属性
4.4标注中表达式
4.5运算符与表达式求值
4.5.1 逻辑运算符
4.5.2 关系运算符与成员关系测试
4.6类型转换
4.7限定表达式
4.11带量词表达式
4.11.1带量词表达式转换成Anna核
4.12 条件表达式
4.13修饰符
4.14表达式的定义性
5语句标注
5.1简单与复合语句标注
5.5循环语句标注
5.8返回语句标注
6子程序标注
6.1子程序声明标注
6.2形式参数标注
6.3子程序体标注
6.4子程序调用标注
6.5函数子程序结果标注
6.6标注中子程序重载
6.7运算符重载
6.8子程序属性
7程序包标注
7.1程序包结构
7.2程序包规格说明中可见标注
7.2.1可见类型标注
7.3程序包隐藏标注
7.4私有类型标注
7.4.1私有类型在标注中的运用
7.4.2私有类型运算
7.4.4受限类型相等运算的重新定义
7.7程序包状态
7.7.1状态类型
7.7.2初始状态和当前状态
7.7.3程序包后继状态
7.7.4相对于程序包状态的函数调用
7.7.5状态类型标注
7.8公理标注
7.8.1公理简化表示法
7.8.2隐式相等公理
7.9Anna程序包的一致性
7.9.1 程序包体的一致性
7.9.2可见标注与程序包体的一致性
7.10带标注程序包举例
8标注的可见性规则
8.2声明与声明标注的作用域
8.3可见性
8.5改名声明
8.7重载分辨的上下文
9任务标注
10程序结构
10.1编译单元标注
10.1.1 虚拟上下文子句
10.1.3上下文标注
10.2子单元标注
11异常标注
11.2异常处理段标注
11.3引发语句标注
11.4传播标注
11.7标注的屏蔽检查
12类属单元标注
12.1类属声明标注
12.1.1类属形式对象标注
12.1.2类属形式类型标注
12.1.3类属形式子程序标注
12.3类属标注例举
12.4带标注类属程序包举例
12.5类属单元的一致性
13依赖实现的特征的标注
13.8机器代码插入的标注
12.9与其它语言接口的标注
13.10不作检查的程序设计的标注
13.10.1不作检查的存贮单元回收的标注
13.10.2 不作检查的类型转换的标注
附录A 预定义Anna属性
附录C 预定义Anna环境
附录E Anna语法概要
附录H Anna程序实例
1 符号表程序包
2 Dijkstra荷兰国旗程序
第三部分：TSL－1一种Ada任务定序语言
1概述
2类型表达式与基本事件
3用户定义事件与执行语句
4占位符
5事件匹配与参数汇集
6哨兵
7复合事件
8规格说明
9性质与更新语句
10 宏定义与调用
11TSL―1任务规格说明
12结束语
附录A TSL－1扩充的语法
附录B TSL－1扩充的保留字
附录C TSL－1扩充预定义环境
附录D 例筛法求质数
参考文献
英汉名词对照
· · · · · · (收起)