Axiomatic Semantics Based on formal logic (first order predicate calculus) formal program verification Original purpose: Define axioms and inference rules in logic for each statement type Approach: in the language (to allow transformations of expressions to other expressions) The expressions are called and are either assertions Preconditions: An assertion before a statement states the relationships and constraints among variables that are true at that point in execution Postconditions: An assertion following a statement It is a good tool for correctness proofs, and an excellent framework for reasoning about programs It is much less useful for language users and compiler writers Meaning of Logic Symbols implies (if then … …) ⇒ if and only if, is necessary and sufficient for, is equivalent to ⇔ conjunction between propositions, means “and” ∧ disjunction between propositions, means “or” ∨ universal quantifier, means "for every", "for each", "for all" ∀ existential quantifier, means “there exists” ∃ therefore ∴ is an element of ∈ is not an element of ∉ not Axiomatic Semantics using Floyd Hoare Logic Axiomatic semantics is based on Hoare Logic named after computer scientist Sir Tony Hoare Based on that describe how execution of a statement changes the state triples of the computation Hoare Logic Setup
Axiomatic Semantics Based on formal logic (first order predicate calculus) Original purpose: formal program verification Approach: Define axioms and inference rules in logic for each statement type in the language (to allow transformations of expressions to other expressions) The expressions are called assertions and are either Preconditions: An assertion before a statement states the relationships and constraints among variables that are true at that point in execution Postconditions: An assertion following a statement It is a good tool for correctness proofs, and an excellent framework for reasoning about programs It is much less useful for language users and compiler writers Meaning of Logic Symbols ⇒ implies (if … then …) ⇔ if and only if, is necessary and sufficient for, is equivalent to ∧ conjunction between propositions, means “and” ∨ disjunction between propositions, means “or” ∀ universal quantifier, means "for every", "for each", "for all" ∃ existential quantifier, means “there exists” ∴ therefore ∈ is an element of ∉ is not an element of not Axiomatic Semantics using Floyd Hoare Logic Axiomatic semantics is based on Hoare Logic named after computer scientist Sir Tony Hoare Based on triples that describe how execution of a statement changes the state of the computation Hoare Logic Setup