COMP40006 REASONING ABOUT PROGRAMS 2020-2021

联系我们： 手动添加方式: 微信>添加朋友>企业微信联系人>13262280223 或者 QQ: 1483266981

TIMED REMOTE ASSESSMENTS 2020-2021

PAPER COMP40006

REASONING ABOUT PROGRAMS

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 de nitions 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 de ned 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 de ned 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 de nition 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) de ned 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 satis es the following speci cation: 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 speci cation 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’,’- ’] a i) Write the result of evaluating Occurs( [’w’,’a’,’a’,’t’,’ ’] , ’a’ ). ii) Write out the state of the whole array r returned from running the code split([’w’,’a’,’a’,’t’,’ ’], ’a’). [ Note: You may assume that new char[x][]; creates a new two-dimensional character array whose outer length is x, with all of its contents set to null. ] b Unfortunately, the author has not fully speci ed the split method. i) Give mid-conditions M1 and M2 that are strong enough to prove partial correctness of the code. (You do not need to prove anything.) ii) Give an invariant I for the loop that is appropriate to show total correctness. (You do not need to prove anything.) [ Hint: The invariant should have four conjuncts: the rst should bound and relate the values of start and pos; the second should describe the contents of the array in; the third should de ne the value of found; and the last should relate the contents of the two-dimensional array out with the array in. ] iii) Give a variant V for the loop that is appropriate to show termination. (You do not need to prove anything.) c Prove that the body of the loop in the split method re-establishes your invariant from part b.ii) in an iteration where in[pos] = c. State clearly what is given and what you need to show. d On line 8, the split method creates a two-dimensional character array out whose outer length is one element more than the length of the input array in. Could we save space by creating the two-dimensional character array out with a smaller outer length, without compromising the correctness of the method Justify your answer and provide a worst case example input to the split method that requires the most space in the two-dimensional character array out. The four parts carry, respectively, 10%, 35%, 45%, and 10% of the marks.