Axiomatic semantics

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Axiomatic semantics" – news · newspapers · books · scholar · JSTOR (December 2021) (Learn how and when to remove this message)

Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs.^[1] 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.