Axiomatic Semantics

Question 1

What are axiomatic semantics?

Answer 1

Question 2

What is an assertion?

Answer 2

Question 3

Give an example of an assertion.

Answer 3

Question 4

(T/F) Axiomatic semantics are used for creating programs.

Answer 4

True.

Question 5

Give an example of a Hoare triple.

Answer 5

Question 6

What can be used to prove that a Hoare triple is valid?

Answer 6

• Axioms
• Inference Rules

They implicitly define the meaning of a program.

Question 7

In axiomatic semantics, what notation is used to say that A is stronger then B, and B is weaker than A.

Answer 7

Question 8

Out of the following triples, which one is the weakest.

Answer 8

Question 9

(T/F) A stronger assertion has less elements in its set.

Answer 9

True.

Question 10

Give an example of an inference rule notation.

Answer 10

Question 11

(T/F) Inference rules can allow to strengthen precondition and weaken postcondition.

Answer 11

True.

Question 12

Give an example of a sequence rule.

Answer 12

Question 13

What is another way to write

Answer 13

Question 14

Explain what logical variables are.

Answer 14

Question 15

Prove the following using the assignment axiom.

Answer 15

Question 16

Answer 16

E has to equal 0.

Question 17

Answer 17

The summation is over an empty range, thus has a value of 0, the identity of +.

Question 18

Create an inference for the following skip triple.

Answer 18

Question 19

Create an inference for the following if triple.

Answer 19

Question 20

Create an inference for the following triple.

Answer 20

Question 21

Assignment Axiom

{Q[V :=E] and E is defined}

V := E

{Q}

What does the assignment axiom say about V and E?

Answer 21

It says that whatever is true about E beforehand, is true about V afterwards.

Question 22

Use the assignment axiom to show the following triple is valid.

{ x = 0 }

x := x + 1

{ x = 1 }

Answer 22

2. { x = 0 }
3. { x + 1 = 1 }

x := x + 1

{ x = 1 }

Question 23

If a triple cannot be proven using assignment axioms, what is an alternative?

Answer 23

Inference rules.