Review for Quiz 1

Syntax and parsing

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.

Solution

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.

Solution

Program proofs

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

Solution

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 = xⁱ }
z := z * x;
i := i + 1;
{ z = xⁱ }

Solution

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 = 2^k AND k >= 0 }     -- The caret `^' represents exponentiation
i := 0;
j := n;
while j > 1 loop
    j := j / 2;
    i := i + 1;
end loop;
{ n = 2ⁱ }

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.

Solution

Question 1-7

Distinguish proofs of total correctness against proofs of partial correctness.

Solution

Binding time

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?

Solution

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.

Solution

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.

Solution