Anna语言导论

作者简介

内容简介

本书是国内第一本介绍Anna语言的书籍.Anna是一种以Ada

为基础的规格说明语言，大量吸收了Pascal等语言的研究成果，

可广泛用于软件开发过程中从需求规格说明、设计、编码、测试到

维护各个阶段。全书由三部分组成：第一部分是Anna入门、对

Anna作一般介绍；第二部分是完整的Anna参考手册；第三部分

详细描述了与Anna互补的TSL－1语言。

本书适用于广大软件工作者、高等院校师生，可作为高校本科

生与研究生有关课程的教学参考书。

书籍目录

目 录

第一部分：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 例筛法求质数

参考文献

英汉名词对照

 Anna语言导论下载