I just watched ZJU Global Dialogue Series: Programming Language Semantics by Prof. Andrew Pitts, and one slide looks like this:
Styles of semantics
- Program logics
- Operational semantics
- Denotational semantics
but elsewhere, e.g. in Benjamin C. Pierce's Types and Programming Languages, I've seen operational and denotational semantics put side by side with axiomatic semantics. The explanation following that slide, talks about "proofs", which makes me think of proofs built on top of axioms, and therefore suggests to me that maybe "program logics" simply stands for "axiomatic semantics".
If that's not the case, then what's the difference between the two?