程序設(shè)計語言的形式語義：計算機科學(xué)叢書

定　價：￥32.00

作　者：	Glynn Winskel著；宋國新等譯；宋國新譯
出版社：	中信出版社
叢編項：
標　簽：	暫缺

購買這本書可以去

ISBN：	9787111131533	出版時間：	2004-01-01	包裝：	膠版紙
開本：	26cm	頁數(shù)：	283	字數(shù)：

內(nèi)容簡介

　　本書以作者在劍橋大學(xué)和Aarhus大學(xué)的講座內(nèi)容為基礎(chǔ)，主要針對計算機科學(xué)專業(yè)和數(shù)學(xué)專業(yè)的本科生和研究生而編寫，可作為開始學(xué)習(xí)形式化和推導(dǎo)程序設(shè)計語言的方法的教材。本書介紹了必要的數(shù)學(xué)背景知識，讀者可以運用它們?nèi)?chuàng)造、形式化和證明一些規(guī)則，使用這些規(guī)則可推導(dǎo)各種各樣的程序設(shè)計語言。本書的內(nèi)容是基礎(chǔ)的，但其中有一些主題來自于最近的研究。書中包含了豐富的從簡單到復(fù)雜的練習(xí)。本書首先介紹集合論基礎(chǔ)，接著是結(jié)構(gòu)化操作語義，并將其作為定義程序設(shè)計語言含義的一種方式，同時也介紹了一些基本的證明技術(shù)。對指稱語義和公理語義是以一個簡單的while程序語言為例進行說明的，并給出了操作語義和指稱語義之間等價的完整證明，以及公理語義的可靠性和相對完備性，也包括哥德爾不完備性定理的一個證明。該定理強調(diào)公理語義不可能達到絕對的完備性，這一結(jié)論可以從附錄中得到支持，附錄基于while程序介紹了可計算性理論。在域論之后，介紹了指稱語義的基礎(chǔ)，論述了幾種函數(shù)式語言的語義和證明方法。最簡單的函數(shù)式語言是既可以傳值調(diào)用也可以傳名調(diào)用求值的遞歸方程。這些研究工作可以進一步擴展到含有高階類型和遞歸類型的語言，其中包括對活性和惰性入演算的論述。本書始終強調(diào)指稱語義和操作語義的聯(lián)系，并給出它們的一致性證。本書較高深的部分之一是遞歸，類型的論述，它要利用信息系統(tǒng)來表示域。在最后一章里介紹了并行程序設(shè)計語言，并討論了不確定性和并行程序的驗證方法。

作者簡介

　　GlynN Winskel，曾任丹麥Aarhus大學(xué)計算機科學(xué)系教授，計算機科學(xué)基礎(chǔ)研究中心主任，現(xiàn)任劍橋大學(xué)計算機實驗室教授。

圖書目錄

  第1章  集合論基礎(chǔ)
    1．1  邏輯記號
    1．2  集合
    1．2．1  集合與性質(zhì)
    1．2．2  一些重要集合
    1．2．3  集合的構(gòu)造
    1．2．4  基本公理
    1．3  關(guān)系與函數(shù)
    1．3．1  A記號
    1．3．2  復(fù)合關(guān)系與復(fù)合函數(shù)
    1．3．3  關(guān)系的正象與逆象
    1．3．4  等價關(guān)系
    1．4  進一步閱讀資料
  第2章  操作語義
    2．1  1MP一種簡單的命令式語言
    2．2  算術(shù)表達式的求值
    2．3  布爾表達式的求值
    2．4  命令的執(zhí)行
    2．5  一個簡單的證明
    2．6  另一種語義
    2．7  進一步閱讀資料
  第3章  歸納原理
    3．1  數(shù)學(xué)歸納法
    3．2  結(jié)構(gòu)歸納法
    3．3  良基歸納法
    3．4  對推導(dǎo)的歸納
    3．5  歸納定義
    3．6  進一步閱讀資料
  第4章  歸納定義
    4．1  規(guī)則歸納法
    4．2  特殊的規(guī)則歸納法
    4．3  操作語義的證明規(guī)則
    4．3．1  算術(shù)表達式的規(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  應(yīng)用霍爾規(guī)則的一個示例
    6．7  進一步閱讀資料
  第7章  霍爾規(guī)則的完備性
    7．1  哥德爾不完備性定理
    7．2  最弱前置條件與可表達性
    7．3  哥德爾定理的證明
    7．4  驗證條件
    7．5  謂詞轉(zhuǎn)換器
    7．6  進一步閱讀資料
  第8章  域論
    8．1  基本定義
    8．2  一個例子流
    8．3  完全偏序上的構(gòu)造
    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  傳值調(diào)用的操作語義
    9．3  傳值調(diào)用的指稱語義
    9．4  傳值調(diào)用的語義等價
    9。5  傳名調(diào)用的操作語義
    9．6  傳名調(diào)用的指稱語義
    9．7  傳名調(diào)用的語義等價
    9．8  局部聲明
    9．9  進一步閱讀資料
  第10章  遞歸技術(shù)
    10．1  貝伊克定理
    10．2  不動點歸納法
    10．3  良基歸納
    10．4  良基遞歸
    10．5  一個練習(xí)
    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  構(gòu)造
    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  不完備性和不可判定性
  參考文獻
  索引