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