Axiomatic Semantics Flashcards
What are axiomatic semantics?
What is an assertion?
Give an example of an assertion.
(T/F) Axiomatic semantics are used for creating programs.
True.
Give an example of a Hoare triple.
What can be used to prove that a Hoare triple is valid?
- Axioms
- Inference Rules
They implicitly define the meaning of a program.
In axiomatic semantics, what notation is used to say that A is stronger then B, and B is weaker than A.
Out of the following triples, which one is the weakest.
(T/F) A stronger assertion has less elements in its set.
True.
Give an example of an inference rule notation.
(T/F) Inference rules can allow to strengthen precondition and weaken postcondition.
True.
Give an example of a sequence rule.
What is another way to write
Explain what logical variables are.
Prove the following using the assignment axiom.
E has to equal 0.
The summation is over an empty range, thus has a value of 0, the identity of +.
Create an inference for the following skip triple.
Create an inference for the following if triple.
Create an inference for the following triple.
Assignment Axiom
{Q[V :=E] and E is defined}
V := E
{Q}
What does the assignment axiom say about V and E?
It says that whatever is true about E beforehand, is true about V afterwards.
Use the assignment axiom to show the following triple is valid.
{ x = 0 }
x := x + 1
{ x = 1 }
- { x = 0 }
- { x + 1 = 1 }
x := x + 1
{ x = 1 }
If a triple cannot be proven using assignment axioms, what is an alternative?
Inference rules.
