Coding Problem Solution By Proof

This is a completely non-extreme approach to the CodingProblem -- programming by proof. Here's the step-by-step explanation of how it went.

The basic preconditions and postconditions:

OrderedCollection>>partitionInto: aCount

"aCount > 0.
aCount isInteger"
...
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1].
result flattened = self"

OK, compute a few important values:

"aCount > 0. aCount isInteger"
binSize := self size // aCount.
extras := self size \\ aCount.
"aCount > 0. aCount isInteger. binSize * aCount + extras = self size. extras < aCount"
...
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1]. result flattened = self"

A logical consequence of the "flattened" condition is that the subcollections all have the same size as the original collection:

"aCount > 0. aCount isInteger"
binSize := self size // aCount.
extras := self size \\ aCount.
"aCount > 0. aCount isInteger. binSize * aCount + extras = self size. extras < aCount"
...
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1]. result flattened = self. self size = (result detectSum: [:each | each size])"

Combining the new postcondition with the results of introducing binSize and extras then gives us

"aCount > 0. aCount isInteger"
binSize := self size // aCount.
extras := self size \\ aCount.
"aCount > 0. aCount isInteger. binSize * aCount + extras = self size. extras < aCount"
...
"binSize * aCount + extras = (result detectSum: [:each | each size])"
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1]. result flattened = self. self size = (result detectSum: [:each | each size])"

Let's assume we can decompose result into two collections. The first collection has length = extras, and each element of the first collection has binSize+1 elements. Each element of the second collection has binSize elements. That means that the number of subelements of a and b together is

((binSize + 1) * extras + binSize * (aCount - extras)
= binSize * extras + extras + binSize * aCount - binSize * extras
= extras + binSize * aCount
= self size

"aCount > 0. aCount isInteger"
binSize := self size // aCount.
extras := self size \\ aCount.
"aCount > 0. aCount isInteger. binSize * aCount + extras = self size. extras < aCount"
...
"a do: [:each | each size = binSize + 1]. a size = extras. b size = aCount - extras. b do: [:each | each size = binSize]."
result := a , b.
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1]. result flattened = self. self size = (result detectSum: [:each | each size])"

Constructing "a" means looping through each of its elements' indexes. If we start "a" an as empty collection, we can use the invariant that each element of "a" up to the current index is of the desired size.

"aCount > 0. aCount isInteger"
binSize := self size // aCount.
extras := self size \\ aCount.
"aCount > 0. aCount isInteger. binSize * aCount + extras = self size. extras < aCount  [C1]"
a := (self species) new.
"C1. a do: [:each | false]. a size = 0"
(1) to: extras
do: [:each |
"C1. a do: [:each | each size = binSize + 1]. a size = each - 1"
...
"C1. a do: [:each | each size = binSize + 1]. a size = each"
].
"C1. a do: [:each | each size = binSize + 1]. a size = extras"
...
"a do: [:each | each size = binSize + 1]. a size = extras. b size = aCount - extras. b do: [:each | each size = binSize]."
result := a , b.
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1]. result flattened = self. self size = (result detectSum: [:each | each size])"

OK, so now we can actually do the "..." that sustains the loop precondition. I'll introduce a stream here to read from the OrderedCollection. That will give us our flattenedness condition.

"aCount > 0. aCount isInteger"
binSize := self size // aCount.
extras := self size \\ aCount.
"aCount > 0. aCount isInteger. binSize * aCount + extras = self size. extras < aCount  [C1]"
a := (self species) new.
stream := ReadStream on: self.
"C1. a do: [:each | false]. a size = 0"
(1) to: extras
do: [:each |
"C1. a do: [:each | each size = binSize + 1]. a size = each - 1"
a add: (stream next: binSize + 1)
"C1. a do: [:each | each size = binSize + 1]. a size = each"
].
"C1. a do: [:each | each size = binSize + 1]. a size = extras"
...
"a do: [:each | each size = binSize + 1]. a size = extras. b size = aCount - extras. b do: [:each | each size = binSize]."
result := a , b.
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1]. result flattened = self. self size = (result detectSum: [:each | each size])"

OK, now we can do the same trick for b:

"aCount > 0. aCount isInteger"
binSize := self size // aCount.
extras := self size \\ aCount.
"aCount > 0. aCount isInteger. binSize * aCount + extras = self size. extras < aCount  [C1]"
a := (self species) new.
stream := ReadStream on: self.
"C1. a do: [:each | false]. a size = 1. a size = 0"
(1) to: extras
do: [:each |
"C1. a do: [:each | each size = binSize + 1]. a size = each - 1"
a add: (stream next: binSize + 1)
"C1. a do: [:each | each size = binSize + 1]. a size = each"
].
"C1. a do: [:each | each size = binSize + 1]. a size = extras [C2]"
b := (self species) new.
"C1. C2. b do: [:each | false]. b size = 0"
extras + 1 to: aCount
do: [:each |
"C1. C2. b do: [:each | each size = binSize]. a size + b size = each - 1"
b add: (stream next: binSize)
"C1. C2. b do: [:each | each size = binSize]. a size + b size = each"
].
"C1. C2. b do: [:each | each size = binSize]. a size + b size = aCount"
"a do: [:each | each size = binSize + 1]. a size = extras. b size = aCount - extras. b do: [:each | each size = binSize]."
result := a , b.
"(result includes: a) and: (result includes: b) ifTrue: [(a size - b size) abs <= 1]. result flattened = self. self size = (result detectSum: [:each | each size])"

Voila! Without the comment junk, the code is:

binSize := self size // aCount.
extras := self size \\ aCount.
a := (self species) new.
stream := ReadStream on: self.
(1) to: extras
do: [:each |a add: (stream next: binSize + 1)].
b := (self species) new.
extras + 1 to: aCount
do: [:each | b add: (stream next: binSize)].
^a , b

and this could probably be simplified with a judious collect: or two to:

binSize := self size // aCount.
extras := self size \\ aCount.
stream := ReadStream on: self.
^ ((1 to: extras) collect: [:each | stream next: binSize + 1]),
((extras + 1 to: aCount) collect: [:each | stream next: binSize])

which obviously works, and is easy to read, despite the programming technique. (-:

Whoever wrote this page, I thank you. I have been working increasingly with lower-level (touching machine registers and implementing language runtimes, et. al.) programming, where unit testing becomes very difficult due to the inavailability of easy runtime polymorphism. I'm finding proof-based coding to be utterly invaluable in this particular domain of software development. I'm even finding that, with the limited practice I've acquired thus far, I can construct software by proof with ever-increasing speed; I'd say I'm within a factor of three of my TestDrivenDevelopment performance now.

Not only that, but the proof-annotation comments serve to help document the software in a manner more instructive than simple parroting. Consider how most folks write their assembly language software:

; Fill textInputBuffer with spaces ; The subsequent comments are pretty useless; even without the ; surrounding context, much of what the comments say is obvious by ; looking at the code (assuming even passing familiarity with 65816 ; assembly language coding experience).

LDA #$2020 ; Pattern for spaces LDX #textInputBufferSize-2 ; Use -2 bias because of BPL below. L1: STA textInputBuffer,X ; Write two bytes at once. DEX ; In 16-bit mode, so decrement twice. DEX BPL L1

versus:

     ; textInputBuffer undefined.

     LDA #$2020
     LDX #textInputBufferSize-2

 L1: ; INVARIANT: 0 <= X+1 < textInputBufferSize
     STA textInputBuffer,X
     DEX
     DEX                            ; -2 <= X+1
     BPL L1                         ; iff 0 <= X+1
     ; X+1 = -1

     ; \/c in textInputBuffer: c = $20

--Samuel A. Falvo II

My pleasure! I wrote this text many years ago (2003, maybe?), and came back to it recently because I was curious about the whole algorithm. -- BillTrost