Axiomatic semantics

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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

See also[edit]