Extended Floyd-Hoare Logic over Relational Nominative Data

The classical Floyd-Hoare logic is defined for the case of total pre- and postconditions and partial programs (i.e. programs can be undefined on some input data, but conditions must be defined on all data). In this paper we propose an extension of this logic for the case of partial conditions and partial programs over structured data. These data are based on two constructing primitives: naming and relational structuring and are called relational nominative data. They can conveniently represent many data structures used in programming. The semantics of the proposed logic is represented by special algebras of partial functions and predicates over relational nominative data. Operations of these algebras are called compositions. We present an inference system for the mentioned logic and propose an approach to its formalization in Mizar proof assistant. The obtained results can be used in software verification.