Comp2212w1 Comp2212 201314 02 [623137]

UNIVERSITY OF SOUTHAMPTON COMP2212W1
SEMESTER 2 EXAMINATION 2013/2014
PROGRAMMING LANGUAGE CONCEPTS
Duration: 120 mins (2 Hours)
Y ou must enter your Student: [anonimizat]:Question Marks
A
B/
B/
B/
Answer ALLquestions from section A (30 marks)
and THREE of the five questions from section B (45 marks).
This examination is worth 75%. The coursework is worth 25%.
University approved calculators MAY be used.
Each answer must be completely contained within the designated space under
its question. No credit will be given for answers presented elsewhere.
Y ou are advised to write using a soft pencil so that you may readily correct
mistakes with an eraser.
Y ou may use blue books for scratch—they will be discarded without being
looked at.
A foreign language translation dictionary (paper version) is permitted provided it
contains no notes, additions or annotations
Copyright c
2014 University of Southampton Number of pages 25

COMP2212W1
Accompanying Reference Sheet
-calculus of Booleans and Products
The syntax of terms, values and types are
t::= true Constant true
false Constant false
iftthentelset Conditional
x Variable
x:T:t Abstraction
tt Application
(t;t) Pairing
fstt First projection
sndt Second projection
v::= true True value
false False value
x:T:t Abstraction value
(v;v) Pair of values
T::=Bool Type of Booleans
T!T Type of functions
TT Product Type
The evaluation rules are
iftrue thent2elset3!t2 iffalse thent2elset3!t3
t1!t0
1
ift1thent2elset3!ift0
1thent2elset3
(x:T:t)v!t[v=x]t1!t0
1
t1t2!t0
1t2t2!t0
2
vt2!vt0
2
fst(v1;v2)!v1 snd(v1;v2)!v2
t1!t0
1
(t1;t2)!(t0
1;t2)t2!t0
2
(v;t2)!(v;t0
2)
Copyright c
2014 University of Southampton Page 2 of 25

COMP2212W1
The type rules are
`true :Bool `false :Bool
`t1:Bool`t2:T`t3:T
`ift1thent2elset3:T
x:T2
`x:T;x:T1`t:T2
`x:T1:t:T1!T2
`t1:T2!T1`t2:T2
`t1t2:T1
`t1:T1`t2:T2
`(t1;t2) :T1T2`t:T1T2
`fstt:T1`t:T1T2
`sndt:T2
Where is a type context given by the grammar ::=;j;x:T
Copyright c
2014 University of Southampton Page 3 of 25 TURN OVER

COMP2212W1
Section A
Do not write in this space 
Copyright c
2014 University of Southampton Page 4 of 25

COMP2212W1
A 1
(a) Define static binding anddynamic binding . (2 marks)
(b) List one advantage and one disadvantage of dynamic type binding. (2 marks)
(c) In functional programming languages, what are the main differences be-
tween the call-by-name and call-by-value evaluation strategies? (2 marks)
Copyright c
2014 University of Southampton Page 5 of 25 TURN OVER

COMP2212W1
A 2
(a) Explain what is typically meant by the terms static typing anddynamic typ-
ing. (2 marks)
(b) The two properties usually used to define type safety for static languages
areprogress andpreservation . Define these concepts in terms of a typing
relation and a small step evaluation relation. (2 marks)
(c) Consider the simply typed lambda calculus with Booleans and Products
given in the accompanying reference sheet. Progress and preservation
holds for this language. Suppose we add an extra type rule as follows:
`t:T
`(fstt;sndt) :T
Do the properties of progress and preservation still hold for this extended
type system? Explain your answer. (2 marks)
Copyright c
2014 University of Southampton Page 6 of 25

COMP2212W1
A 3
(a) Explain what is meant by a deterministic small step reduction relation. (2 marks)
(b) Consider the lambda calculus of Booleans and Products given in the ac-
companying reference sheet. Show the sequence of small step reductions
for the following term:
(f: (Bool!Bool)Bool:(fstf)(sndf)))((b:Bool:ifbthen false else true );true)
(3 marks)
(c) Is the small step semantics for the -calculus of Booleans and Products
deterministic? Explain your answer. (1 marks)
Copyright c
2014 University of Southampton Page 7 of 25 TURN OVER

COMP2212W1
A 4The Java code below is part of an implementation of a concurrent stack that
uses the compareAndSet instruction in order to ensure consistency of the stack
data structure.
public class ConcurrentStack <E> {
AtomicReference<Node<E>> top = new AtomicReference<Node<E>>();
public void push(E item) {
Node<E> newHead = new Node<E>(item);
Node<E> oldHead;
do {
oldHead = top.get();
newHead.next = oldHead;
} while (!top.compareAndSet(oldHead, newHead));
}
…
}
(a) Explain the behaviour of compareAndSet . (2 marks)
Copyright c
2014 University of Southampton Page 8 of 25

COMP2212W1
(b) A correct thread-safe implementation can alternatively be obtained by us-
ing the Java synchronized keyword instead of compareAndSet . Write the
code for this alternative implementation, and compare and contrast the two.
(4 marks)
Copyright c
2014 University of Southampton Page 9 of 25 TURN OVER

COMP2212W1
A 5
(a) Give a formal definition of the concept of bisimulation . (2 marks)
(b) Consider the two labelled transition systems below.
x0
a
x1
aXXb//x2y0
a
y1
a
b//y2
y3
aXXb//y4
Show thatR=f(x0;y0);(x1;y1);(x2;y2);(x1;y3);(x2;y4)gis a bisimulation.
(4 marks)
Copyright c
2014 University of Southampton Page 10 of 25

COMP2212W1
Do not write in this space 
Copyright c
2014 University of Southampton Page 11 of 25 TURN OVER

COMP2212W1
Section B
Do not write in this space 
Copyright c
2014 University of Southampton Page 12 of 25

COMP2212W1
Do not write in this space 
Copyright c
2014 University of Southampton Page 13 of 25 TURN OVER

COMP2212W1
B 6
(a) Consider the simple BNF specification below:
<ifstm> ::=if(<boolexp> )<stmt>
jif(<boolexp> )<stmt> else <stmt>
<boolexp> ::=truejfalse
<stmt> ::=<ifstm>jskip
For each of the following, state whether or not the string is generated by the
grammar (assuming top level non-terminal <stmt> )
(i)if(true )if(false )else skip
(ii)if(true )if(false )skip else skip
(iii)if(true )true else false
(iv)if(true )if(true )if(true )if(true )if(true )skip
(4 marks)
(b) Explain what it means for a BNF specification to be ambiguous . Why is
ambiguity typically considered to be a problem? (3 marks)
Copyright c
2014 University of Southampton Page 14 of 25

COMP2212W1
(c) With the aid of an example, show that the BNF specification given in Part
(a) is ambiguous. (3 marks)
(d) Extend the grammar to obtain a more realistic set of boolean expressions.
In particular, expressions can contain boolean variables, binary logical op-
erations^and!, and a unary operation :. Design your grammar so that ^
associates to the left, while !associates to the right (i.e. a^b^cshould
mean ((a^b)^c)whilea!b!cshould mean (a!(b!c)).(5 marks)
Copyright c
2014 University of Southampton Page 15 of 25 TURN OVER

COMP2212W1
B 7 This question refers to a subset of the typed -calculus of Booleans and
Products. Consider the type rules for terms of this language as given in the
accompanying reference sheet. Below we have an incomplete and faulty OCaml
implementation of the typing relation for this language.
exception TypeError;;
type typ = TyBool | TyPair of typ * typ | TyFun of typ * typ ;;
type exp = TmTrue | TmFalse | TmIf of exp * exp * exp | TmPair of exp * exp |
TmAbs of string * typ * exp | TmApp of exp * exp |
TmVar of string ;;
type context = Context of ???
let rec getType ctx str = ???
let rec addBind ctx str ty = ???
let rec typeOf ctx t = match t with
TmTrue -> TyTrue
| TmFalse -> TyFalse
| TmIf (b, t1, t2) ->
(match (typeOf ctx b) with
TyBool -> (let ty1 = typeOf ctx t1 in
let ty2 = typeOf ctx t2 in
match (ty1=ty2) with
true -> ty1
| false -> ty2 )
| _ -> raise TypeError )
| TmPair (t1 , t2) -> ( typeOf ctx t1 , typeOf ctx t2)
| TmVar (s) -> getType ctx s
| TmAbs (s,ty1,t) -> let ty2 = typeOf (addBind ctx s ty1) t
in TyFun(ty2,ty1)
| TmApp (t1,t2) -> ( match typeOf ctx t1 with
TyFun(ty1,ty2) -> (match (ty1 = ty2) with
true -> ty2
| false -> raise TypeError )
| _ -> raise TypeError )
;;
(a) Complete the definitions for the type declaration context and the functions
getType and addBind . (5 marks)
Copyright c
2014 University of Southampton Page 16 of 25

COMP2212W1
(b) Find all of the mistakes in the faulty implementation above and show how to
correct them. (10 marks)
Copyright c
2014 University of Southampton Page 17 of 25 TURN OVER

COMP2212W1
B 8 This question is concerned with the operational semantics of the following
simple programming language of boolean expressions with an error term:
t::=errjtruejfalsejiftthentelsetjandtt v ::=truejfalse
true+true false +false
t1+truet2+v
ift1thent2elset3+vt1+falset3+v
ift1thent2elset3+v
t1+false
andt1t2+falset2+false
andt1t2+falset1+truet2+true
andt1t2+true
(a) Show the derivation of the big step evaluation of the following term:
and (iftrue then(and true false )else(and false true ))true
(3 marks)
Copyright c
2014 University of Southampton Page 18 of 25

COMP2212W1
(b) Design a small-step semantics ( t!t0) for this language such that
t+vif and only if t!v
(7 marks)
Question B8 continues on the next page 
Copyright c
2014 University of Southampton Page 19 of 25 TURN OVER

COMP2212W1
(c) Consider a translation of terms ^tsuch that every occurrence of the subterm
“andt1t2” intis replaced with
if^t1then ^t2elsefalse:
Give a counter-example to the statement ^t+vif and only if t+v
(2 marks)
(d) Do you think that there can be any such translation ^tinto the sublanguage
without and for which the statement in (c) above holds? Explain your an-
swer. (3 marks)
Copyright c
2014 University of Southampton Page 20 of 25

COMP2212W1
Do not write in this space 
Copyright c
2014 University of Southampton Page 21 of 25 TURN OVER

COMP2212W1
B 9 Suppose that two threads share a volatile boolean variable free and that it
is initially set to true. Both threads need to access a critical region (which does
not use free) and use the following code fragment to enforce mutual exclusion:
while (!free);
free = false;
critical_region();
free = true;
(a) Does this enforce mutual exclusion? Justify your answer. (4 marks)
(b) What if free were declared to be an atomic variable where both the assign-
ments and reads are guaranteed to be atomic? (1 marks)
(c) An alternative implementation using a shared volatile integer variable turn
with initial value 0is given below. The two threads each have a local integer
Copyright c
2014 University of Southampton Page 22 of 25

COMP2212W1
variable mine initialised as 0and1respectively.
while (turn != mine);
critical_region();
turn = (1-mine);
Explain any possible problems with this alternative implementation. (8 marks)
(d) Modern optimising compilers sometimes reorder instructions. What could
go wrong for the code in (c)? (2 marks)
Copyright c
2014 University of Southampton Page 23 of 25 TURN OVER

COMP2212W1
B 10
(a) Consider the labelled transition system Xillustrated below:
x0
a
x1
b
}}{{{{{{{{c
!!CCCCCCCC
x2 x3
(2 marks)
List all the traces from x0.
(b) Consider additionally the labelled transition system Yillustrated below:
y0
a
~~||||||||a
BBBBBBBB
y1
b
y2
c
y3 y4
(3 marks)
Show thatx0simulatesy0, that is, that there is a simulation from YtoXthat
contains (y0;x0).
Copyright c
2014 University of Southampton Page 24 of 25

COMP2212W1
(c) Show that y0does not simulatex0. (3 marks)
(d) Consider the labelled transition system Zillustrated below:
z0 a
$$a
~~||||||||a
BBBBBBBB
z1
b
z2
c
z3
b
~~||||||||c
BBBBBBBB
z4 z5z6 z7
Show thatx0andz0are simulation equivalent. (5 marks)
(e) Show that x0andz0arenotbisimulation equivalent. (2 marks)
END OF PAPER