Abstract
The proposed sound and relatively complete sequential system for proving the properties of regular programs is based on decomposition of a formula into parts. The inference rules follow the syntax of the programming constructs. This allows us to organize the proofs that follows the program structure. The same system is used to prove the properties of deterministic and nondeterministic programs, including partial and total correctness. Deterministic constructs are written in language P used here in a usual way. The most interesting rule of the proposed system is the antecedent rule for iteration. In this rule instead of an invariant and a bound function needed for proving a total correctness of programs with iteration [1] some formula variable is used. It allows to bury induction deeply in logic of the underlying language and the user of system is free from care about the utilization of the induction. This together with invertibility. of all inference rules allow us to construct the proof of total correctness of some program automatically and leave the problem to logic. Some proof-theoretical investigation of the system is carried out.
Preview
Unable to display preview. Download preview PDF.
References
K.R.Apt, E.R.Olderog. Introduction to program verification. Report CS-R9036, Dept. of Software Technology, CWI, August, 1990.
D.Harel, A.Pnueli and J.Stavi. A complete axiomatic system for proving deductions about recursive programs. Proc. 9 th Ann. ACM Symp. on Theory of Computing, 249–260, Boulder, Colorado, 1977.
Z.Manna. The correctness of programs. JCSS. 3, 119–127, 1969.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pliuškevičienė, A. (1992). Sequential calculus for proving the properties of regular programs. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023890
Download citation
DOI: https://doi.org/10.1007/BFb0023890
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55707-4
Online ISBN: 978-3-540-47276-6
eBook Packages: Springer Book Archive