Princeton University
Computer Science Dept.

Computer Science 441
Programming Languages
Fall 1998

Assignment 10
Not to be turned in
  1. Variables can be said to have both L-values and R-values, where the L-value of a variable is the location it denotes and the R-value is the value stored in that location. The environment keeps track of the locations corresponding to variables, while the store (or state) keeps track of the values stored in locations. Recall that the semantics of the assignment statement for most programming languages is usually given as follows: When V := E is executed, the L-value of V is first obtained from the environment (call it l), then the expression E is evaluated, and that resulting value is stored in the location l. While side-effects can create great confusion in terms of what the result of an assignment statement will be; in this problem, side-effects are not the problem!

    a) Describe in detail the effect of executing the Pascal assignment

    		a[a[i]] := a[i] + 1
    b) Is it always the case (in Pascal) that the value of L after executing assignment L := E is equal to the value of E before executing the command? I.e. if you execute the following code:
    		write(E); L := E; writeln(L);
    will the two values printed always be the same? For the purposes of this problem assume that the evaluation of E has no side effects. Hint : consider the assignment in part (a) with i = 2, a[2] = 2, a[3] = 0.

    c) What does this tell you about the validity of the axiomatic rule for assignment,{P [E / L]} L := E {P}, (e.g., if L = a[a[i]], E = a[i] + 1, and P is a[a[i]] = 3)? Suggest a restriction which makes it valid.

  2. Use the formal rules for axiomatic semantics given in the lecture notes to prove the correctness of the following program:

    {Precondition: n > 0}

    	i <- n
	fact <- 1
	while i > 0 do
		{assert:  ...}
		fact <- fact * i
		i <- i - 1
	end while
	{Postcondition:	fact = 1*2*...*n}
    Hint: You need to figure out the loop invariant before you can complete the proof. Your proof should take the same form as the one in the lecture notes - hand-waving is NOT acceptable.

    Note: If you prefer to use the weakest precondition rules in the text, be my guest, but I suspect you will find it easier to use those given in class instead