Axiomatic semantics is an approach based on
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
for 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
*
Algebraic semantics (computer science) — in terms of algebras
*
Denotational semantics
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'' ...
— by translation of the program into another language
*
Operational semantics — in terms of the state of the computation
*
Formal semantics of programming languages
In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid string (computer science), strings in a programming language syntax. It is cl ...
— overview
*
Predicate transformer semantics — describes the meaning of a program fragment as the function transforming a
postcondition to the
precondition needed to establish it.
*
Assertion (computing)
References
Formal specification languages
Logic in computer science
Programming language semantics
{{Formalmethods-stub