Program Analysis
Introduction
David Weir (U of Sussex) Program Analysis Term 1, 2017 1 / 606
Illustrative Problem
Use the Stable Match problem to illustate key concepts
What is a problem?
What is an algorithm?
What is a measure of progress?
How do we analyse an algorithm’s running time?
How do we prove that an algorithm is correct?
David Weir (U of Sussex) Program Analysis Term 1, 2017 2 / 606
Problem to Consider
Matching people up.
D
C
B
A
?
Z
Y
X
W
David Weir (U of Sussex) Program Analysis Term 1, 2017 3 / 606
Perfect Match
Everyone paired with exactly one person
D
C
B
A
Z
Y
X
W
David Weir (U of Sussex) Program Analysis Term 1, 2017 4 / 606
Preferences
blue people’s preferences
1st 2nd 3rd 4th
A X Z W Y
B X Y W Z
C W X Y Z
D Z X Y W
red people’s preferences
1st 2nd 3rd 4th
W A B D C
X C D B A
Y A D B C
Z D A B C
David Weir (U of Sussex) Program Analysis Term 1, 2017 5 / 606
Stability
D
C
B
A
Z
Y
X
W
Might some couple elope?
David Weir (U of Sussex) Program Analysis Term 1, 2017 6 / 606
Stability
Need to consider preferences of blue people and red people
A X Z W Y
B X Y W Z
C W X Y Z
D Z X Y W
W A B D C
X C D B A
Y A D B C
Z D A B C
David Weir (U of Sussex) Program Analysis Term 1, 2017 7 / 606
An Instability
Consider A and Z
A has been matched with Y
Z has been matched with C
A prefers Z to Y
Z prefers A to C
Both A and Z would prefer to be matched
Instability in the matching
A X Z W Y
B X Y W Z
C W X Y Z
D Z X Y W
W A B D C
X C D B A
Y A D B C
Z D A B C
D
C
B
A
Z
Y
X
W
David Weir (U of Sussex) Program Analysis Term 1, 2017 8 / 606
It Takes Two to Tango
Consider C and Y
C has been matched with Z
Y has been matched with A
C prefers Y to Z
but Y prefers A to C
Only C would prefer the match with Y
Not an instability in the matching
A X Z W Y
B X Y W Z
C W X Y Z
D Z X Y W
W A B D C
X C D B A
Y A D B C
Z D A B C
D
C
B
A
Z
Y
X
W
David Weir (U of Sussex) Program Analysis Term 1, 2017 9 / 606
Another Matching
D
C
B
A
Z
Y
X
W
Is it stable?
David Weir (U of Sussex) Program Analysis Term 1, 2017 10 / 606
Preferences
A X Z W Y
B X Y W Z
C W X Y Z
D Z X Y W
W A B D C
X C D B A
Y A D B C
Z D A B C
David Weir (U of Sussex) Program Analysis Term 1, 2017 11 / 606
Any Instabilities?
A pair where both prefer each other to the assigned match
What about C and X?
C would prefer W or X to Y
W does not like C!
X however would prefer C to her match B
This is an instability in the matching
A X Z W Y
B X Y W Z
C W X Y Z
D Z X Y W
W A B D C
X C D B A
Y A D B C
Z D A B C
D
C
B
A
Z
Y
X
W
David Weir (U of Sussex) Program Analysis Term 1, 2017 12 / 606
Definitions
A matching is perfect if everyone is paired with exactly one person
A perfect matching is stable if the are no instabilities
David Weir (U of Sussex) Program Analysis Term 1, 2017 13 / 606
Questions
Can a stable matching always be found?
How can we construct a stable match when one exists?
Stable Match Problem
Applies to other situations:
— matching hospitals and patients
— matching employers and applicants
David Weir (U of Sussex) Program Analysis Term 1, 2017 14 / 606
What a Problem is and isn’t
What a problem is:
Specification of a relationship between inputs and outputs
Usually a mapping — one valid output for a given input
What a problem isn’t:
Not a matter of doing something in a particular way!
Not procedural
The Stable Match Problem is a fairly generic problem
David Weir (U of Sussex) Program Analysis Term 1, 2017 15 / 606
What an Algorithm is and isn’t
What an algorithm is:
Specification as to how to tackle a problem
Can be abstract
We will use informal pseudo-code language
What an algorithm isn’t:
Not the same as a program
Programs implement algorithms
Same algorithm implemented in different languages
Solving a problem means getting valid output for each input given to
the algorithm
David Weir (U of Sussex) Program Analysis Term 1, 2017 16 / 606
Question for you
Write down a specification of the sorting problem.
David Weir (U of Sussex) Program Analysis Term 1, 2017 17 / 606
Question for you
Write down a specification of the sorting problem.
Input: A sequence of values A and an ordering relation r
Output: A permutation of A that is in sorted order
according to the relation r
David Weir (U of Sussex) Program Analysis Term 1, 2017 17 / 606
Question for you
Write down a specification of the problem that the binary search
algorithm solves
David Weir (U of Sussex) Program Analysis Term 1, 2017 18 / 606
Question for you
Write down a specification of the problem that the binary search
algorithm solves
Input: A sequence of values A that are ordered and a
search item a
Output: true if a is in A, and false otherwise.
David Weir (U of Sussex) Program Analysis Term 1, 2017 18 / 606
Question for you
Write down a specification of the Stable Match problem.
David Weir (U of Sussex) Program Analysis Term 1, 2017 19 / 606
Question for you
Write down a specification of the Stable Match problem.
Input: Two sets of entities, A and B, together with the
preferences for each element of A in the form of a
ranking of the elements of B, and the preferences of
each element of B in the form of a ranking of the
elements of A.
Output: A set of pairs S where the first element of the
pair is from A and the second element of the pair is from
B, such that S is a perfect match and S is stable.
David Weir (U of Sussex) Program Analysis Term 1, 2017 19 / 606
Algorithm
initialize each person to be free
while some blue person is free & has red people to propose to
choose one such blue person, α
let β be next best option α’s preference list
if β is free
assign α and β to be engaged
else if β prefers α to β’s fiancé α′
assign α and β to be engaged, and α′ to be free
else
β rejects α
Gale and Shapley, 1962
David Weir (U of Sussex) Program Analysis Term 1, 2017 20 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
Initially, everyone is free
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
Choose α = C
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
β = W
✔
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔
W is free so C and W become engaged
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔
Choose α = A
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔
β = X
✔
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔
X is free, so A and X become engaged to each other
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔
Choose α = B
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔
β = X
✔
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
X is already engaged to A, but prefers B
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
A and X break engagement and B and X become engaged
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
Choose α = A
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
β = Z
✔
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
Z is free, so A and Z become engaged to each other
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
α = D
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
β = Z
✔
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
Z is already engaged to A, but prefers D
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
A and Z break engagement and D and Z become engaged
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
α = A
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
β = W
✔
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
W is already engaged to C, but prefers A
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
C and W break engagement and A and W become engaged
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
α = C
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
β = X
✔
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
✔
X is already engaged to B, but prefers C
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
✔
B and X break engagement and C and X become engaged
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
✔
α = B
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
✔
β = Y
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
✔✔
Y is free, so B and Y become engaged to each other
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Illustration
DDD
CCC
BBB
AAA
ZZZ
YYY
XXX
WWW
A
X
Z
W
Y
B
X
Y
W
Z
C
W
X
Y
Z
D
Z
X
Y
W
W
A
B
D
C
X
C
D
B
A
Y
A
D
B
C
Z
D
A
B
C
✔✔ ✔
✔
✔
✔
✔✔
No one is now free, so a stable match has been established
David Weir (U of Sussex) Program Analysis Term 1, 2017 21 / 606
Example for you
Apply the algorithm to this problem instance.
A Y W Z X
B Z W Y X
C Z Y X W
D W Y X Z
W C D B A
X A B D C
Y C B D A
Z C B A D
Always choose blue person in order of rows in table
David Weir (U of Sussex) Program Analysis Term 1, 2017 22 / 606
Example for you
Apply the algorithm to this problem instance.
A Y W Z X
B Z W Y X
C Z Y X W
D W Y X Z
W C D B A
X A B D C
Y C B D A
Z C B A D
Always choose blue person in order of rows in table
C paired with Z
D paired with W
B paired with Y
A paired with X
David Weir (U of Sussex) Program Analysis Term 1, 2017 22 / 606
Algorithm
initialize each person to be free
while some blue person is free & has red people to propose to
choose one such blue person, α
let β be next best option α’s preference list
if β is free
assign α and β to be engaged
else if β prefers α to β’s fiancé α′
assign α and β to be engaged, and α′ to be free
else
β rejects α
Gale and Shapley, 1962
David Weir (U of Sussex) Program Analysis Term 1, 2017 23 / 606
Questions for you
Give a problem instance involving two blue people and two red
where there are two stable matches. Which one will the algorithm
find?
David Weir (U of Sussex) Program Analysis Term 1, 2017 24 / 606
Questions for you
Give a problem instance involving two blue people and two red
where there are two stable matches. Which one will the algorithm
find?
blueA redA redB
blueB redB redA
redA blueB blueA
redB blueA blueB
David Weir (U of Sussex) Program Analysis Term 1, 2017 24 / 606
Issues
Is the algorithm guaranteed to terminate?
How efficient is the algorithm?
Can we be certain that the algorithm always finds a stable match?
How fair is the algorithm?
Does it matter how we resolve the non-determinism?
David Weir (U of Sussex) Program Analysis Term 1, 2017 25 / 606
Termination
How many times could the while loop be executed?
Need some measure of progress
— a value that monotonically increases as number of executions
of loop increases
Consider: the number of blue people that are still free
Reject: this doesn’t necessarily decrease each time loop is
executed
Consider: the number of engaged couples
Reject: this doesn’t necessarily increase each time loop is
executed
David Weir (U of Sussex) Program Analysis Term 1, 2017 26 / 606
Measure of Progress
The number of proposals made so far
Always increases by 1 when loop executed
Upper limit on number of proposals is n2
— where n is number of blue people (and number of red people)
Gives upper limit on executions of while loop
The algorithm will therefore always terminate
David Weir (U of Sussex) Program Analysis Term 1, 2017 27 / 606
Efficiency
Running time will depend on how long it takes for each execution
of loop
Possible to do it in constant time
We will look at this shortly
Needs more detailed consideration of data structures
David Weir (U of Sussex) Program Analysis Term 1, 2017 28 / 606
Proving Correctness
A stable match is always found
Let’s show that it would be a contradiction to assert that . . .
there is an unstable pair in a match produced by the algorithm
A proof by contradiction
David Weir (U of Sussex) Program Analysis Term 1, 2017 29 / 606
Continuing Proof of Correctness
Suppose we have the following:
an unstable pair α and β
α paired by the algorithm with β′ 6= β
β paired by the algorithm with α′ 6= α
Instability means:
α prefers β to β′
β refers α to α′
David Weir (U of Sussex) Program Analysis Term 1, 2017 30 / 606
Completing Proof of Correctness
Case 1: α didn’t propose to β at any point
α proposes in decreasing order of preference
α must have proposed to β′
So β′ must be preferred to β by α
Contradicts previous assumption
Case 2: β proposed to α but was rejected (immediately or at later
point)
β would only reject α in favour of a blue person she preferred
So α′ must be preferred to α by β
Contradicts previous assumption
David Weir (U of Sussex) Program Analysis Term 1, 2017 31 / 606