`split`

:
split: list alpha -> list alpha # list alpha;

What does split do?

split(k) <= (firstHalf k,secondHalf k);

This will work fine provided that we have functions
`firstHalf`

and functions `secondHalf`

with the following specification:

Specification: `firstHalf`

is a function which takes a list `k`

and returns a list consisting of the first `length(k) div 2`

elements of the list. For example `firstHalf [1,2,3,4,5]`

should give `[1,2]`

since the length is 5 and 5 div 2 is 2.

Now what about `secondHalf`

? `secondHalf`

is a function which takes a list `k`

and returns a list consisting of k after the first `length(k) div 2`

elements k have been thrown away.
So we have

firstHalf: list(alpha) -> list(alpha); firstHalf k <= keep( (length k) div 2 ,k); secondHalf: list(alpha) -> list(alpha); secondHalf k <= throwAway( (length k) div 2 ,k);So all that is left to do is specify and design

`keep`

and `throwAway`

.
The function `keep`

takes a number `n`

and a list `k`

and returns
a list consisting of the first `n`

elements of `k`

. That's easy:

keep: num # list(alpha) -> list(alpha); keep(0,k) <= []; keep (n+1,x::k) <= x::keep(n,k);

The function `throwAway`

takes a number `n`

and a list `k`

and returns
list `k`

with the first `n`

elements thrown away.

throwAway: num # list(alpha) -> list(alpha); throwAway(0,k) <= k; throwAway (n+1,x::k) <= throwAway(n,k);Our task is now complete. This gives is the complete Hope program:

throwAway: num # list(alpha) -> list(alpha); throwAway(0,k) <= k; throwAway (n+1,x::k) <= throwAway(n,k); keep: num # list(alpha) -> list(alpha); keep(0,k) <= []; keep (n+1,x::k) <= x::keep(n,k); length: list(alpha) -> num; length [] <= 0; length (x::k) <= 1 + length k; firstHalf: list(alpha) -> list(alpha); firstHalf k <= keep( (length k) div 2 ,k); secondHalf: list(alpha) -> list(alpha); secondHalf k <= throwAway( (length k) div 2 ,k); split: list alpha -> list alpha # list alpha; split(k) <= (firstHalf k,secondHalf k);s.danicic@gold.ac.uk

Sebastian Danicic BSc MSc PhD (Reader in Computer Science)

Dept of Computing, Goldsmiths, University of London, London SE14 6NW

Last updated 2010-12-29