Program Logics Based on Algebras with the Composition of Predicate Complement
Mykola S. Nikitchenko, Oksana Shkilniak, S.S. Shkilniak · 2019
The formalism of program logics is the main instrument for software verification. Many such logics reflecting different properties of software systems were proposed. Floyd-Hoare logic and its variants are popular for program verification. But this logic is oriented on total pre- and post-conditions (predicates) and becomes unsound in the case of partial predicates. In our previous works we considered different methods to extend Floyd-Hoare logic for partial predicates. One of the methods involves program algebras with the composition of predicate complement. Introduction of this composition permits to modify rules of the logic making them sound, but the obtained logic becomes more complicated because it involves undefinedness conditions. In this paper we continue our research of such logics. We introduce special consequence relation and prove the soundness and completeness theorems for the case of logic of propositional level with the composition of predicate complement.