A practical method of documenting and verifying Ada programs with packages. Program Verification and Verification-Oriented Programming

被引：0

作者：

Luckham, David C. ^{[1
]}

Polak, Wolfgang ^{[1
]}

机构：

[1] Stanford University, Computer Systems Laboratory, United States

来源：

ACM SIGPLAN Notices | 1980年 / 15卷 / 11期

基金：

美国国家科学基金会;

关键词：

Formal specification;

D O I：

10.1145/947783.948648

中图分类号：

学科分类号：

摘要：

We present a method of formal specification of Ada programs containing packages. The method suggests concepts and guidelines useful for giving adequate informal documentation of packages by means of comments.The method depends on (1) the standard inductive assertion technique for subprograms, (2) the use of history sequences in assertions specifying the declaration and use of packages, and (3) the addition of three categories of specifications to Ada package declarations: (a) visible specifications, (b) boundary specifications, (c) internal specifications.Axioms and proof rules for the Ada package constructs (declaration, instantiation, and function and procedure call) are given in terms of history sequences and package specifications. These enable us to construct formal proofs of the correctness of Ada programs with packages. The axioms and proof rules are easy to implement in automated program checking systems. The use of history sequences in both in formal documentation and formal specifications and proofs is illustrated by examples. © 1980 ACM.

引用

页码：113 / 122