程序設(shè)計(jì)語(yǔ)言的形式語(yǔ)義：計(jì)算機(jī)科學(xué)叢書(shū)

定　價(jià)：￥32.00

作　者：	Glynn Winskel著；宋國(guó)新等譯；宋國(guó)新譯
出版社：	中信出版社
叢編項(xiàng)：
標(biāo)　簽：	暫缺

購(gòu)買這本書(shū)可以去

ISBN：	9787111131533	出版時(shí)間：	2004-01-01	包裝：	膠版紙
開(kāi)本：	26cm	頁(yè)數(shù)：	283	字?jǐn)?shù)：

內(nèi)容簡(jiǎn)介

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

作者簡(jiǎn)介

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

圖書(shū)目錄

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