12. Hoare Logic Flashcards
What is formal specification?
Using mathmatical notation to give a precise description of what a program should do
What is formal verification?
Using logical rules to mathematically prove that a program satisfies a formal speficification
What are denotional semantics?
Construct mathmatical objects that describe meaning
programs = functions: [[C]] : State -> State
What are operational semantics?
Describes the steps of computation during program execution
What are axiomatic semantics?
Define axioms and rules of some logic of programs
Hoard logic {P} C {Q}
What is the specification of a Hoare triple {P} C {Q}?
Given a state the satisfies preconditions P, executing a program C (and assuming termination) results in a state that satisfies postconditions Q
What is total correctness?
Partial correctness + termination
What is the assignment axiom (Hoare)?
What is the sequencing rule (Hoare)?
What is the skip axiom (Hoare)?
What is the conditional rule (Hoare)?
What is precondition strengthening (Hoare)?
What is postcondition weakening?
What is the while rule (Hoare)?
