Proof in VDM: A Practitioner's Guide
Proof in VDM: A Practitioner's Guide
复制标题
VDM 中的证明：从业者指南
DOI：
10.1007/978-1-4471-2033-9
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
B. Ritchie
中科院分区：
文献类型：
--
作者：
J. Bicarregui;J. Fitzgerald;P. Lindsay;Richard C. Moore;B. Ritchie
1简介-1.1背景。-1.2实践中如何出现证明：介绍性示例。-1.3证明的逻辑框架。-1.4摘要。 2.2基本的公理化。-2.3使用矛盾推理的派生规则推理。-2.4使用定义：连接。构造。-2.6摘要。 .- 3.5扩展到具有均等性的键入谓词LPF。 4.1简介。-4.2联合类型。-4.3笛卡尔产品类型。-4.4可选类型。-4.5子类型。-4.6复合类型的注释。-4.7摘要。-4.8练习。 -5.3通过归纳对添加和证明的公理化。-5.4通过归纳进行更多证明。-5.5使用直接定义。-5.6摘要。-5.7练习。-6有限集。-6.1简介。-6.2集合设置成员资格归纳的发电机。-6.3使用集合诱导的证明。-6.4定量量化。-6.5子集套件集均等心率。-6.6其他设置构造函数。理解。-6.8关于设定理解的推理。-6.9摘要。-6.10练习。-7有限地图。-7.1简介。-7.2基本的公理化。------- 7.3使用发电机的公理化。-7.4诱饵的提取和抽象。-7.5使用子公司定义。-7.6多态亚型和相关的感应诱导规则。-7.7 MAP GRONSENSION.- 7.8摘要 - 7.9练习。 -8.2基本的轴心化。-8.3 destructors.- 8.4列表之间的平等。-8.5列表上的运算符。- 8.6替代生成器集合。-8.7摘要。-8.8练习。-9布尔值。-9.1简介-9.2基本的公理化。-9.3布尔值算子的编队规则。 9.5摘要 - 9.6练习。定义S.- 10.3状态。-10.4功能和值。-10.5操作。-10.6验证证明。-10.7摘要。-10.8练习。 11.4一个示例重新校正证明。-11.5实施功能。-11.6实施偏见和无法实现的状态。-11.7摘要。-11.8练习。-12空中流量控制中的案例研究。-12.1简介 - 12.2空气交通控制系统。-12.3国家模型的形式化。-12.4顶级操作。改进步骤。-12.7结论备注 - 13个高级主题。-13.1简介-13.2作为数据类型的功能。-13.3比较元素 - 13.4递归类型定义。-13.5列举集，地图和序列。-13.6模式。-13.7其他表达式。-13.8其他类型。 14.2具有平等的谓词LPF。-14.3基本类型构造函数。-14.4自然数。-14.5有限集。-14.6有限地图 - 14.7有限序列。-14.8布尔值。-14.9规格。-14.10重新配置.- 14.11案例研究I：摘要规范。-14.12案例研究II：修订II：index.-符号索引 - 索引 - 索引规则。
1 Introduction.- 1.1 Background.- 1.2 How proofs arise in practice: an introductory example.- 1.3 A logical framework for proofs.- 1.4 Summary.- I A Logical Basis for Proof in VDM.- 2 Propositional LPF.- 2.1 Introduction.- 2.2 Basic axiomatisation.- 2.3 Derived rules reasoning by cases reasoning using contradiction.- 2.4 Using definitions: conjunction.- 2.5 Implication definedness further defined constructs.- 2.6 Summary.- 2.7 Exercises.- 3 Predicate LPF with Equality.- 3.1 Predicates.- 3.2 Types in predicates.- 3.3 Predicate calculus for LPF: proof strategies for quantifiers.- 3.4 Reasoning about equality: substitution and chains of equality.- 3.5 Extensions to typed predicate LPF with equality.- 3.6 Summary.- 3.7 Exercises.- 4 Basic Type Constructors.- 4.1 Introduction.- 4.2 Union types.- 4.3 Cartesian product types.- 4.4 Optional types.- 4.5 Subtypes.- 4.6 A note on composite types.- 4.7 Summary.- 4.8 Exercises.- 5 Numbers.- 5.1 Introduction.- 5.2 Axiomatising the natural numbers.- 5.3 Axiomatisation of addition and proof by induction.- 5.4 More on proof by induction.- 5.5 Using direct definitions.- 5.6 Summary.- 5.7 Exercises.- 6 Finite Sets.- 6.1 Introduction.- 6.2 Generators for sets set membership set induction.- 6.3 Proof using set induction.- 6.4 Quantification over sets.- 6.5 Subsets set equality cardinality.- 6.6 Other set constructors.- 6.7 Set comprehension.- 6.8 Reasoning about set comprehension.- 6.9 Summary.- 6.10 Exercises.- 7 Finite Maps.- 7.1 Introduction.- 7.2 Basic axiomatisation.- 7.3 Axiomatisation using generators.- 7.4 Extraction and abstraction of lemmas.- 7.5 Using subsidiary definitions.- 7.6 Polymorphic subtypes and associated induction rules.- 7.7 Map comprehension.- 7.8 Summary.- 7.9 Exercises.- 8 Finite Sequences.- 8.1 Introduction.- 8.2 Basic axiomatisation.- 8.3 Destructors.- 8.4 Equality between lists.- 8.5 Operators on lists.- 8.6 An alternative generator set.- 8.7 Summary.- 8.8 Exercises.- 9 Booleans.- 9.1 Introduction.- 9.2 Basic axiomatisation.- 9.3 Formation rules for boolean-valued operators.- 9.4 An example of a well-formedness proof obligation.- 9.5 Summary.- 9.6 Exercises.- II Proof in Practice.- 10 Proofs From Specifications.- 10.1 Introduction.- 10.2 Type definitions.- 10.3 The state.- 10.4 Functions and values.- 10.5 Operations.- 10.6 Validation proofs.- 10.7 Summary.- 10.8 Exercises.- 11 Verifying Reifications.- 11.1 Introduction.- 11.2 Data reification.- 11.3 Operation modelling.- 11.4 An example reification proof.- 11.5 Implementing functions.- 11.6 Implementation bias and unreachable states.- 11.7 Summary.- 11.8 Exercises.- 12 A Case Study in Air-Traffic Control.- 12.1 Introduction.- 12.2 The air-traffic control system.- 12.3 Formalisation of the state model.- 12.4 Top-level operations.- 12.5 First refinement step.- 12.6 Second refinement step.- 12.7 Concluding remarks.- 13 Advanced Topics.- 13.1 Introduction.- 13.2 Functions as a data type.- 13.3 Comparing elements of disjoint types.- 13.4 Recursive type definitions.- 13.5 Enumerated sets, maps and sequences.- 13.6 Patterns.- 13.7 Other expressions.- 13.8 Other types.- III Directory of Theorems.- 14 Directory of Theorems.- 14.1 Propositonal LPF.- 14.2 Predicate LPF with equality.- 14.3 Basic type constructors.- 14.4 Natural numbers.- 14.5 Finite sets.- 14.6 Finite maps.- 14.7 Finite sequences.- 14.8 Booleans.- 14.9 Specifications.- 14.10 Reifications.- 14.11 Case study I: abstract specification.- 14.12 Case study II: refinement.- Index of Symbols.- Index of Rules.