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: example and proof
1. Axiomatic semantics: example and proof
2. 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?
3. Other questions
Assume that variables are integers and initialized.
What about overflow or underflow of the operations "+" or "-"?
And what about data types that are not defined for "+" or "-"?
4. 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?
5. Proof: start
x = y ^ x;
y = y ^ x;
x = x ^ y;
// { post: (x = a) and (y = b) }
6. Proof: step #1
x = y ^ x;
y = y ^ x;
// { #1: ((x ^ y) = a) and (y = b) }
x = x ^ y;
// { post: (x = a) and (y = b) }
7. Proof: step #2
x = y ^ x;
// { #2: ((x ^ (y ^ x)) = a) and ((y ^ x) = b) }
y = y ^ x;
// { #1: ((x ^ y) = a) and (y = b) }
x = x ^ y;
// { post: (x = a) and (y = b) }
We need to simplify
((x ^ (y ^ x))).
8. Truth table
Let us start with the logical expression and extended truth table for logical equivalence.
x y | x ^ ( y ^ x )
-------------------
0 0 | 0 0 ( 0 0 0 )
0 1 | 0 1 ( 1 1 0 )
1 0 | 1 0 ( 0 1 1 )
1 1 | 1 1 ( 1 0 1 )
Note that it appears to simplify to
y.
9. Truth table proof
Let us start with the logical expression and extended truth table for logical equivalence.
x y | ( x ^ ( y ^ x ) ) = y
---------------------------
0 0 | ( 0 0 ( 0 0 0 ) ) 1 0
0 1 | ( 0 1 ( 1 1 0 ) ) 1 1
1 0 | ( 1 0 ( 0 1 1 ) ) 1 0
1 1 | ( 1 1 ( 1 0 1 ) ) 1 1
10. Proof: step #3
// { #3: (y = a) and ((y ^ (y ^ x)) = b) }
x = y ^ x;
// { #2: (y = a) and ((y ^ x) = b) }
// { #2: ((x ^ (y ^ x)) = a) and ((y ^ x) = b) }
y = y ^ x;
// { #1: ((x ^ y) = a) and (y = b) }
x = x ^ y;
// { post: (x = a) and (y = b) }
We need to simplify
((x ^ (y ^ x))) (again).
11. Proof: step #3 (simplified)
// { #3: (y = a) and (x = b) }
x = y ^ x;
// { #2: (y = a) and ((y ^ x) = b) }
// { #2: ((x ^ (y ^ x)) = a) and ((y ^ x) = b) }
y = y ^ x;
// { #1: ((x ^ y) = a) and (y = b) }
x = x ^ y;
// { post: (x = a) and (y = b) }
Note: The exclusive or approach does not have the same risk of overflow or underflow.
12. Lessons learned
Axiomatic semantics can be used to both determine what code does and to develop new code from goals.
Mathematical logic (e.g., truth table logic), algebra, etc., may be needed to complete the proof. Usually some insight/intuition is needed to make the mental jump.
13. End of page
