2024/11/20 by Gurov, Dilian, Hähnle, Reiner
#68Q55 (Primary) 03B45 (Secondary) #F.3.1 #F.3.2 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Software Engineering (cs.SE)
paper · doi:10.48550/arxiv.2411.13125
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.