Statistics:
mean 21.750 (261.000/12) stddev 7.037 median 24.000 midrange 16.000-27.500 # avg 1 11.50 / 15 2 5.92 / 10 3 4.33 / 5
Prove the following using our axiomatic scheme.
{ i * k = n AND k mod 2 = 0 } k := k / 2; i := i * 2; {i * k = n }
Consider the following Ada program.
with Text_IO; use Text_IO; procedure Test is X : Integer; procedure A is begin X := 3; end A; procedure B is X : Integer; begin X := 4; A; Put_Line(Integer'Image(X)); end B; begin X := 2; B; Put_Line(Integer'Image(X)); end Test;
Consider the following grammar.
S -> a S b S | x
1. i * k = n AND k mod 2 = 0 implies (i * 2) * (k / 2) = n (Math fact) 2. { i * k = n AND k mod 2 = 0 } (Conseq: 1) { (i * 2) * (k / 2) = n } 3. { (i * 2) * (k / 2) = n } (Assignment) k := k / 2; { (i * 2) * k = n } 4. { i * k = n AND k mod 2 = 0 } (Seq: 2, 3) k := k / 2; { (i * 2) * k = n } 5. { (i * 2) * k = n } (Assignment) i := i * 2; {i * k = n } 6. { i * k = n AND k mod 2 = 0 } (Seq: 4, 5) k := k / 2; i := i * 2; {i * k = n }