axiomatic semantics

{{Short description|Logic for proving computer program correctness}}

{{Semantics}}{{RefImprove|date=December 2021}}

Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs.{{Cite book|last=Winskel|first=Glynn|url=https://books.google.com/books?id=JzUNn6uUxm0C&q=%22Axiomatic+semantics%22|title=The Formal Semantics of Programming Languages: An Introduction|date=1993-02-05|publisher=MIT Press|isbn=978-0-262-73103-4|language=en}} It is closely related to Hoare logic.

Axiomatic semantics define the meaning of a command in a program by describing its effect on assertions about the program state. The assertions are logical statements—predicates with variables, where the variables define the state of the program.