OESPA:面向語義的編程理論(簡體書)
- 系列名:智能科學技術著作叢書
- ISBN13:9787030600936
- 出版社:科學出版社
- 作者:Yuan Chongyi
- 裝訂/頁數:平裝/200頁
- 規格:24cm*17cm (高/寬)
- 版次:一版
- 出版日:2019/08/08
商品簡介
目次
Introduction 1
Part 1 ARM-a simple methodology 5
Chapter 1 ARM as a meta-method 7
1.1 Steps in ARM 7
1.2 Importance of abstraction step 10
Chapter 2 ARM leads to a 3-layer model of BPM 13
2.1 Why BPM today: the purpose 13
2.2 Abstraction 14
2.2.1 Physical objects 14
2.2.2 Mathematical objects 15
2.3 Mathematical system: the 3 layers 19
2.4 Correctness criteria and proof method 22
Part 2 OESPA: to combine program semantics with program syntax 27
Chapter 3 Assertions on programs 29
3.1 Formal treatment 29
3.2 Assertions and weakest preconditions 32
3.3 To remove ambiguity from programs 33
Chapter 4 OE: operation expressions 38
4.1 Operations on a memory location 39
4.1.1 Read and write operations 40
4.1.2 Semantic functions 44
4.1.3 Semantic predicates 46
4.2 Operation expressions 51
4.2.1 OE syntax in terms of BNF 51
4.2.2 Semantic axioms for OE 59
4.3 How to compute semantic function u( p) 66
4.4 Theorems provable from semantic axioms 77
Chapter 5 SP calculus 81
5.1 Reduction rules 82
5.2 SP-formulas for loops 88
5.2.1 Loop pn 88
5.2.2 Loop pb and pb′ 91
5.3 Complete specification 93
Chapter 6 Programming in OE by examples 96
6.1 8-queen problem 96
6.1.1 Abstraction and specification 96
6.1.2 Specification refinement 98
6.1.3 Programming in OE 107
6.1.4 Program verification 115
6.1.5 Complete OE of queen-all 121
6.2 Sorting an array into ascending order 122
6.2.1 Specification 122
6.2.2 Sorting program in C 124
6.2.3 Replacing val with swap 127
6.2.4 Quick-sorting in OE 130
6.2.5 Verifying q-sorting 132
6.3 N-lift problem: service sharing 137
6.3.1 From requirement to specification 137
6.3.2 Global control vs local determination 142
6.3.3 Atomic action and atomic request 144
6.3.4 To assemble actions at floor k in up direction 150
6.3.5 Complete OE for the lift 154
Part 3 Connecting OE with C 157
Chapter 7 Pointers, functions and structures on C 159
7.1 Semantic axioms on C pointers 159
7.2 Theorems about C pointers and examples 161
7.3 C functions: definition and call 171
7.4 Structures and union of C 175
Part 4 Parallel operation expressions(POE) 177
Chapter 8 Syntax and semantics of POE 179
8.1 Semantic consideration on POE 180
8.2 Semantics of solutions in different categories 183
8.2.1 Loose dependence: shared services 183
8.2.2 Simple dependence: shared resources 187
8.2.3 Simple cooperation: shared CPU time 189
8.2.4 Frangible cooperation: shared operands 190
8.2.5 Other problems involving parallelism 195
Chapter 9 5-philosopher problem 198
9.1 Fork management 198
9.2 Efficiency and fairness 202
9.2.1 Efficiency by “law” 202
9.2.2 Fairness 204
9.3 Shared variables as communication channels 207
References 212
Epilogue 213
主題書展
更多主題書展
更多書展本週66折
您曾經瀏覽過的商品
購物須知
大陸出版品因裝訂品質及貨運條件與台灣出版品落差甚大,除封面破損、內頁脫落等較嚴重的狀態,其餘商品將正常出貨。
特別提醒:部分書籍附贈之內容(如音頻mp3或影片dvd等)已無實體光碟提供,需以QR CODE 連結至當地網站註冊“並通過驗證程序”,方可下載使用。
無現貨庫存之簡體書,將向海外調貨:
海外有庫存之書籍,等候約45個工作天;
海外無庫存之書籍,平均作業時間約60個工作天,然不保證確定可調到貨,尚請見諒。
為了保護您的權益,「三民網路書店」提供會員七日商品鑑賞期(收到商品為起始日)。
若要辦理退貨,請在商品鑑賞期內寄回,且商品必須是全新狀態與完整包裝(商品、附件、發票、隨貨贈品等)否則恕不接受退貨。