程序設計語言的形式語義：計算機科學叢書

  第1章  集合論基礎
    1．1  邏輯記號
    1．2  集合
    1．2．1  集合與性質
    1．2．2  一些重要集合
    1．2．3  集合的構造
    1．2．4  基本公理
    1．3  關系與函數(shù)
    1．3．1  A記號
    1．3．2  復合關系與復合函數(shù)
    1．3．3  關系的正象與逆象
    1．3．4  等價關系
    1．4  進一步閱讀資料
  第2章  操作語義
    2．1  1MP一種簡單的命令式語言
    2．2  算術表達式的求值
    2．3  布爾表達式的求值
    2．4  命令的執(zhí)行
    2．5  一個簡單的證明
    2．6  另一種語義
    2．7  進一步閱讀資料
  第3章  歸納原理
    3．1  數(shù)學歸納法
    3．2  結構歸納法
    3．3  良基歸納法
    3．4  對推導的歸納
    3．5  歸納定義
    3．6  進一步閱讀資料
  第4章  歸納定義
    4．1  規(guī)則歸納法
    4．2  特殊的規(guī)則歸納法
    4．3  操作語義的證明規(guī)則
    4．3．1  算術表達式的規(guī)則歸納法
    4．3．2  布爾表達式的規(guī)則歸納法
    4．3．3  命令的規(guī)則歸納法
    4．4  算子及其最小不動點
    4．5  進一步閱讀資料
  第5章  IMP的指稱語義
    5．1  目的
    5．2  指稱語義
    5．3  語義的等價性
    5．4  完全偏序與連續(xù)函數(shù)
    5．5  克納斯特塔爾斯基定理
    5．6  進一步閱讀資料
  第6章  IMP的公理語義
    6．1  基本思想
    6．2  斷言語言Assn
    6．2．1  自由變量與約束變量
    6．2．2  代人
    6．3  斷言的語義
    6．4  部分正確性的證明規(guī)則
    6．5  可靠性
    6．6  應用霍爾規(guī)則的一個示例
    6．7  進一步閱讀資料
  第7章  霍爾規(guī)則的完備性
    7．1  哥德爾不完備性定理
    7．2  最弱前置條件與可表達性
    7．3  哥德爾定理的證明
    7．4  驗證條件
    7．5  謂詞轉換器
    7．6  進一步閱讀資料
  第8章  域論
    8．1  基本定義
    8．2  一個例子流
    8．3  完全偏序上的構造
    8．3．1  離散完全偏序
    8．3．2  有限積
    8．3．3  函數(shù)空間
    8．3．4  提升
    8．3．5  和
    8．4  元語言
    8．5  進步閱讀資料
  第9章  遞歸方程
    9．1  REC語言
    9．2  傳值調用的操作語義
    9．3  傳值調用的指稱語義
    9．4  傳值調用的語義等價
    9。5  傳名調用的操作語義
    9．6  傳名調用的指稱語義
    9．7  傳名調用的語義等價
    9．8  局部聲明
    9．9  進一步閱讀資料
  第10章  遞歸技術
    10．1  貝伊克定理
    10．2  不動點歸納法
    10．3  良基歸納
    10．4  良基遞歸
    10．5  一個練習
    10．6  進一步閱讀資料
  第11章  高階類型語言
    11．1  活性語言
    11．2  活性操作語義
    11．3  活性指稱語義
    11．4  活性語義的一致性
    11．5  惰性語言
    11．6  惰性操作語義
    11．7  惰性指稱語義
    11．8  惰性語義的一致性
    11．9  不動點算子
    11．10  觀察與完全抽象
    11．11  和
    11．12  進步閱讀資料
  第12章  信息系統(tǒng)
    12．1  遞歸類型
    12．2  信息系統(tǒng)定義
    12．3  閉族與斯科特前域
    12．4  信息系統(tǒng)的完全偏序
    12．5  構造
    12．5．1  提升
    12．5．2  和
    12．5．3  積
    12．5．4  提升函數(shù)空間
    12．6  進步閱讀資料
第13章  遞歸類型
    13．1  活性語言
    13．2  活性操作語義
    13．3  活性指稱語義
    13．4  活性語義的適用性
    13．5  活性入演算
    13．5．1  等式理論
    13．5．2  不動點算子
    13．6  惰性語言
    13．7  惰性操作語義
    13．8  惰性指稱語義
    13．9  惰性語言的適用性
    13．10  惰性入演算
    13．10．I  等式理論
    13．10．2  不動點算子
    13．11  進步閱讀資料
第14章  不確定性和并行性
    14．1  引言
    14．2  衛(wèi)式命令
    14．3  通信進程
    14．4  米爾納的CCS
    14．5  純CCS
    14．6  規(guī)范語言
    14．7  模態(tài)v演算
    14．8  局部模型檢查
    14．9  進步閱讀資料
    附錄A  不完備性和不可判定性
  參考文獻
  索引