1      This question is about proof by induction.

a    The following code describes two Haskell functions, rev and revTR, which reverse lists; the latter is tail-recursive.

rev::   [a]  ->   [a]

rev   []  =   []

rev   (x:xs)  =    rev  xs  ++   [x]

revTR   ::   [a]  ->   [a]  ->   [a]

revTR   []  ys  =  ys

revTR   (x:xs)  ys  =  revTR  xs   (x:ys)

i)   Write out the result of

revTR   (1:3:5:[])   (2:4:[])

(You do not need to show any intermediate steps.)

ii)   Prove that

(*)    Axs :  [a]● Ays :  [a] ● Azs :  [a] ●

[  revTR (xs++ys) zs    =  revTR   ys ((rev  xs)++zs)  ] Write what is to be shown, what is taken arbitrary and justify each step.

You may want to use some of the following properties of lists, which hold for all u:a, all us:[a], all vs:[a], and all ws:[a].

(A)   us++(vs++ws) =  (us++vs)++ws

(B)    u:us =  [u]++us

(C)    us++[] =  us

(D)    []++us =  us

(E)    rev (us++vs) =  (rev vs)++(rev us)

iii)   Prove that

(**)   Axs:[a]●[  revTR   xs   []  =  rev   xs  ]

b    Consider the following three definitions of Haskell data types, where Exp

describes a simple language of expressions, TypeT is meant to represent integer and boolean types, and Val is meant to represent values.

data  Exp  =  Cond  Exp  Exp  Exp   |  BoolE  Bool   |  IntE  Int data  TypeT  =  IntT   |  BoolT

data  Val  =  IntV  Int   |  BoolV  Bool

The following three relations

EType C Exp x TypeT VType C Val x TypeT EVal C Exp x Val

describes the type of an expression,

describes the type of a value, and

describes the value of an expression.

are defined below:

(R1)   Ai:Int● EType(IntE  i/ IntT)

(R2)   Ab:Bool● EType(BoolE  b/ BoolT)

(R3)   Ae1/ e2/ e3 : Exp ● At : TypeT ●

[  EType(e1/ BoolT) A EType(e2/ t) A EType(e3/ t)      →  EType(Cond  e1  e2  e3/ t) ]

(R4)   Ai:Int● VType(IntV  i/ IntT)

(R5)   Ab:Bool● VType(BoolV  b/ BoolT)

(R6)   Ai:Int● EVal(IntE  i/ IntV  i)

(R7)   Ab:Bool● EVal(BoolE  b/ BoolV  b)

(R8)   Ae1/ e2/ e3 : Exp ● Av2/ v3 : Val

[  EVal(e1/ BoolV  true) A EVal(e2/ v2) A EVal(e3/ v3) →  EVal(Cond  e1  e2  e3/ v2) ]

(R9)   Ae1/ e2/ e3 : Exp ● Av2/ v3 : Val

[  EVal(e1/ BoolV  false) A EVal(e2/ v2) A EVal(e3/ v3) →  EVal(Cond  e1  e2  e3/ v3) ]

i)   Consider the expression e defined as:

e 全 Cond (BoolE  false) (IntE  3) ( Cond (BoolE  true) (IntE  4) (IntE  5) ) Give a value v e Val such that EVal(e/ v) holds.

(You do not need to show any intermediate steps or justify your answer.)

ii)   Write an expression e’ e Exp for which there exists no type t e TypeT for which EType(e/ t) holds.     (You do not need to justify your answer.)

iii)   Based on the definition of EType, write the inductive principle that would allow you to prove:

(***) Ae : Exp ● At : TypeT ●

[  EType(e/ t)  →  3v●[ EVal(e/ v) A VType(v/ t) ] ]

The two parts carry, respectively, 60% and 40% of the marks.

2      This is a question about loops and method calls.

Consider the Java method split(char[]  in,  char  c) defined as:

1     char[][]  split(  char[]  in,  char  c  )

2     //  PRE:  in  null                                                                                                                               (P)

3     //  POST:  3k:N. [ Occurs( in[..), c ) = k A in[..) ≈ Flatten( r[..), c, k ) : r[k] ] A in ≈ in[..)pre     (Q)

4     {

5          int  start  =  0;

6          int  pos  =  0;

7          int  found  =  0;

8         char[][]  out  =  new  char[in .length+1][]; 9

10          //  INV:  ???                                                                                                                                 (I)

11          //  VAR:  ???                                                                                                                                 (V)

12         while   (pos  <  in .length){

13              if   (  in[pos]  ==  c  ){

14                   out[found]  =  slice(in,  start,  pos);

15                   found++;

16                   start  =  pos  +  1; 17              }

18              pos++; 19         }

20

21          //  MID:  ???                                                                                                                                 (M1)

22         out[found]  =  slice(in,  start,  pos);

23          //  MID:  ???                                                                                                                                 (M2)

24         return  out;

25     }

This method splits up a provided string (treated as a character array) into an        array of substrings that were delimited by the provided character c in the original string. The method makes use of an auxiliary library method slice that creates a partial copy of a provided array. The implementation of the slice method is  not known, but it is claimed that it satisfies the following specification:

char[]  slice(char[]  str,  int  start,  int  finish)

//PRE:  str  null A 0 < start < finish < str .length

//POST:  r[..) ≈ str[start..finish) A  str[..) ≈ str[..)pre

{     ...    }

The specification of the split method relies on the following functions for array slices:

Occurs( a[..), v )   全   I{ k I a[k] = v }I

Flatten( a[..), v, k )   全   

where Flatten( a[..), v, k ) converts k elements of a two-dimensional array a into a one-dimensional array interleaved with the element v. For example:

Flatten([ [’a’,’b’],[’c’] ], ’- ’, 2) =  [’a’,’b’,’- ’,’c’,’- ’]