Home
Scholarly Works
A logic for describing, not verifying, software
Journal article

A logic for describing, not verifying, software

Abstract

An important perquisite for verification of the correctness of software is the ability to write mathematically precise documents that can be read by practitioners and advanced users. Without such documents, we won't know what properties we should verify. Tabular expressions, in which predicate expressions may appear, have been found useful for this purpose. We frequently use partial functions in our tabular documentation. Conventional interpretations of expressions that describe predicates are not appropriate for our application because they do not deal with partial functions. Experience with this documentation has led us to choose a logic in which predicates are total but functions remain partial. We have found that this particular interpretation results in simpler expressions and is easily understood by practitioners.

Authors

Parnas DL

Journal

Erkenntnis, Vol. 43, No. 3, pp. 321–338

Publisher

Springer Nature

Publication Date

November 1, 1995

DOI

10.1007/bf01135377

ISSN

0165-0106

Contact the Experts team