Axiomatic semantics

Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs.[1] It is closely related to Hoare logic.

Semantics
  • Linguistic
  • Logical
Subfields
  • Computational
  • Lexical (lexis, lexicology)
  • Statistical
  • Structural
Topics
  • Analysis
  • Compositionality
  • Context (language use)
    • Prototype theory
    • Force dynamics
  • Semantic feature
  • Semantic gap
  • Theory of descriptions
Analysis
Applications
Semantics of
programming languages
Types
Theory
  • Language
  • Linguistics

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 — by translation of the program into another language
  • Operational semantics — in terms of the state of the computation
  • Formal semantics of programming languages — 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
  1. Winskel, Glynn (1993-02-05). The Formal Semantics of Programming Languages: An Introduction. MIT Press. ISBN 978-0-262-73103-4.


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.