同類熱銷排行榜

形式化方法(理論及應用信息電腦類研究生系列教材)

作者：編者:華保健|責編:張燦//劉蘇銳
出版社：中國科大
ISBN：9787312058752

出版日期：2024/05/01
裝幀：平裝
頁數：347

人民幣：RMB 76 元售價：元

內容大鋼

    形式化方法是電腦科學理論中歷史悠久、理論性強、發展成熟的學科，已發展成為電腦科學的重要分支之一。形式化方法主要用數學的理論和工具，對電腦軟硬體系統進行形式建模和性質推理研究，以期證明系統的實現正確性，或提高系統的可靠性和健壯性等。本書全面講授形式化方法理論及應用，從基礎知識出發，討論了數理邏輯、可滿足性、決策過程以及理論應用等內容，並給出了豐富的實例。
    全書共分為13章，分別討論了理論基礎、命題邏輯、布爾可滿足性、謂詞邏輯、可滿足性模理論、數據結構的判定、符號執行、程序驗證、程序合成、Curry-Howard同構、依賴類型等內容，並給出了充分的實踐討論與應用實例。
    本書適合高等學校信息與電腦科學與技術、軟體工程、信息安全等相關專業的學生，以及對軟體工程、形式化方法等感興趣的工程技術人員閱讀。

作者介紹

編者:華保健|責編:張燦//劉蘇銳

前言
第1章  基礎知識
  1.1  集合
  1.2  關係與映射
  1.3  上下文無關文法
  1.4  歸納法
  1.5  歸納定義
  1.6  實現
第2章  命題邏輯
  2.1  語法
  2.2  證明系統
  2.3  構造邏輯
  2.4  語義系統
  2.5  可靠性和完備性定理
  2.6  可判定性
  2.7  命題邏輯的實現
第3章  布爾可滿足性
  3.1  布爾可滿足性
  3.2  合取範式
  3.3  決議與傳播
  3.4  DPLL演算法
  3.5  實現
第4章  謂詞邏輯
  4.1  命題的內部結構
  4.2  語法
  4.3  證明系統
  4.4  語義系統
  4.5  可靠性和完備性
  4.6  可判定性
  4.7  實現
第5章  等式與未解釋函數理論
  5.1  可滿足性模理論
  5.2  等式與未解釋函數理論
  5.3  基本性質
  5.4  判定演算法
  5.5  實現
  5.6  應用
第6章  線性算術理論
  6.1  語法
  6.2  高斯消元
  6.3  傅里葉-莫茨金消元
  6.4  單純形法
  6.5  分支定界法
  6.6  減法邏輯
  6.7  實現
  6.8  應用
第7章  數據結構理論
  7.1  位向量
  7.2  數組
  7.3  指針

  7.4  字元串
第8章  理論組合
  8.1  理論組合
  8.2  Nelson-Oppen協作過程
  8.3  凸理論
  8.4  非凸理論
  8.5  DPLL(T)演算法
  8.6  實現
第9章  符號執行
  9.1  命令式語言IMP
  9.2  操作語義
  9.3  符號執行
  9.4  混合執行
  9.5  符號執行工程
  9.6  實現
  9.7  應用
第10章  程序驗證
  10.1  霍爾三元組
  10.2  公理語義
  10.3  最弱前條件
  10.4  驗證條件
  10.5  前向驗證條件生成
  10.6  實現
第11章  程序合成
  11.1  基本概念
  11.2  基於語法的合成
  11.3  基於符號執行的合成
  11.4  實現
第12章  Curry-Howard同構
  12.1  無類型λ演算
  12.2  簡單類型化λ演算
  12.3  Curry-Howard同構
  12.4  二階邏輯與系統F
  12.5  實現
第13章  依賴類型
  13.1  基本概念
  13.2  純一階依賴類型
  13.3  依賴總和類型
  13.4  構造演算
  13.5  邏輯框架
  13.6  實現
參考文獻

Δ訂單支付
付款方式
運費計算方式

Δ關於我們
關於美商天龍
聯絡我們

首頁│ 新手上路│ 客服中心│ 關於我們│ 聯絡我們│ 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

同類熱銷排行榜

最近瀏覽的商品

形式化方法(理論及應用信息電腦類研究生系列教材)