智能科学技术著作丛书OESPA:面向语义的编程理论(英文版)
本书特色
[
传统的软件理论研究是形式语法和形式语义分离，语义研究成果没有实用性,测试一直是软件开发的必要步骤。本书是统一研究语法与语义的成果，包括程序模型（OE），语义公理（A），语义谓词（SP），语义谓词演算，是一套全新的完整的实用的程序理论。实例证明用OESPA可以用于程序开发各步骤，程序验证及程序验证自动化（符号演算）。测试不再是必要的。为开发相应的验证工具奠定了基础。
]
内容简介
[
传统的软件理论研究是形式语法和形式语义分离，语义研究成果没有实用性,测试一直是软件开发的必要步骤。本书是统一研究语法与语义的成果，包括程序模型（OE），语义公理（A），语义谓词（SP），语义谓词演算，是一套全新的完整的实用的程序理论。实例证明用OESPA可以用于程序开发各步骤，程序验证及程序验证自动化（符号演算）。测试不再是必要的。为开发相应的验证工具奠定了基础。语义谓词和语义谓词演算是传统数学没有的新概念，新理论，突破了传统数学的局限，使新的程序理论成为可能。
]
目录
ContentsIntroduction 1Part 1 ARM-a simple methodology 5Chapter 1 ARM as a meta-method 71.1 Steps in ARM 71.2 Importance of abstraction step 10Chapter 2 ARM leads to a 3-layer model of BPM 132.1 Why BPM today: the purpose 132.2 Abstraction 142.2.1 Physical objects 142.2.2 Mathematical objects 152.3 Mathematical system: the 3 layers 192.4 Correctness criteria and proof method 22Part 2 OESPA: to combine program semantics with program syntax 27Chapter 3 Assertions on programs 293.1 Formal treatment 293.2 Assertions and weakest preconditions 323.3 To remove ambiguity from programs 33Chapter 4 OE: operation expressions 384.1 Operations on a memory location 394.1.1 Read and write operations 404.1.2 Semantic functions 444.1.3 Semantic predicates 464.2 Operation expressions 514.2.1 OE syntax in terms of BNF 514.2.2 Semantic axioms for OE 594.3 How to compute semantic function u( p) 664.4 Theorems provable from semantic axioms 77Chapter 5 SP calculus 815.1 Reduction rules 825.2 SP-formulas for loops 885.2.1 Loop pn 885.2.2 Loop pb and pb′ 915.3 Complete specification 93Chapter 6 Programming in OE by examples 966.1 8-queen problem 966.1.1 Abstraction and specification 966.1.2 Specification refinement 986.1.3 Programming in OE 1076.1.4 Program verification 1156.1.5 Complete OE of queen-all 1216.2 Sorting an array into ascending order 1226.2.1 Specification 1226.2.2 Sorting program in C 1246.2.3 Replacing val with swap 1276.2.4 Quick-sorting in OE 1306.2.5 Verifying q-sorting 1326.3 N-lift problem: service sharing 1376.3.1 From requirement to specification 1376.3.2 Global control vs local determination 1426.3.3 Atomic action and atomic request 1446.3.4 To assemble actions at floor k in up direction 1506.3.5 Complete OE for the lift 154Part 3 Connecting OE with C 157Chapter 7 Pointers， functions and structures on C 1597.1 Semantic axioms on C pointers 1597.2 Theorems about C pointers and examples 1617.3 C functions: definition and call 1717.4 Structures and union of C 175Part 4 Parallel operation expressions(POE) 177Chapter 8 Syntax and semantics of POE 1798.1 Semantic consideration on POE 1808.2 Semantics of solutions in different categories 1838.2.1 Loose dependence: shared services 1838.2.2 Simple dependence: shared resources 1878.2.3 Simple cooperation: shared CPU time 1898.2.4 Frangible cooperation: shared operands 1908.2.5 Other problems involving parallelism 195Chapter 9 5-philosopher problem 1989.1 Fork management 1989.2 Efficiency and fairness 2029.2.1 Efficiency by “law” 2029.2.2 Fairness 2049.3 Shared variables as communication channels 207References 212Epilogue 213
封面
书名:智能科学技术著作丛书OESPA:面向语义的编程理论(英文版)
作者:袁崇义
页数:200
定价:¥120.0
出版社:科学出版社
出版日期:2018-04-01
ISBN:9787030600936
PDF电子书大小:148MB 高清扫描完整版