2 Ada典型特征 3
4.6 上下文标注 1 3
第一部分：Ada及其规格说明语言Anna 3
3 Anna基本概念 5
3.1 虚拟Ada行文 6
3.2 标注 8
3.3 新增运算与属性 9
3.4 带量词表达式 9
4 标注种类 9
4.1 对象标注 10
4.2 （子）类型标注 10
4.3 语句标注 10
4.4 子程序标注 12
4.5 异常传播标注 12
5.1 可见标注与隐藏标注 14
5 程序包标注 14
5.2 程序包状态 15
5.3 程序包公理 16
6 语义、实现及工具 17
6.1 公理语义 18
6.2 转换语义与实现 18
6.3 基本工具 19
7 结束语 20
附录 Ada语法 20
第二部分：Anna语言参考手册 32
1 Anna基本概念 37
1.1 虚拟Ada行文 37
1.2 标注 39
1.3 标注的语义 42
1.4 一致性检查 45
1.5 手册结构 47
1.6 错误分类 49
2 词法元素 49
2.1 字符集 49
2.2 词法元素、分隔符与定界符 50
2.7 形式注解 50
2.9 保留字 51
2.10 允许的字符替换 51
3 声明与类型标注 52
3.1 声明标注 52
3.2 对象标注 54
3.3 类型与子类型声明标注 59
11.2 异常处理段标注 1 63
3.5 纯量类型运算 65
3.4 派生类型标注 65
3.6 数组类型标注 66
3.7 记录类型标注 69
3.8 访问类型标注 73
3.9 声明部分 81
4 标注中名字与表达式 82
4.1 标注中名字 82
4.4 标注中表达式 83
4.5 运算符与表达式求值 84
4.7 限定表达式 87
4.11 带量词表达式 87
4.6 类型转换 87
4.12 条件表达式 92
4.13 修饰符 94
4.14 表达式的定义性 97
5 语句标注 100
5.1 简单与复合语句标注 100
5.5 循环语句标注 103
6 子程序标注 104
5.8 返回语句标注 104
6.1 子程序声明标注 105
6.2 形式参数标注 107
6.3 子程序体标注 109
6.4 子程序调用标注 110
6.5 函数子程序结果标注 111
6.6 标注中子程序重载 112
6.7 运算符重载 112
6.8 子程序属性 112
7 程序包标注 114
7.1 程序包结构 115
7.2 程序包规格说明中可见标注 116
7.3 程序包隐藏标注 119
7.4 私有类型标注 121
7.7 程序包状态 127
7.8 公理标注 140
7.9 Anna程序包的一致性 147
7.10 带标注程序包举例 153
8 标注的可见性规则 156
8.2 声明与声明标注的作用域 156
8.3 可见性 157
8.5 改名声明 158
8.7 重载分辨的上下文 159
9 任务标注 159
10 程序结构 160
10.1 编译单元标注 160
10.2 子单元标注 162
11.1 异常标注 163
11.3 引发语句标注 164
11.4 传播标注 164
11.7 标注的屏蔽检查 167
12.1 类属声明标注 168
12 类属单元标注 168
12.3 类属标注例举 174
12.4 带标注类属程序包举例 175
12.5 类属单元的一致性 176
13 依赖实现的特征的标注 178
13.8 机器代码插入的标注 178
13.9 与其它语言接口的标注 178
13.10 不作检查的程序设计的标注 178
附录A 预定义Anna属性 179
附录C 预定义Anna环境 181
附录E Anna语法概要 181
附录H Anna程序实例 186
第三部分：TSL-1：一种Ada任务定序语言 194
1 概述 194
2 类型表达式与基本事件 197
3 用户定义事件与执行语句 199
4 占位符 200
5 事件匹配与参数汇集 201
6 哨兵 202
7 复合事件 203
8 规格说明 204
9 性质与更新语句 206
10 宏定义与调用 207
11 TSL-1任务规格说明 208
12 结束语 210
附录A TSL-1扩充的语法 210
附录B TSL-1扩充的保留字 215
附录C TSL-1扩充预定义环境 215
附录D 例筛法求质数 216
参考文献 220
英汉名词对照 222