OESPA:面向语义的编程理论(英文版)

OESPA:面向语义的编程理论(英文版)
分享
扫描下方二维码分享到微信
打开微信,点击右上角”+“,
使用”扫一扫“即可将网页分享到朋友圈。
作者:
出版社: 科学出版社
2019-01
版次: 1
ISBN: 9787030600936
定价: 120.00
装帧: 平装
开本: 16开
页数: 200页
3人买过
  • 传统的软件理论研究是形式语法和形式语义分离,语义研究成果没有实用性,测试一直是软件开发的必要步骤。本书是统一研究语法与语义的成果,包括程序模型(OE),语义公理(A),语义谓词(SP),语义谓词演算,是一套全新的完整的实用的程序理论。实例证明用OESPA可以用于程序开发各步骤,程序验证及程序验证自动化(符号演算)。测试不再是必要的。为开发相应的验证工具奠定了基础。 Contents
    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
  • 内容简介:
    传统的软件理论研究是形式语法和形式语义分离,语义研究成果没有实用性,测试一直是软件开发的必要步骤。本书是统一研究语法与语义的成果,包括程序模型(OE),语义公理(A),语义谓词(SP),语义谓词演算,是一套全新的完整的实用的程序理论。实例证明用OESPA可以用于程序开发各步骤,程序验证及程序验证自动化(符号演算)。测试不再是必要的。为开发相应的验证工具奠定了基础。
  • 目录:
    Contents
    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
查看详情
相关图书 / 更多
OESPA:面向语义的编程理论(英文版)
OECD国家税收概览/上海高校智库
胡怡建、田志伟、刘雨朦 编
OESPA:面向语义的编程理论(英文版)
OECD教育指标引领教育发展研究(2035中国教育发展战略研究)
黄忠敬 著
OESPA:面向语义的编程理论(英文版)
OEC管理:大学生党建创新模式研究
赵纪新
OESPA:面向语义的编程理论(英文版)
OECDTransferPricingGuidelinesforMultinationalEnterprisesandTaxAdministrations2010
Publishing Oecd Publishing 著
OESPA:面向语义的编程理论(英文版)
OECD国家长期护理津贴制度研究
戴卫东、顾梦洁 著
OESPA:面向语义的编程理论(英文版)
OECD/G20税基侵蚀和利润转移(BEPS)项目2015年成果最终报告(套装全6册)
经济合作与发展组织 著;国家税务总局国际税务司 译
OESPA:面向语义的编程理论(英文版)
OECD税收协定范本及注释
经济合作与发展组织
OESPA:面向语义的编程理论(英文版)
OECD中国经济调查(2019年)
OECD
OESPA:面向语义的编程理论(英文版)
OECD风险管理策略评述 2009,日本大洪水与地震
Organisation for Economic Cooperation and Development 胡昌伟 刘媛媛 刘业森 著;胡昌伟、 刘媛媛、刘业森 译
OESPA:面向语义的编程理论(英文版)
OECD Investment Policy Reviews: Kazakhstan 2017
OECD
OESPA:面向语义的编程理论(英文版)
OECD风险管理策略评述:2010意大利国家民事保护体系
Organisation for Economic Cooperation and Development
OESPA:面向语义的编程理论(英文版)
OECD Transfer Pricing Guidelines for Multinational Enterprises and Tax Administrations:2017
Organisation for Economic Cooperation and Development;OECD
您可能感兴趣 / 更多
OESPA:面向语义的编程理论(英文版)
Petri网应用
袁崇义 著
OESPA:面向语义的编程理论(英文版)
Petri网原理与应用
袁崇义 著