幫助中心 | 我的帳號 | 關於我們
進階搜尋
car

同類熱銷排行榜

最近瀏覽的商品

軟體理論基礎(普通高等學校電腦類一流本科專業建設創新教材)

  • 作者：編者:羅貴明//張宇來|責編:于海雲
  • 出版社：科學
  • ISBN：9787030837745
  • 出版日期：2025/12/01
  • 裝幀：平裝
  • 頁數：273
人民幣：RMB 69.8 元      售價：元
放入購物車
加入收藏夾
內容大鋼
    本書系統闡述了電腦科學和軟體工程中形式語言、自動機、形式邏輯、軟體系統建模和驗證等核心理論與方法。全書從基礎知識開始，介紹了有限自動機、正則表示與正則語言、上下文無關文法、下推自動機與上下文無關語言、圖靈機與計算模型，深入探討問題的可判定性與計算複雜性、命題邏輯、謂詞邏輯和時序邏輯，並進一步擴展至軟體形式化建模與驗證和抽象解釋等相關領域。
    本書知識體系連貫、結構嚴謹，敘述與證明簡潔，注重理論推導的同時兼顧實際應用。內容編排循序漸進，嘗試架構軟體基礎知識體系，使複雜概念的表述和推理更加清晰、準確和易懂，對應課程于2020年入選教育部「國家級一流本科課程」。
    本書適合作為電腦科學與技術、軟體工程、人工智慧、信息安全等專業本科生及研究生的教材，也可供從事形式化方法、程序語言理論、系統驗證等相關領域研究及工程實踐的科技人員參考。
作者介紹
編者:羅貴明//張宇來|責編:于海雲
目錄
第1章  基礎知識
  1.1  數學結構
    1.1.1  集合與映射
    1.1.2  圖結構
    1.1.3  同構與同態
  1.2  符號邏輯
    1.2.1  邏輯概念與運算
    1.2.2  運算的性質與量詞
  1.3  證明方法
    1.3.1  演繹法
    1.3.2  反證法
    1.3.3  數學歸納法
    1.3.4  鴿巢原理
  1.4  語言
    1.4.1  語言的結構
    1.4.2  語言的運算
  1.5  形式文法
    1.5.1  文法的概念
    1.5.2  文法的定義與類型
    1.5.3  文法的語言
  小結
  練習
第2章  有限自動機
  2.1  確定有限自動機
    2.1.1  確定有限自動機的概念
    2.1.2  確定有限自動機的定義
    2.1.3  DFA狀態轉移函數的擴展
    2.1.4  正則語言
  2.2  非確定有限自動機
    2.2.1  非確定有限自動機的概念
    2.2.2  非確定有限自動機的定義
    2.2.3  NFA狀態轉移函數的擴展
    2.2.4  NFA與DFA的關係
  2.3  有限自動機的應用
  小結
  練習
第3章  正則語言與表示
  3.1  正則語言運算的封閉性
    3.1.1  單一終態的NFA
    3.1.2  正則語言的運算性質
  3.2  正則表示
    3.2.1  正則表示的文法
    3.2.2  正則表示的語義
  3.3  正則表示與正則語言
    3.3.1  自動機的擴展
    3.3.2  正則表示的構造
    3.3.3  正則表示與正則語言的關係
    3.3.4  正則表示的代數律
  3.4  正則語言的同態
  3.5  正則表示的應用

    3.5.1  UNIX正則表示
    3.5.2  應用實例
  3.6  正則文法
  小結
  練習
第4章  正則語言的判定性質與優化演算法
  4.1  正則語言的判定性質
    4.1.1  正則語言與元素的關係
    4.1.2  屬性檢測
  4.2  泵引理
    4.2.1  泵引理介紹
    4.2.2  泵引理的應用
  4.3  自動機的優化
    4.3.1  狀態集上的關係
    4.3.2  填表演算法
    4.3.3  最小化的DFA
  小結
  練習
第5章  上下文無關文法和語言
  5.1  上下文無關文法的概念
  5.2  文法的推理
    5.2.1  遞歸推理與推導
    5.2.2  最左推導與最右推導
  5.3  語法分析樹
    5.3.1  語法分析樹介紹
    5.3.2  文法推理與分析樹的關係
  5.4  上下文無關語言與上下文無關文法
    5.4.1  上下文無關語言
    5.4.2  上下文無關文法的構造
  5.5  上下文無關文法的應用
    5.5.1  形式定義中的應用
    5.5.2  語法分析器
    5.5.3  標記語言
  5.6  二義文法
    5.6.1  二義文法的概念
    5.6.2  文法二義性的消除法
    5.6.3  固有二義語言
  小結
  練習
第6章  下推自動機
  6.1  下推自動機的概念
    6.1.1  下推自動機的介紹
    6.1.2  下推自動機的定義
    6.1.3  下推自動機的即時描述
  6.2  PDA的語言
    6.2.1  終態型PDA語言
    6.2.2  空棧型PDA語言
    6.2.3  PDA的語言表示
  6.3  PDA與CFG的關係
    6.3.1  從CFG構造PDA

    6.3.2  從PDA構造CFG
    6.3.3  PDA與CFG的等價性
  6.4  確定的下推自動機
    6.4.1  確定PDA的概念
    6.4.2  DPDA語言與正則語言
    6.4.3  確定PDA與二義文法
  小結
  練習
第7章  上下文無關語言的性質
  7.1  CFG的規範
    7.1.1  變數替換
    7.1.2  CFG的簡化
    7.1.3  Chomsky範式
  7.2  CFL的泵引理及運算性質
    7.2.1  CFL泵引理
    7.2.2  CFL運算的封閉性
    7.2.3  CFL「交」運算性質
  7.3  CFL的判定性質
    7.3.1  空語言和無限語言
    7.3.2  CFL與字元串
  小結
  練習
第8章  圖靈機
  8.1  圖靈機的概念
    8.1.1  圖靈機的介紹
    8.1.2  圖靈機的定義
    8.1.3  圖靈機的即時描述和語言
  8.2  圖靈機的計算
    8.2.1  圖靈機的計算設計
    8.2.2  圖靈機的編程技術
  8.3  圖靈機的擴展
    8.3.1  等價證明
    8.3.2  圖靈機帶的擴展
    8.3.3  圖靈機移動的擴展
    8.3.4  受限圖靈機
    8.3.5  TM的文法
  8.4  圖靈機與其他自動機的關係
    8.4.1  TM與PDA
    8.4.2  TM與電腦
  小結
  練習
第9章  判定性問題
  9.1  TM語言的性質
    9.1.1  編碼TM
    9.1.2  TM語言的補
  9.2  問題的判定性質
    9.2.1  問題與語言
    9.2.2  不可判定問題
  9.3  POST對應問題
    9.3.1  POST對應問題介紹

    9.3.2  GPOST對應問題
    9.3.3  CFG二義性的判定
  9.4  計算複雜性
    9.4.1  時間複雜度
    9.4.2  可滿足性問題
  小結
  練習
第10章  命題邏輯
  10.1  命題邏輯介紹
    10.1.1  基本符號
    10.1.2  命題邏輯的文法
  10.2  命題邏輯的語義
    10.2.1  命題的解釋
    10.2.2  命題的模型
    10.2.3  命題運算的規則與性質
    10.2.4  命題的範式
  10.3  命題邏輯中的證明
    10.3.1  證明系統介紹
    10.3.2  演繹系統介紹
  小結
  練習
第11章  一階邏輯
  11.1  一階邏輯介紹
    11.1.1  個體詞與謂詞
    11.1.2  量詞與作用域
    11.1.3  一階邏輯的文法
    11.1.4  一階邏輯的語義
    11.1.5  一階邏輯的替換
  11.2  一階邏輯的證明系統
    11.2.1  一階邏輯的推理
    11.2.2  一階邏輯的屬性
  11.3  一階邏輯比較
    11.3.1  一階邏輯與命題邏輯
    11.3.2  一階邏輯與高階邏輯
  小結
  練習
第12章  時序邏輯
  12.1  線性時序邏輯
    12.1.1  Kripke結構
    12.1.2  線性時序邏輯介紹
  12.2  LTL公式轉換與屬性描述
    12.2.1  LTL公式轉換
    12.2.2  LTL屬性描述
  12.3  計算樹邏輯
    12.3.1  CTL文法
    12.3.2  CTL語義
  12.4  CTL公式轉換與屬性描述
    12.4.1  CTL公式轉換
    12.4.2  CTL屬性描述
  12.5  LTL與CTL

    12.5.1  LTL與CTL的關係
    12.5.2  時序邏輯的擴展
  小結
  練習
第13章  軟體形式化建模與驗證
  13.1  軟體的形式化方法
    13.1.1  軟體可靠性面臨的挑戰
    13.1.2  形式化方法
  13.2  時間自動機
    13.2.1  時間自動機介紹
    13.2.2  時間自動機結構
  13.3  B?chi自動機
    13.3.1  B?chi自動機介紹
    13.3.2  LTL到BA的轉換
  13.4  軟體的驗證
    13.4.1  定理證明
    13.4.2  模型檢測
  小結
  練習
第14章  抽象解釋
  14.1  抽象解釋理論
    14.1.1  抽象解釋簡介
    14.1.2  Galois連接
  14.2  抽象逼近
    14.2.1  最優抽象逼近
    14.2.2  不動點理論
    14.2.3  收斂運算元
  14.3  形式語義的抽象
    14.3.1  遷移系統
    14.3.2  遷移系統的語義
    14.3.3  語義抽象分析
  14.4  形式化方法的應用
    14.4.1  狀態空間抽象
    14.4.2  MVB形式化建模與實現
  小結
  練習
參考文獻

  • 商品搜索：
  • | 高級搜索
首頁│ 新手上路│ 客服中心│ 關於我們│ 聯絡我們│ Top↑│
Copyrightc 1999~2008 美商天龍國際圖書股份有限公司 臺灣分公司. All rights reserved.
營業地址:臺北市中正區重慶南路一段103號1F 105號1F-2F
讀者服務部電話：02-2381-2033 02-2381-1863　時間：週一-週五 10:00-17:00
　服務信箱：bookuu@69book.com 客戶、意見信箱:cs@69book.com
ICP證：浙B2-20060032