Sequent Calculus for a Program-oriented Predicate Logic over Complex-Named Data
Mykola S. Nikitchenko, Oksana Shkilniak, S.S. Shkilniak · 2020
The multiplicity of data structures used in programming complicates analysis and verification of software systems. Nominative data aim to serve as a unified model of different data structures. The main feature of such data is usage of complex names to access or modify data components. This leads to a problem considered in the paper: to define and investigate a class of nominative data with complex names (complex-named data), operations on this class, properties of this class (specified as predicates over such data), and compositions of such predicates. We define an algebra of predicates over data with complex names and specify a first order logic that describes general properties of such algebras. For this logic we construct a sequent calculus and prove its soundness and completeness.