Consider the following Ada code, based on the parser of Project 1.
procedure Parse_Term is begin if Token.Category = Ident then Chomp(Ident); else Chomp(Num); end if; end Parse_Term; procedure Parse_Expr is begin if Token.Category = Semi then Chomp(Semi); else Parse_Term; Chomp(Plus); Parse_Expr; end if; end Parse_Expr;
Consider the following Ada code, based on the parser of Project 1.
procedure Parse is begin case Token.Category is when A => Chomp(A); while(Token.Category == A) Chomp(T_A); parse; Chomp(T_B); while(Token.Category == B) Chomp(T_B); parse; when B => Chomp(B); Chomp(T_B); Parse; Chomp(T_A); Parse; when C => Chomp(C); default: Put_Line("unexpected token: expected A, B, or C"); raise Parse_Error; end case; end Parse;
Prove the following using our axiomatic scheme. The notation fib(i) is used to represent the ith Fibonacci number.
{ a = fib(i) AND b = fib(i - 1) } c := a + b; { c = fib(i + 1) AND a = fib(i) }
Provide a step-by-step partial correctness proof for the following. Justify each step with one of the three rules below, or ``algebraic fact'' if the conclusion is algebraically true and involves no assertions.
{ z = xi } z := z * x; i := i + 1; { z = xi }
Prove the following using our axiomatic scheme
{ TRUE } if n mod 2 = 0 then n := n - 2; else n := n - 1; end if; { n mod 2 = 0 }
Say you are to prove the following using our axiomatic scheme.
{ n = 2k AND k >= 0 } -- The caret `^' represents exponentiation i := 0; j := n; while j > 1 loop j := j / 2; i := i + 1; end loop; { n = 2i }
Distinguish proofs of total correctness against proofs of partial correctness.
Consider the following Java program.
static class Test { static int a = 1; int f() { return a; } int main() { int a = 2; System.out.println(f()); } }
Many languages (such as Java, Ada, and ML) do static type checking, while others (such as PostScript, Scheme, and Smalltalk) use dynamic type checking.
expr -> SEMI | term PLUS expr
term -> IDENT | NUM
1. a = fib(i) AND b = fib(i - 1) (mathematical fact) IMPLIES a + b = fib(i + 1) AND a = fib(i) 2. { a = fib(i) AND b = fib(i - 1) } (Consequence: 1) { a + b = fib(i + 1) AND a = fib(i) } 3. { a + b = fib(i + 1) AND a = fib(i) } (Assignment) c := a + b; { c = fib(i + 1) AND a = fib(i) } 4. { a = fib(i) AND b = fib(i - 1) } (Sequence: 2, 3) c := a + b; { c = fib(i + 1) AND a = fib(i) }
1. z = xi implies z * x = xi + 1 (algebraic fact) 2. { z = xi } { z * x = xi + 1 } (consequence: 1) 3. { z * x = xi + 1 } z := z * x; { z = xi + 1 } (assignment) 4. { z = xi } z := z * x; { z = xi + 1 } (sequence: 3, 4) 5. { z = xi + 1 } i := i + 1; { z = xi } (assignment) 6. { z = xi } z := z * x; i := i + 1; { z = xi } (sequence: 4, 5)
1. TRUE AND n mod 2 = 0 implies (n - 2) mod 2 = 0 (mathematical fact) 2. { TRUE AND n mod 2 = 0 } (Consequence: 1) { (n - 2) mod 2 = 0 } 3. { (n - 2) mod 2 = 0 } (Assignment) n := n - 2; { n mod 2 = 0 } 4. { TRUE AND n mod 2 = 0 } (Sequence: 2, 3) n := n - 2; { n mod 2 = 0 } 5. TRUE AND n mod 2 /= 0 implies (n - 1) mod 2 = 0 (mathematical fact) 6. { TRUE AND n mod 2 /= 0 } (Consequence: 5) { (n - 1) mod 2 = 0 } 7. { (n - 1) mod 2 = 0 } (Assignment) n := n - 1; { n mod 2 = 0 } 8. { TRUE AND n mod 2 /= 0 } (Sequence: 6, 7) n := n - 1; { n mod 2 = 0 } 9. { TRUE } (Selection: 4, 8) if n mod 2 = 0 then n := n - 2; else n := n - 1; end if; { n mod 2 = 0 }
It allows for variables within functions that can remember values from previous calls to the function.
It is more space-efficient, as space is only allocated for the functions currently on the call stack.
Program execution is faster, as type-checking for each operation is expensive.
The code tends to be simpler, as it does not require type annotations.