On the incorrectness of a branching program and loop

S. A. Zhucov

Abstract


Within the Hoare approach to program correctness, the incorrectness of a certain type of branching program, which can model decision tables with bounded input, and a loop without subloops is studied. The relationships between the code structure of such a branching program and the postconditions that lead to incorrectness are studied. Satisfiable postconditions are given under which any given branching program is incorrect. Sufficient properties of the postcondition are determined under which a loop of the above type will be incorrect, as well as a logical expression linking loop invariants to the postcondition in the case of loop incorrectness. Program incorrectness can be expressed as the falsity of a certain statement describing the properties of the program postcondition in the case where the program function is defined recursively. Specifically, a class of recursive definitions D was identified such that the incorrectness of a program for computing a function defined by D is equivalent to the violation of certain properties described by a logical assertion constructed from D. An example of the definitions of two mutually recursive functions is given, the incorrectness of whose programs is analyzed through the construction of logical assertions describing the properties of these functions. The negation of the assertions constructed expresses the incorrectness of the corresponding programs.


Full Text:

PDF (Russian)

References


Baier C., Katoen J. P. Principles of model checking. The MIT Press, 2008. 975 p.

Glushkov V.M. Teorema o nepolnote formal'nyh teorij s pozicii programmista //Kibernetika, 1979, # 2, s. 15.

Borger E., Gradel E., Gurevich Y. The classical decision problem. Springer-Verlag, 2001. 482 p.

Hambi Je. Programmirovanie tablic reshenij.  M.: Mir, 1976.  86 s.

Frajtag G. i dr. Vvedenie v tehniku raboty s tablicami reshenij.  M.: Jenergija, 1979. – 88 s.

Grigor'ev D.Ju. Algebraicheskaja slozhnost' vychislenija bilinejnyh form //Zh. vychisl. matem. i matem. fiz., 1979, t.19, # 3, s. 563 – 580.

Ben-Or M. Lower bounds for algebraic computation trees //STOC83: Proc. of the fifteenth annual ACM symposium on theory computing, 1983, p. 80 86.

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

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

Pak K. The Matiyasevich theorem. Preliminaries. //Formalized mathematics, 2017, v. 25, # 4, p. 315 – 322.

S.-W. Lin, J. Sun, H. Xiao, Y. Liu, D. Sanán, H. Hansen Fib: Squeezing loop invariants by interpolation between forward/backward predicate transformers // in 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2017, pp. 793– 803.

Linger R., Mills H., Uitt B. Teorija i praktika strukturnogo programmirovanija. – M.: Mir, 1982.  408 s.

Meyer A.R., Ritchie D.M. The complexity of loop programs // Proceedings 22nd National ACM Conference, 1967, pp. 465 – 470.

Constable R.L., Borodin A.B. Subrecursive programming languages, Part I: Efficiency and program structure //Journal of ACM, 1972, v. 19, # 3, pp. 526 – 568.

Mazzanti S. Plain bases for classes of primitive recursive functions //Mathematical logic quarterly, 2002, v. 48, # 1, pp. 93 – 104.

Tsichritzis D. A note on comparison of subrecursive hierarchies // Information processing letters, 1971, v. 1, pp. 42 – 44.

Tsichritzis D. The equivalence problem of simple programs // Journal of ACM, 1970, v. 17, # 4, pp. 729 – 738.

McCarthy J. Towards a mathematical science of computation // Proc. IFIP Congress, 1962, ed. C.M. Popplewell, Ams.:Norh-Holland, pp. 21 – 28.


Refbacks

  • There are currently no refbacks.


Abava  Кибербезопасность Monetec 2026 СНЭ

ISSN: 2307-8162