One-page version suitable for printing.
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.