贊譽(yù)
譯者序
推薦序
致謝
第1章　信息物理系統(tǒng)概述1
　1.1　引言1
　　1.1.1　舉例分析信息物理系統(tǒng)1
　　1.1.2　應(yīng)用領(lǐng)域2
　　1.1.3　意義2
　　1.1.4　安全的重要性3
　1.2　混成系統(tǒng)與信息物理系統(tǒng)4
　1.3　多動(dòng)態(tài)系統(tǒng)5
　1.4　如何學(xué)習(xí)信息物理系統(tǒng)6
　1.5　信息物理系統(tǒng)的計(jì)算思維7
　1.6　學(xué)習(xí)目標(biāo)8
　1.7　本書(shū)的結(jié)構(gòu)9
　1.8　總結(jié)12
　參考文獻(xiàn)12
部分　初等信息物理系統(tǒng)
第2章　微分方程與域18
　2.1　引言18
　2.2　作為連續(xù)物理過(guò)程模型的微分方程18
　2.3　微分方程的含義20
　2.4　微分方程示例的簡(jiǎn)短綱要21
　2.5　微分方程的域26
　2.6　連續(xù)程序的語(yǔ)法27
　　2.6.1　連續(xù)程序28
　　2.6.2　項(xiàng)28
　　2.6.3　一階公式29
　2.7　連續(xù)程序的語(yǔ)義30
　　2.7.1　項(xiàng)30
　　2.7.2　一階公式31
　　2.7.3　連續(xù)程序34
　2.8　總結(jié)35
　2.9　附錄35
　　2.9.1　存在性定理35
　　2.9.2　性定理36
　　2.9.3　常系數(shù)線性微分方程37
　　2.9.4　延拓與連續(xù)依賴38
　習(xí)題39
　參考文獻(xiàn)41
第3章　選擇與控制42
　3.1　引言42
　3.2　混成程序的逐步介紹43
　　3.2.1　混成程序的離散變化43
　　3.2.2　混成程序的合成44
　　3.2.3　混成程序中的決策45
　　3.2.4　混成程序中的選擇45
　　3.2.5　混成程序中的測(cè)試47
　　3.2.6　混成程序中的重復(fù)48
　3.3　混成程序50
　　3.3.1　混成程序的語(yǔ)法50
　　3.3.2　混成程序的語(yǔ)義51
　3.4　混成程序設(shè)計(jì)54
　　3.4.1　制動(dòng)還是不制動(dòng)，這是個(gè)問(wèn)題54
　　3.4.2　選擇的問(wèn)題55
　3.5　總結(jié)56
　3.6　附錄：機(jī)器人彎道運(yùn)動(dòng)建模56
　習(xí)題58
　參考文獻(xiàn)61
第4章　安全性與契約63
　4.1　引言63
　4.2　CPS契約的逐步介紹64
　　4.2.1　彈跳球Quantum歷險(xiǎn)記64
　　4.2.2　Quantum如何在時(shí)間結(jié)構(gòu)中發(fā)現(xiàn)裂縫67
　　4.2.3　Quantum怎樣學(xué)會(huì)放氣68
　　4.2.4　CPS的后置條件契約69
　　4.2.5　CPS的前置條件契約70
　4.3　混成程序的邏輯公式71
　4.4　微分動(dòng)態(tài)邏輯73
　　4.4.1　微分動(dòng)態(tài)邏輯的語(yǔ)法73
　　4.4.2　微分動(dòng)態(tài)邏輯的語(yǔ)義75
　4.5　邏輯形式的CPS契約77
　4.6　查明CPS的需求78
　4.7　總結(jié)82
　4.8　附錄82
　　4.8.1　順序合成證明的中間條件82
　　4.8.2　選擇的證明84
　　4.8.3　測(cè)試的證明85
　習(xí)題86
　參考文獻(xiàn)90
第5章　動(dòng)態(tài)系統(tǒng)與動(dòng)態(tài)公理92
　5.1　引言92
　5.2　CPS的中間條件93
　5.3　動(dòng)態(tài)系統(tǒng)的動(dòng)態(tài)公理95
　　5.3.1　非確定性選擇的動(dòng)態(tài)公理95
　　5.3.2　公理的可靠性97
　　5.3.3　賦值的動(dòng)態(tài)公理98
　　5.3.4　微分方程的動(dòng)態(tài)公理99
　　5.3.5　測(cè)試的動(dòng)態(tài)公理101
　　5.3.6　順序合成的動(dòng)態(tài)公理102
　　5.3.7　循環(huán)的動(dòng)態(tài)公理104
　　5.3.8　尖括號(hào)模態(tài)的公理105
　5.4　短暫彈跳球的證明105
　5.5　總結(jié)107
　5.6　附錄108
　　5.6.1　模態(tài)肯定前件在方括號(hào)模態(tài)中的蘊(yùn)涵108
　　5.6.2　如果沒(méi)有任何相關(guān)變化，則為空虛狀態(tài)變化109
　　5.6.3　哥德?tīng)枌⒂勒嫘苑夯�到方括�?hào)模態(tài)中109
　　5.6.4　后置條件的單調(diào)性110
　　5.6.5　自由變量和約束變量111
　　5.6.6　自由變量和約束變量分析111
　習(xí)題113
　參考文獻(xiàn)116
第6章　真理與證明118
　6.1　引言118
　6.2　真理和證明119
　　6.2.1　相繼式120
　　6.2.2　證明122
　　6.2.3　命題證明規(guī)則122
　　6.2.4　證明規(guī)則的可靠性126
　　6.2.5　動(dòng)態(tài)的證明127
　　6.2.6　量詞證明規(guī)則129
　6.3　派生證明規(guī)則131
　6.4　單跳彈跳球的相繼式證明132
　6.5　實(shí)算術(shù)證明規(guī)則133
　　6.5.1　實(shí)數(shù)量詞消除法134
　　6.5.2　實(shí)例化實(shí)算術(shù)量詞136
　　6.5.3　通過(guò)去除假設(shè)來(lái)弱化實(shí)算術(shù)137
　　6.5.4　相繼式演算中的結(jié)構(gòu)證明規(guī)則138
　　6.5.5　在公式中代入等式139
　　6.5.6　縮寫項(xiàng)以降低復(fù)雜性139
　　6.5.7　創(chuàng)造性地切割實(shí)算術(shù)轉(zhuǎn)化問(wèn)題140
　6.6　總結(jié)140
　習(xí)題141
　參考文獻(xiàn)143
第7章　控制回路與不變式145
　7.1　引言145
　7.2　控制循環(huán)146
　7.3　循環(huán)回路147
　　7.3.1　循環(huán)的歸納公理147
　　7.3.2　循環(huán)的歸納規(guī)則149
　　7.3.3　循環(huán)不變式150
　　7.3.4　上下文可靠性需求153
　7.4　一個(gè)歡快重復(fù)的彈跳球的證明154
　7.5　將后置條件拆分為單獨(dú)的情況158
　7.6　總結(jié)159
　7.7　附錄159
　　7.7.1　證明的循環(huán)159
　　7.7.2　打破證明循環(huán)161
　　7.7.3　循環(huán)的不變式證明163
　　7.7.4　歸納公理的替代形式163
　習(xí)題165
　參考文獻(xiàn)166