Review for Quiz 1

Question 1-1

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;
Give an BNF grammar that describes the language that Parse_Expr accepts. The terminals of the language are PLUS, SEMI, IDENT, and NUM.

Question 1-2

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;
Give an EBNF grammar describing what language this function accepts. Your grammar should have only one nonterminal (name it S) and three nonterminals, A, B, and C.

Question 1-3

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) }

Question 1-4

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 }

Question 1-5

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 }

Question 1-6

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 }
What is the loop invariant that will allow you to write the proof? Do not write the proof, just the invariant. Partial credit will be given for partially correct invariants.

Question 1-7

Distinguish proofs of total correctness against proofs of partial correctness.

Question 1-8

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());
    }
}
  • a. If Java used dynamic variable scoping, what would it output?

  • b. If Java used static variable scoping, what would it output?

  • c. Does Java use static or dynamic scoping?

Question 1-9

Recall from class that FORTRAN uses static variable allocation, while most other languages (including Ada and Java) use stack-dynamic variable allocation.

  • a. Name and explain an advantage of static variable allocation over stack-dynamic variable allocation.

  • b. Name and explain an advantage of stack-dynamic variable allocation over static allocation.

Question 1-10

Many languages (such as Java, Ada, and ML) do static type checking, while others (such as PostScript, Scheme, and Smalltalk) use dynamic type checking.

  • a. Name and explain an advantage of compile-time type checking over run-time type checking.

  • b. Name and explain an advantage of run-time type checking over compile-time type checking.

Solutions

Solution 1-1

expr -> SEMI | term PLUS expr

term -> IDENT | NUM

Solution 1-2

S -> A {A} S B {B} S | B S A S | C

Solution 1-3

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) }

Solution 1-4

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)

Solution 1-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 }

Solution 1-6

n = j 2i AND j >= 1

Solution 1-7

A proof of total correctness includes arguments that the program terminates. A partial-correctness proof may omit this fact - it proves that if the program terminates, then it reaches its conclusion correctly.

Solution 1-8

  • a. 2

  • b. 1

  • c. Java uses static scoping. (It also uses dynamic variable allocation (via the stack), but that's another issue entirely.)

Solution 1-9

  • a. It is marginally more efficient because the computer can use direct loads instead of indirect loads.

    It allows for variables within functions that can remember values from previous calls to the function.

  • b. It is much more conducive to recursion, because each recursive call gets its own set of variables.

    It is more space-efficient, as space is only allocated for the functions currently on the call stack.

    Solution 1-10

    • a. Programmer errors are detected at compile-time, so that debugging happens more reliably and faster.

      Program execution is faster, as type-checking for each operation is expensive.

    • b. It allows more flexibility to the programmer, so that variables can mean different things at different times.

      The code tends to be simpler, as it does not require type annotations.