CMPSC 461: Programming Language Concepts Assignment 7 Solution
Problem 1 [8pt] Prove that the following two Hoare triples are valid. (Hint: in predicate logic P1 ⇒ P2 is equivalent to ¬P1 ∨ P2).
a) (4pt)
{x = 1}
y := x + 2; y := y * 3; {y > 8}
Solution:
wp(y:=x+2;y:=y*3, y > 8) = wp(y:=x+2, wp(y:=y*3, y > 8)) = wp(y:=x+2, y ∗ 3 > 8)
= (x + 2) ∗ 3 > 8
Moreover, the precondition x = 1 implies that (x + 2) ∗ 3 = 9, hence, the weakest precondition
(x + 2) ∗ 3 > 8 holds. b) (4pt)
{x = 2, y = 3}
if (x<1) y := 5; else y := y - 1; {y = 2}
Solution:
wp(if (x<1) y:=5; else y:=y-1,y=2)=((x<1)⇒wp(y:=5,y=2))∧
((x ≥ 1) ⇒ wp(y:=y-1, y = 2))
= ((x < 1) ⇒ 5 = 2) ∧ ((x ≥ 1) ⇒ y − 1 = 2) = ((x < 1) ⇒ false) ∧ ((x ≥ 1) ⇒ y = 3)
We can simplify the last form to ((x ≥ 1) ∨ false) ∧ ((x < 1) ∨ (y = 3)) (using the hint), which is further simplified to (x ≥ 1) ∧ ((x < 1) ∨ (y = 3)). Finally, it is easy to check that the precondition x = 2 ∧ y = 3 implies that (x ≥ 1) and y = 3. Hence, the weakest precondition is true.
Problem 2 [12pt] Below is the pseudo code that computes 2x + 3y, along with the pre- and post-conditions to be verified.
{z = 2x ∧ n = 0 ∧ y > 0} while (n < y) {
z = z + 3;
n = n + 1; }
{z = 2x + 3y}
Write down a loop invariant and prove the correctness of this program. That is, write down an invariant, and show that the loop invariant is 1) true before the first execution of the loop, 2) true after the execution of each loop iteration, given that the loop condition and the invariant are both true before the iteration, and 3) strong enough to prove the correctness of the code (i.e., z = 2x + 3y is true after the loop, if it terminates).
1/4
Solution:
The invariant is n ≤ y ∧ z = 2x + 3n. We use I to represent this loop invariant.
Condition 1): easy to check that z = 2x ∧ n = 0 ∧ y > 0 implies I. Condition 2): we need to check the following Hoare triple is true:
{n < y ∧ I} z = z + 3; n = n + 1; {I}
Based on the postcondition, we can compute that the weakest precondition is
n + 1 ≤ y ∧ z + 3 = 2x + 3(n + 1) n ≤ y − 1 ∧ z = 2x + 3n
which can be simplified as
So the Hoare triple above is correct since n < y ∧ I implies the formula above (note that n is an integer, so
n ≤ y − 1 is the same as n < y ).
Condition 3): Easy to check that n ≥ y ∧ I implies the postcondition z = 2x + 3y.
Problem 3 [12pt] Consider the following Java classes:
class A {
public int foo () { return 1;}
public void message () { System.out.println( "A"); }
}
class B extends A {
public void message () { System.out.println( "B"); } }
class C extends A {
public int foo() {return 3;}
}
class D extends C {
public void message () {System.out.println( "D");} }
a) (8pt) Draw the virtual tables of classes A, B, C, D, and the code implementations that they point to.
Assignment 7, Solution, Cmpsc 461 2020 Fall 2/4
A’s vtable C’s vtable
foo code (return 1)
foo code (return 3)
foo
foo
message
foo
message
message code (print “A”)
message code (print “B”)
message
B’s vtable D’s vtable
message code (print “D”)
foo
message
b) (4pt) Consider the following function:
void func(C c) { c.message(); }
With subtype polymorphism, this function prints “A” given an instance of class C; prints “D” given an instance of class D. Give the pseudo code for the body of func after compilation to explain how does this happen with dynamic dispatching. Assume that the base address of c is stored in a pointer this, and that the target machine has 4-byte addresses. You can ignore the calling sequence (e.g., save and restore registers, store return address and so on).
Solution:
The compiled code looks like:
vt = *this; // find the vtable from the object’s base address call *(vt+4); // vt+4 is the address of function "message"
Problem 4 [12pt] Consider the heap state as shown below before garbage collection:
a) (3pt) For the Mark-and-Compact algorithm, what objects remain on the heap after collection? Do they stay in the same location after collection?
Solution:
Objects A, B, D, E, F remain on the heap after collection. No.
b) (9pt) Consider algorithms Mark-and-Sweep, Mark-and-Compact, Stop-and-Copy. For each of them, write down the objects being visited during the collection in sequence. Assume 1) reachability analysis uses depth-first search, which will skip objects that have already been visited, 2) search starts from p, and then q, 3) when the entire heap is traversed, objects are visited from left to right. You don’t need to write down the newly created object copies, if any.
Solution:
Mark-and-Sweep: A, D, F, E, B (Mark), A, B, C, D, E, F, G (Sweep).
Stack p
q
Heap
A
B
C
D
E
F
G
Assignment 7, Solution, Cmpsc 461 2020 Fall 3/4
Mark-and-Compact: A, D, F, E, B (Mark), A, B, C, D, E, F, G (Compute new addresses), A, B, C, D, E, F, G (Move objects to new address).
Stop-and-Copy: A, D, F, E, B.
Problem 5 [6pt] For each of the following data characteristics, briefly explain which of the garbage col- lection algorithms discussed in class (Mark and Sweep, Mark and Compact, Stop and Copy) would be the most appropriate and why. Make no other assumptions than those given.
a (3pt) All objects are of the same size and many have relatively long lifetime.
Solution:
Mark and sweep is the best since most objects have relatively long lifetime, and it avoids the cost of copying data. Moreover, since objects are of the same size, it does not introduce fragmentation.
b (3pt) Most objects have short lifetime and data locality greatly improves application’s performance.
Solution:
Stop and copy is suitable for data with short lifetime. It also eliminates fragmentation, and hence, im- proves data locality.
Assignment 7, Solution, Cmpsc 461 2020 Fall 4/4