On the Incorrectness of Unconditional Programs

S.A. Zhucov

Abstract


In the logical analysis of imperative programs, situations requiring the formulation of a negative statement about them have been little explored. Incorrectness logic is an exception to this rule, as it allows for the formulation of statements about possible incorrect program results relative to the logical specification. It has inspired the study of negative statements about the correctness of terminating programs, but within the framework of Hoare's traditional approach. Within the framework of an imperative, non-procedural language, the conditions under which negation must be used in Hoare triples for unconditional programs—that is, programs in which logical conditions are not used or not considered as a control mechanism—are investigated. Specifically, conditions are established under which the negation of a postcondition in a Hoare triple entails the negation of the Hoare triple itself, and, conversely, the negation of a Hoare triple entails the negation of its postcondition. Conditions are formulated under which a Hoare triple for the assignment operator is unsatisfiable. In the case of sequential composition of two programs, sufficient conditions for its incorrectness are identified, and it is also shown that sequential composition of two incorrect programs can be correct. The algorithmic undecidability of total correctness in the class of imperative non-procedural programs is proven.


Full Text:

PDF (Russian)

References


Apt K.R. Ten years of Hoar’s logic: A survey – Part 1 // ACM Transactions on programming languages and systems, 1984, v. 3, # 4, pp. 431-483.

Apt K.R., de Boer F.S., Olderog E.R. Verification of sequential and concurrent programs, 3rd Edition. N.Y.:Springer, 2009. 502 p.

Kemmerer R.A. Testing formal specification to detect design errors // IEEE Transactions on software engineering, 1985, v. SE-I 1, # 1, pp. 32-43.

Konighofer R., Hofferek G., Bloem R. Debugging formal specifications using simple counterstrategies // IEEE: Formal Methods in Computer-Aided Design, 2009, pp. 152–159.

O’Hearn P.W. Incorrectness logic // Proceedings ACM Programming languages, 2020, v. 4, POPL, Article 10, pp. 10.1-10.32.

Mills H. D. The new math of computing programming // Communications of the ACM, 1975, v. 18, # 1, pp. 43 – 48.

Matiyasevich Y. On Hilbert’s tenth problem. Calgary: PIMS, 2000. 71 p.

Carnicer J., Gasca M. Evaluation of multivariate polynomials and their derivations // Mathematics of computation, 1990, v. 54, # 189, pp. 231-243.

Mal'cev A. I. Algoritmy i rekursivnye funkcii. M: Nauka, 1986. 368 s.

Grabowski M. On relative incompleteness of logic for total correctness // Lecture notes in computer science, 1985, v. 195, pp. 118-127.

Clarke E., German S., Halpern J. Effective axiomatizations of Hoare logics // JACM, 1983, v. 30, # 3, pp. 612-636.

Bicarregui J., Hoare C.A.R., Woodcock J. The verified software repository: a step towards the verifying compiler // Formal Aspects of Computing, 2006, v. 18, # 2, pp. 143-151.


Refbacks

  • There are currently no refbacks.


Abava  Кибербезопасность ИТ конгресс СНЭ

ISSN: 2307-8162