目 錄
第一部分：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 例篩法求質數
參考文獻
英漢名詞對照
· · · · · · (收起)