Program Logics of Renominative Level with the Composition of Predicate Complement
Mykola S. Nikitchenko, Oksana Shkilniak, S.S. Shkilniak · 2019
Program logics are wildly used for software verification. Such logics are based on formal program models and reflect main program properties. Among various program logics, Floyd-Hoare logic and its variants take a spe- cial place because of its naturalness and simplicity. But such logics are oriented on total pre- and post-conditions, and in the case of partial conditions they be- come unsound. Different methods to overcome this problem were proposed in our previous works. One of the methods involves extension of program algebras with the composition of predicate complement. This permits to modify rules of the logic making them sound. Such modification requires introduction of unde- finedness conditions into logic rules. In this paper we continue our research of such logics. We investigate a special predicate logic called logic of renomina- tive (quantifier-free) level with the composition of predicate complement. This logic is a constituent part of the program logic. We introduce a special conse- quence relation for this logic, construct a sequent calculus, and prove its sound- ness and completeness.