Send
Close Add comments:
(status displays here)
Got it! This site uses cookies. You consent to this by clicking on "Got it!" or by continuing to use this website.nbsp; Note: This appears on each machine/browser from which this site is accessed.
Axiomatic semantics: assignment statement
1. Axiomatic semantics: assignment statement
2. Assignment statement
The C assignment statement
x = e;
where
x is a variable
e is an expression
has as the operational semantics,
evaluate the expression e to a value, and
destructively replace the variable x with that value.
3. Assignment rule
The axiomatic semantics for the assignment statement, or
assignment rule, is as follows.
// { 2: p where e replaces x }
x = e;
// { 1: p }
In showing program correctness, always work backwards from the goal, even though program execution proceeds forward from the initial point of the program. The numbers "
1:", "
2:", etc., are not usually written, but are included so that you can see the order in which the assertions are used.
The two steps in replacing
x with
e are as follows.
Substitute e for x in p.
Simplify the result as much as possible and/or as needed.
4. Example 1
Apply the rules by working backwards.
// { 2: x = 7 ➜ 7 = 7 ➜ true }
x = 7;
// { 1: x = 7 }
5. Example 2
Interpretation: The assignment statement
x = 7;
will always result in in
x having the value of
7, since the assignment rule, working backwards, derives true.
6. Example 3
Apply the rules by working backwards.
// { 2: x = 5 ➜ (x+3) = 5 ➜ x = 2 }
x = x + 3;
// { 1: x = 5 }
Interpretation: The assignment statement
x = x + 3;
will result in
x having the value of
5 if and only if
x has the value of
2 before the assignment statement is executed.
7. Example
// { 2: p ➜ p }
x = x;
// { 1: p }
Interpretation: Whatever is true before the assignment statement
x = x;
is executed will be true after the assignment statement is executed.
8. Swap routine
Suppose that we want to write statements to exchange the values of
x and
y. The precondition and postcondition are as follows.
// { pre: (x = a) and (y = b) }
... code to swap values ...
// { post: (x = b) and (y = a) }
9. First attempt
Will the following work?
x = y;
y = x;
10. Apply the rules
Apply the rules by working backwards.
// { pre: (x = a) and (y = b) }
// Meet in the middle (are there contradictions at this point?)
// { 4: y = b = a = x }
// { 3: (x = a) and (y = b) and (y = a) }
// { 2: (y = b) and (y = a) }
x = y;
// { 1: (x = b) and (x = a) }
y = x;
// { post: (x = b) and (y = a) }
Interpretation: The statements
x = y;
y = x;
will correctly swap the values in
x and
y if and only if
x and
y have the same initial values. Notice that we get this result without thinking operationally. We only have to apply the rules and interpret the results.
Remember Miller's Law (one can only keep about up to 7 things in memory at once).
Any contractions in the middle must be resolved. If not, the code is not correct.
11. Second attempt
Will the following work?
t = y;
y = x;
x = t;
12. Apply the rules
Apply the rules by working backwards.
// { pre: (x = a) and (y = b) }
t = y;
// { 2: (t = b) and (x = a) }
y = x;
// { 1: (t = b) and (y = a) }
x = t;
// { post: (x = b) and (y = a) }
13. Suppose
Suppose that we had written the following.
y = t;
t = x;
x = y;
What happens when we apply the rules?
14. Exercise
What does the following C code do? Use assertions and the assignment rule to justify your answer.
x = y - x;
y = y - x;
x = x + y;
Can you explain it operationally?
If not, how do you expect to explain anything more complicated, as the above code consists of three assignment statements with a total of two different variables?
15. Apply the rules again
Apply the rules by working backwards.
// { pre: (y = b) and (x = a) }
// { 3: (y = b) and ((y-(y-x)) = a) }
x = y - x;
// { 2b: (y = b) and ((y-x) = a) }
// { 2a: ((x+(y-x)) = b) and ((y-x) = a) }
y = y - x;
// { 1: ((x+y) = b) and (y = a) }
x = x + y;
// { post: (x = b) and (y = a) }
16. Exam help
{ 2:before: p where e replaces x }
x = e;
{ 1:after: p }
17. End of page
