Functional Programming

+
Verification
Winter 2021/22

Helmut Seidl

TUM

1
0 General

Contents of this lecture

• Correctness of programs
• Functional programming with OCaml

2
1 Correctness of Programs

• Programmers make mistakes !?

• Programming errors can be expensive, e.g., when a rocket explodes
or a vital business system is down for hours ...
• Some systems must not have errors, e.g., control software of
planes, signaling equipment of trains, airbags of cars ...

Problem
How can it be guaranteed that a program behaves as it should behave?

3
Approaches

• Careful engineering during software development

• Systematic testing
==⇒ formal process model (Software Engineering)
• proof of correctness
==⇒ verification

Tool: assertions

4
Approaches

• Careful engineering during software development

• Systematic testing
==⇒ formal process model (Software Engineering)
• proof of correctness
==⇒ verification

Tool: assertions

5
Example
public class GCD {
public static void main (String[] args) {
int x, y, a, b;
a = read(); x = a;
b = read(); y = b;
while (x != y)
if (x > y) x = x - y;
else y = y - x;

assert(x == y);

write(x);
} // End of definition of main();
} // End of definition of class GCD;

6
Comments

• The static method assert() expects a Boolean argument.

• During normal program execution, every call assert(e); is
ignored !?
• If Java is launched with the option: –ea (enable assertions),
the calls of assert are evaluated:

⇒ If the argument expression yields true, program execution

continues.
⇒ If the argument expression yields false, the error
AssertionError is thrown.

7
Caveat
The run-time check should evaluate a property of the program state
when reaching a particular program point.

The check should by no means change the program state (significantly)

!!!
Otherwise, the behavior of the observed system differs from the
unobserved system ???

Hint
In order to check properties of complicated data-structures, it is
recommended to realize distinct inspector classes whose objects allow to
inspect the data-structure without interference !?

8
Caveat
The run-time check should evaluate a property of the program state
when reaching a particular program point.

The check should by no means change the program state (significantly)

!!!
Otherwise, the behavior of the observed system differs from the
unobserved system ???

Hint
In order to check properties of complicated data-structures, it is
recommended to realize distinct inspector classes whose objects allow to
inspect the data-structure without interference !

9
Problem

• In general, there are many program executions ...

• Validity of assertions can be checked by the Java run-time only for a
specific execution at a time.

==⇒

We require a general method in order to guarantee that a given assertion

is valid ...

10
1.1 Program Verification

Robert W Floyd, Stanford U. (1936 – 2001)

11
Simplification
For the moment, we consider MiniJava only:

• only a single static method, namely, main

• only int variables
• only if and while.

12
Simplification
For the moment, we consider MiniJava only:

• only a single static method, namely, main

• only int variables
• only if and while.

Idea
• We annotate each program point with an assertion !
• At every program point, we argue that the assertion is valid ...
logic

13
Simplification
For the moment, we consider MiniJava only:

• only a single static method, namely, main

• only int variables
• only if and while.

Idea
• We annotate each program point with a formula !
• At every program point, we prove that the assertion is valid
==⇒ logic

14
Background: Logic
Assertion: “All humans are mortal”,
“Socrates is a human”, “Socrates is mortal”

Deduction:

Tautology:

15
Background: Logic
Assertion: “All humans are mortal”,
“Socrates is a human”, “Socrates is mortal”

∀ x. human( x) ⇒ mortal( x)
human(Socrates), mortal(Socrates)

Deduction:

Tautology:

16
Background: Logic
Assertion: “All humans are mortal”,
“Socrates is a human”, “Socrates is mortal”

∀ x. human( x) ⇒ mortal( x)
human(Socrates), mortal(Socrates)

Deduction: If ∀ x. P( x) holds, then also P( a) for a specific a !

If A ⇒ B und A holds, then B must hold as well !

Tautology:

17
Background: Logic
Assertion: “All humans are mortal”,
“Socrates is a human”, “Socrates is mortal”

∀ x. human( x) ⇒ mortal( x)
human(Socrates), mortal(Socrates)

Deduction: If ∀ x. P( x) holds, then also P( a) for a specific a !

If A ⇒ B und A holds, then B must hold as well !

Tautology: A ∨ ¬A
∀ x ∈ Z. x < 0 ∨ x = 0 ∨ x > 0

18
Background: Logic (cont.)
Laws: ¬¬ A ≡ A double negation

A∧A ≡ A idempotence
A∨A ≡ A
¬( A ∨ B) ≡ ¬ A ∧ ¬ B De Morgan
¬( A ∧ B) ≡ ¬ A ∨ ¬ B
A ∧ ( B ∨ C ) ≡ ( A ∧ B) ∨ ( A ∧ C ) distributivity
A ∨ ( B ∧ C ) ≡ ( A ∨ B) ∧ ( A ∨ C )
A ∨ ( B ∧ A) ≡ A absorption
A ∧ ( B ∨ A) ≡ A

19
Our Example

20
 Start

x = a = read();
y = b = read();

no yes
x != y

no yes
write(x); x<y

x=x−y; y=y−x;
Stop

21
Discussion

• The program points correspond to the edges of the control-flow

diagram !
• We require one assertion per edge ...

Background
d | x holds iff x = d · z for some integer z.
For integers x, y, let gcd( x, y) = 0, if x = y = 0, and the greatest
number d which both divides x and y, otherwise.
Then the following laws hold:

22
gcd( x, 0) = | x|
gcd( x, x) = | x|
gcd( x, y) = gcd( x, y − x)
gcd( x, y) = gcd( x − y, y)

23
Idea for the Example

• Initially, nothing holds.

• After a=read(); x=a; a=x holds.
• Before entering and during the loop, we should have:

A ≡ gcd( a, b) = gcd( x, y)

• At program exit, we should have:

B ≡ A∧x = y

24
Idea for the Example

• Initially, nothing holds.

• After a=read(); x=a; a=x holds.
• Before entering and during the loop, we should have:

A ≡ gcd( a, b) = gcd( x, y)

• At program exit, we should have:

B ≡ A∧x = y

• These assertions should be locally consistent ...

25
Our Example
Start
true
x = a = read();
a=x
y = b = read();

A
no yes
x != y
B A
no yes
write(x); x<y
A A
B x=x−y; y=y−x;
Stop

26
Question
How can we prove that the assertions are locally consistent?

Sub-problem 1: Assignments

Consider, e.g., the assignment: x = y+z;

In order to have after the assignment: x > 0, // post-condition
we must have before the assignment: y + z > 0. // pre-condition

27
General Principle

• Every assignment transforms a post-condition B into a minimal

assumption that must be valid before the execution so that B
is valid after the execution.

28
General Principle

• Every assignment transforms a post-condition B into a minimal

assumption that must be valid before the execution so that B
is valid after the execution.
• In case of an assignment x = e; the weakest pre-condition is
given by
WP[[x = e;]] ( B) ≡ B[e/ x]
This means: we simply substitute everywhere in B, x by e !!!

29
General Principle

• Every assignment transforms a post-condition B into a minimal

assumption that must be valid before the execution so that B
is valid after the execution.
• In case of an assignment x = e; the weakest pre-condition is
given by
WP[[x = e;]] ( B) ≡ B[e/ x]
This means: we simply substitute everywhere in B, x by e !!!
• An arbitrary pre-condition A for a statement s is valid,
whenever
A ⇒ WP[[s]] ( B)
// A implies the weakest pre-condition for B.

30
Example
assignment: x = x-y;
post-condition: x>0
weakest pre-condition: x−y > 0
stronger pre-condition: x−y > 2
even stronger pre-condition: x−y = 3

31
... in the GCD Program (1):

assignment: x = x-y;
post-condition: A
weakest pre-condition:

A[ x − y/ x] ≡ gcd( a, b) = gcd( x − y, y)
≡ gcd( a, b) = gcd( x, y)
≡ A

32
... in the GCD Program (2):

assignment: y = y-x;
post-condition: A
weakest pre-condition:

A[ y − x/ y] ≡ gcd( a, b) = gcd( x, y − x)
≡ gcd( a, b) = gcd( x, y)
≡ A

33
Wrap-up

∀ x. B B B[e/x]
x = read(); write(e); x = e;

B B B

WP[[;]]( B) ≡ B
WP[[x = e;]]( B) ≡ B[e/ x]
WP[[x = read();]]( B) ≡ ∀ x. B
WP[[write(e);]]( B) ≡ B

34
Discussion

• For all actions, the wrap-up provides the corresponding weakest

pre-conditions for a post-condition B.
• An output statement does not change any variable. Therefore, the
weakest pre-condition is B itself.
• An input statement x=read(); modifies the variable x
unpredictably.
In order B to hold after the input, B must hold for every
possible x before the input.

35
Orientation
Start
true
x = a = read();
a=x
y = b = read();

A
no yes
x != y
B A
no yes
write(x); x<y
A A
B x=x−y; y=y−x;
Stop

36
For the statements: b = read(); y = b; we calculate:

WP[[y = b;]] ( A) ≡ A[b/ y]

≡ gcd( a, b) = gcd( x, b)

37
For the statements: b = read(); y = b; we calculate:

WP[[y = b;]] ( A) ≡ A[b/ y]

≡ gcd( a, b) = gcd( x, b)

WP[[b = read();]] ( gcd( a, b) = gcd( x, b))

≡ ∀ b. gcd( a, b) = gcd( x, b)
⇐ a=x

38
Orientation
Start
true
x = a = read();
a=x
y = b = read();

A
no yes
x != y
B A
no yes
write(x); x<y
A A
B x=x−y; y=y−x;
Stop

39
For the statements: a = read(); x = a; we calculate:

WP[[x = a;]] ( a = x) ≡ a=a

≡ true

WP[[a = read();]] (true) ≡ ∀ a. true

≡ true

40
Sub-problem 2: Conditionals

A
no yes
b
B0 B1

It should hold:

• A ∧ ¬b ⇒ B0 and
• A ∧ b ⇒ B1 .

41
This is the case, if A implies the weakest pre-condition of the
conditional branching:

WP[[b]] ( B0 , B1 ) ≡ ((¬b) ⇒ B0 ) ∧ (b ⇒ B1 )

Die schwächste Vorbedingung können wir umschreiben in:

42
This is the case, if A implies the weakest pre-condition of the
conditional branching:

WP[[b]] ( B0 , B1 ) ≡ ((¬b) ⇒ B0 ) ∧ (b ⇒ B1 )

The weakest pre-condition can be rewritten into:

WP[[b]] ( B0 , B1 ) ≡ (b ∨ B0 ) ∧ (¬b ∨ B1 )
≡ (¬b ∧ B0 ) ∨ (b ∧ B1 ) ∨ ( B0 ∧ B1 )
≡ (¬b ∧ B0 ) ∨ (b ∧ B1 )

43
Example

B0 ≡ x > y ∧ y > 0 B1 ≡ y > x ∧ x > 0

Assume that b is the condition y > x.

Then the weakest pre-condition is given by:

44
Example

B0 ≡ x > y ∧ y > 0 B1 ≡ y > x ∧ x > 0

Assume that b is the condition y > x.

Then the weakest pre-condition is given by:

( x ≥ y ∧ x > y ∧ y > 0) ∨ ( y > x ∧ y > x ∧ x > 0)

≡ ( x > y ∧ y > 0) ∨ ( y > x ∧ x > 0)
≡ x > 0 ∧ y > 0 ∧ x 6= y

45
... for the GCD Example

b ≡ y>x

¬b ∧ A ≡ x ≥ y ∧ gcd( a, b) = gcd( x, y)
b∧A ≡ y > x ∧ gcd( a, b) = gcd( x, y)

46
... for the GCD Example

b ≡ y>x

¬b ∧ A ≡ x ≥ y ∧ gcd( a, b) = gcd( x, y)
b∧A ≡ y > x ∧ gcd( a, b) = gcd( x, y)

==⇒ The weakest pre-condition is given by

gcd( a, b) = gcd( x, y)

... i.e., exactly A

47
Orientation
Start
true
x = a = read();
a=x
y = b = read();

A
no yes
x != y
B A
no yes
write(x); x<y
A A
B x=x−y; y=y−x;
Stop

48
The argument for the assertion before the loop is analogous:

b ≡ y 6= x

¬b ∧ B ≡ B
b∧A ≡ A ∧ x 6= y

==⇒ A ≡ ( A ∧ x = y) ∨ ( A ∧ x 6= y) is the weakest pre-

condition for the conditional branching.

49
Summary of the Approach

• Annotate each program point with an assertion.

• Program start should receive annotation true.
• Verify for each statement s between two assertions A and B,
that A implies the weakest pre-condition of s for B i.e.,

A ⇒ WP[[s]]( B)

• Verify for each conditional branching with condition b, whether the

assertion A before the condition implies the weakest pre-condition
for the post-conditions B0 and B1 of the branching, i.e.,

A ⇒ WP[[b]] ( B0 , B1 )

An annotation with the last two properties is called locally consistent.

50
1.2 Correctness

Questions

• Which program properties can be verified by means of locally

consistent annotations ?
• How can we be sure that our method does not prove wrong claims
??

51
Recap (1)
• In MiniJava, the program state σ consists of a variable
assignment, i.e., a mapping of program variables to integers (their
values), e.g.,

σ = { x 7→ 5, y 7→ −42}

52
Recap (1)
• In MiniJava, the program state σ consists of a variable
assignment, i.e., a mapping of program variables to integers (their
values), e.g.,

σ = { x 7→ 5, y 7→ −42}

• A state σ satisfies an assertion A , if

A[σ ( x)/ x] x∈ A

// every variable in A is substituted by its value in σ

is a tautology, i.e., equivalent to true.

We write: σ |= A.

53
Example
σ = { x 7→ 5, y 7→ 2}
A ≡ ( x > y)
A[5/ x, 2/ y] ≡ (5 > 2)
≡ true

54
Example
σ = { x 7→ 5, y 7→ 2}
A ≡ ( x > y)
A[5/ x, 2/ y] ≡ (5 > 2)
≡ true

σ = { x 7→ 5, y 7→ 12}
A ≡ ( x > y)
A[5/ x, 12/ y] ≡ (5 > 12)
≡ false

55
Trivial Properties
σ |= true for every σ
σ |= false for no σ

σ |= A1 and σ |= A2 is equivalent to
σ |= A1 ∧ A2

σ |= A1 or σ |= A2 is equivalent to
σ |= A1 ∨ A2

56
Recap (2)

• An execution trace π traverses a path in the control-flow graph.

• It starts in a program point u0 with an initial state σ0 and
leads to a program point um with a final state σm .
• Every step of the execution trace performs an action and (possibly)
changes program point and state.

57
Recap (2)

• An execution trace π traverses a path in the control-flow graph.

• It starts in a program point u0 with an initial state σ0 and
leads to a program point um with a final state σm .
• Every step of the execution trace performs an action and (possibly)
changes program point and state.
==⇒ The trace π can be represented as a sequence

(u0 , σ0 )s1 (u1 , σ1 ) . . . sm (um , σm )

where si are elements of the control-flow graph, i.e., basic

statements or (possibly negated) conditional expressions (guards) ...

58
Example
Start
0
x = a = read();
y = b = read();

no yes
5 x != y 2
no yes
write(x); 4 x<y 3
6 x=x−y; y=y−x;
Stop

59
Assume that we start in point 3 with { x 7→ 6, y 7→ 12}.

Then we obtain the following execution trace:

π = (3, { x 7→ 6, y 7→ 12}) y = y-x;

(1, { x 7→ 6, y 7→ 6}) ¬(x != y)
(5, { x 7→ 6, y 7→ 6}) write(x);
(6, { x 7→ 6, y 7→ 6})

60
Assume that we start in point 3 with { x 7→ 6, y 7→ 12}.

Then we obtain the following execution trace:

π = (3, { x 7→ 6, y 7→ 12}) y = y-x;

(1, { x 7→ 6, y 7→ 6}) ¬(x != y)
(5, { x 7→ 6, y 7→ 6}) write(x);
(6, { x 7→ 6, y 7→ 6})

Important operation: Update of of state

σ ⊕ { x 7→ d} = { z 7→ σ z | z 6≡ x} ∪ { x 7→ d}

61
Assume that we start in point 3 with { x 7→ 6, y 7→ 12}.

Then we obtain the following execution trace:

π = (3, { x 7→ 6, y 7→ 12}) y = y-x;

(1, { x 7→ 6, y 7→ 6}) ¬(x != y)
(5, { x 7→ 6, y 7→ 6}) write(x);
(6, { x 7→ 6, y 7→ 6})

Important operation: Update of of state

σ ⊕ { x 7→ d} = { z 7→ σ z | z 6≡ x} ∪ { x 7→ d}

{ x 7→ 6, y 7→ 12} ⊕ { y 7→ 6} = { x 7→ 6, y 7→ 6}

62
Theorem

Let p be a MiniJava program, let π be an execution trace

starting in program point u and leading to program point v.
Assumptions:
• The program points in p are annotated by assertions which
are locally consistent.
• The program point u is annotated with A.
• The program point v is annotated with B.

63
Theorem

Let p be a MiniJava program, let π be an execution trace

starting in program point u and leading to program point v.
Assumptions:
• The program points in p are annotated by assertions which
are locally consistent.
• The program point u is annotated with A.
• The program point v is annotated with B.
Conclusion:
If the initial state of π satisfies the assertion A, then the final
state satisfies the assertion B.

64
Remarks

• If the start point of the program is annotated with true, then

every execution trace reaching program point v satisfies the
assertion at v.
• In order to prove that an assertion A holds at a program point
v, we require a locally consistent annotation satisfying:

(1) The start point is annotated with true.

(2) The assertion at v implies A.

65
Remarks

• If the start point of the program is annotated with true, then

every execution trace reaching program point v satisfies the
assertion at v.
• In order to prove that an assertion A holds at a program point
v, we require a locally consistent annotation satisfying:

(1) The start point is annotated with true.

(2) The assertion at v implies A.

• So far, our method does not provide any guarantee that v is

ever reached !!!
• If a program point v can be annotated with the assertion
false, then v cannot be reached.

66
Proof

Let π = (u0 , σ0 )s1 (u1 , σ1 ) . . . sm (um , σm )

Assumption: σ0 |= A.
Proof obligation: σm |= B.

Idea
Induction on the length m of the execution trace.
Base m = 0:
The endpoint of the execution equals the startpoint.
==⇒
==⇒

67
Proof

Let π = (u0 , σ0 )s1 (u1 , σ1 ) . . . sm (um , σm )

Assumption: σ0 |= A.
Proof obligation: σm |= B.

Idea
Induction on the length m of the execution trace.
Base m = 0:
The endpoint of the execution equals the startpoint.
==⇒ σ0 = σm and A ≡ B
==⇒ the claim holds.

68
Important Notion: Evaluation of Expressions

Program State

σ = { x 7→ 5, y 7→ −1, z 7→ 21}

Arithmetic Expression

t ≡ 2∗z+y

Evaluation

[[t]] σ = [[2 ∗ z + y]] {x 7→ 5, y 7→ −1, z 7→ 21}

= 2 · 21 + (−1)
= 41

69
Proposition
For (arithmethic) expressions t, e,

[[t]] (σ ⊕ { x 7→ [[e]] σ }) = [[t[e/x]]] σ

70
Proposition
For (arithmethic) expressions t, e,

[[t]] (σ ⊕ { x 7→ [[e]] σ }) = [[t[e/x]]] σ

E.g.„ consider t ≡ x + y, e ≡ 2 ∗ z
for σ = { x 7→ 5, y 7→ −1, z 7→ 21}.

71
Proposition
For (arithmethic) expressions t, e,

[[t]] (σ ⊕ { x 7→ [[e]] σ }) = [[t[e/x]]] σ

E.g.„ consider t ≡ x + y, e ≡ 2 ∗ z
for σ = { x 7→ 5, y 7→ −1, z 7→ 21}.

[[t]] (σ ⊕ { x 7→ [[e]] σ }) = [[t]] (σ ⊕ { x 7→ 42})

= [[t]] ({ x 7→ 42, y 7→ −1, z 7→ 21})
= 42 + (−1) = 41

[[t[e/x]]] σ = [[(2 ∗ z) + y]] σ

= (2 · 21) − 1 = 41

72
Proposition

σ ⊕ { x 7→ [[e]] σ } |= t1 < t2 iff σ |= t1 [e/x] < t2 [e/x]

73
Proposition

σ ⊕ { x 7→ [[e]] σ } |= t1 < t2 iff σ |= t1 [e/x] < t2 [e/x]

Proof
σ ⊕ { x 7→ [[e]] σ } |= t1 < t2
iff [[t1 ]] (σ ⊕ { x 7→ [[e]] σ }) < [[t2 ]] (σ ⊕ { x 7→ [[e]] σ })
iff [[t1 [e/x]]] σ < [[t2 [e/x]]] σ
iff σ |= t1 [e/x] < t2 [e/x] ✷

74
Proposition
for every formula A,

σ ⊕ { x 7→ [[e]] σ } |= A iff σ |= A[e/x]

75
Proposition
for every formula A,

σ ⊕ { x 7→ [[e]] σ } |= A iff σ |= A[e/x]

Proof
Induction on the structure of formula A ✷

76
Induction Proof of Correctness (cont.)
Step m > 0:
Induction Hypothesis: The statement holds already for m − 1.
Let B′ denote the assertion at point um−1 .
==⇒ σm−1 |= B′

First, we deal with statements.

Case 1. sm ≡ ;

Then • σm−1 = σm
• WP[[;]] ( B) ≡ B
==⇒ B′ ⇒ B
==⇒ σm−1 = σm |= B ✷

77
Case 2. sm ≡ write(e);

Then • σm−1 = σm
• WP[[;write(e)]] ( B) ≡ B
==⇒ B′ ⇒ B
==⇒ σm−1 = σm |= B ✷

78
Case 2. sm ≡ write(e);

Then • σm−1 = σm
• WP[[;write(e)]] ( B) ≡ B
==⇒ B′ ⇒ B
==⇒ σm−1 = σm |= B ✷

Case 3. sm ≡ x = read();

Then • σm = σm−1 ⊕ { x 7→ c} for some c ∈ Z

• WP[[x = read();]] ( B) ≡ ∀ x. B
==⇒ B′ ⇒ ∀ x. B ⇒ B[c/ x]
==⇒ σm |= B ✷

79
Case 4. sm ≡ x = e; Then we have:

• σm = σm−1 ⊕ { x 7→ [[e]] σm−1 }

• B′ =⇒ WP[[x = e;]] ( B) ≡ B[e/ x]

==⇒ σm−1 |= B[e/ x]

==⇒ σm−1 |= B[e/ x] iff σm |= B
==⇒ σm |= B ✷

80
Case 4. sm ≡ x = e; Then we have:

• σm = σm−1 ⊕ { x 7→ [[e]] σm−1 }

• B′ =⇒ WP[[x = e;]] ( B) ≡ B[e/ x]

==⇒ σm−1 |= B[e/ x]

==⇒ σm−1 |= B[e/ x] iff σm |= B
==⇒ σm |= B ✷

81
Induction Proof of Correctness (cont.)
Step m > 0:
Inductive Hypothesis: The statement holds already for m − 1.
Let B′ denote the assertion at point um−1 .
==⇒ σm−1 |= B′

82
Induction Proof of Correctness (cont.)
Step m > 0:
Inductive Hypothesis: The statement holds already for m − 1.
Let B′ denote the assertion at point um−1 .
==⇒ σm−1 |= B′

Finally, consider tests sm ≡ b .

Then in particular, σm−1 = σm

83
Case 1. σm |= b

==⇒ B′ ⇒ WP[[b]] (C, B) where

WP[[b]] (C, B) ≡ (¬b ⇒ C ) ∧ (b ⇒ B)
==⇒ σm |= b ∧ (b ⇒ B)
==⇒ σm |= B ✷

84
Case 1. σm |= b

==⇒ B′ ⇒ WP[[b]] (C, B) where

WP[[b]] (C, B) ≡ (¬b ⇒ C ) ∧ (b ⇒ B)
==⇒ σm |= b ∧ (b ⇒ B)
==⇒ σm |= B ✷

Case 2. σm |= ¬b

==⇒ B′ ⇒ WP[[b]] ( B, C ) where

WP[[b]] ( B, C ) ≡ (¬b ⇒ B) ∧ (b ⇒ C )
==⇒ σm |= ¬b ∧ (¬b ⇒ B)
==⇒ σm |= B ✷

This completes the proof of the theorem.

85
Conclusion

• The method of Floyd allows us to prove that an assertion B

holds whenever (or under certain assumptions) a program point is
reached ...
• For the implementation, we require:

• the assertion true at the start point

• assertions for each further program point
• a proof that the assertions are locally consistent
==⇒ Logic, automated theorem proving

86
1.3 Optimization

Goal: Reduction of the number of required assertions

Observation

If the program has no loops, a weakest pre-condition can be calculated

for each program point !!!

87
Example

B3
x=x+2;
x = x+2; B2
z = z+x; z=z+x;
i = i+1; B1
i=i+1;
B

88
Example (cont.)

Assume B ≡ z = i2 ∧ x = 2i − 1
Then we calculate:

B1 ≡ WP[[i = i+1;]]( B) ≡ z = (i + 1 )2 ∧ x = 2 (i + 1 ) − 1
≡ z = (i + 1)2 ∧ x = 2i + 1

89
Example (cont.)

Assume B ≡ z = i2 ∧ x = 2i − 1
Then we calculate:

B1 ≡ WP[[i = i+1;]]( B) ≡ z = (i + 1 )2 ∧ x = 2 (i + 1 ) − 1
≡ z = (i + 1)2 ∧ x = 2i + 1
B2 ≡ WP[[z = z+x;]]( B1 ) ≡ z + x = (i + 1)2 ∧ x = 2i + 1
≡ z = i2 ∧ x = 2i + 1

90
Example (cont.)

Assume B ≡ z = i2 ∧ x = 2i − 1
Then we calculate:

B1 ≡ WP[[i = i+1;]]( B) ≡ z = (i + 1 )2 ∧ x = 2 (i + 1 ) − 1
≡ z = (i + 1)2 ∧ x = 2i + 1
B2 ≡ WP[[z = z+x;]]( B1 ) ≡ z + x = (i + 1)2 ∧ x = 2i + 1
≡ z = i2 ∧ x = 2i + 1
B3 ≡ WP[[x = x+2;]]( B2 ) ≡ z = i2 ∧ x + 2 = 2i + 1
≡ z = i2 ∧ x = 2i − 1
≡ B

91
Idea

• For every loop, select one program point.

Meaningful selections:

→ Before the condition

→ At the entry of the loop body
→ At the exit of the loop body ...

• Provide an assertion for each selected program point

==⇒ loop invariant
• For all other program points, the assertions are obtained by means
of WP[[...]]().

92
Example
int a, i, x, z;
a = read();
i = 0;
x = -1;
z = 0;
while (i != a) {
x = x+2;
z = z+x;
i = i+1;
}
assert(z==a*a);
write(z);

93
Example
Start

a = read();

i = 0;
x = −1;
z = 0;

B
no yes
i != a
z = a2 B
write(z); x=x+2;
z=z+x;

Stop i=i+1;

94
We verify:

WP[[i != a]]( z = a2 , B)
≡ (i = a ∧ z = a2 ) ∨ (i 6 = a ∧ B )
≡ (i = a ∧ z = a2 ) ∨ (i 6= a ∧ z = i2 ∧ x = 2i − 1)

⇐ (i = a ∧ z = i2 ∧ x = 2i − 1) ∨ (i 6= a ∧ z = i2 ∧ x = 2i − 1)
≡ z = i2 ∧ x = 2i − 1 ≡ B

95
Orientation
Start

a = read();

i = 0;
x = −1;
z = 0;

B
no yes
i != a
z = a2 B
write(z); x=x+2;
z=z+x;

Stop i=i+1;

96
We verify:

WP[[z = 0;]]( B) ≡ 0 = i2 ∧ x = 2i − 1
≡ i = 0 ∧ x = −1
WP[[x = -1;]](i = 0 ∧ x = −1) ≡ i=0
WP[[i = 0;]](i = 0) ≡ true
WP[[a = read();]](true) ≡ true

97
1.4 Termination

Problem

• By our approach, we can only prove that an assertion is valid at a

program point whenever that program point is reached !!!
• How can we guarantee that a program always terminates ?
• How can we determine a sufficient condition which guarantees
termination of the program ??

98
Examples

• The GCD program only terminates for inputs a, b with a = b or

a > 0 and b > 0.
• The square program terminates only for inputs a ≥ 0.
• while (true) ; never terminates.
• Programs without loops terminate always!

99
Examples

• The GCD program only terminates for inputs a, b with a = b or

a > 0 and b > 0.
• The square program terminates only for inputs a ≥ 0.
• while (true) ; never terminates.
• Programs without loops terminate always!

Can this example be generalized ??

100
Example int i, j, t;
t = 0;
i = read();
while (i>0) {
j = read();
while (j>0) { t = t+1; j = j-1; }
i = i-1;
}
write(t);

• The read number i (if non-negative) indicates how often j is read.

• The total running time (essentially) equals the sum of all
non-negative values read into j

101
Example int i, j, t;
t = 0;
i = read();
while (i>0) {
j = read();
while (j>0) { t = t+1; j = j-1; }
i = i-1;
}
write(t);

• The read number i (if non-negative) indicates how often j is read.

• The total running time (essentially) equals the sum of all
non-negative values read into j
==⇒ the program always terminates !!!

102
Programs with for-loops only of the form:
for (i=n; i>0; i--) {...}
// i is not modified in the body
... always terminate !

103
Programs with for-loops only of the form:
for (i=n; i>0; i--) {...}
// i is not modified in the body
... always terminate !

Question

How can we turn this observation into a method that is applicable to

arbitrary loops ?

104
Idea

• Make sure that each loop is executed only finitely often ...
• For each loop, identify an indicator value r, that has two
properties

(1) r > 0 whenever the loop is entered;

(2) r is decreased during every iteration of the loop.

• Transform the program in a way that, alongside ordinary program

execution, the indicator value r is computed.
• Verify that properties (1) and (2) hold!

105
Example: Safe GCD Program

int a, b, x, y;
a = read(); b = read();
if (a < 0) x = -a; else x = a;
if (b < 0) y = -b; else y = b;
if (x == 0) write(y);
else if (y == 0) write(x);
else {
while (x != y)
if (y > x) y = y-x;
else x = x-y;
write(x);
}

106
We choose: r = x+y

Transformation
int a, b, x, y, r;
a = read(); b = read();
if (a < 0) x = -a; else x = a;
if (b < 0) y = -b; else y = b;
if (x == 0) write(y);
else if (y == 0) write(x);
else { r = x+y;
while (x != y) {
if (y > x) y = y-x;
else x = x-y;
r = x+y; }
write(x);
}
107
 Start no yes
x == 0
no yes
a = read(); y == 0 write(y);

write(x);
b = read();
r=x+y;
no yes
a<0
no yes
x = a; x = −a; 3 x != y 1 r>0

no yes
x<y
write(x);
no yes
b<0 x=x−y; y=y−x;

2
y = b; y = −b; r > x+y
r=x+y;
Stop

108
At program points 1, 2 and 3, we assert:

(1) A ≡ x 6= y ∧ x > 0 ∧ y > 0 ∧ r = x + y

(2) B ≡ x > 0∧y > 0∧r > x+y
(3) true

Then we have:

A⇒r>0 und B ⇒ r > x+y

109
We verify:

WP[[x != y]](true, A) ≡ x=y ∨ A

⇐ x > 0∧y > 0∧r = x+y
≡ C

110
We verify:

WP[[x != y]](true, A) ≡ x=y ∨ A

⇐ x > 0∧y > 0∧r = x+y
≡ C
WP[[r = x+y;]](C ) ≡ x > 0∧y > 0
⇐ B

111
We verify:

WP[[x != y]](true, A) ≡ x=y ∨ A

⇐ x > 0∧y > 0∧r = x+y
≡ C
WP[[r = x+y;]](C ) ≡ x > 0∧y > 0
⇐ B
WP[[x = x-y;]]( B) ≡ x > y∧y > 0∧r > x
WP[[y = y-x;]]( B) ≡ x > 0∧y > x∧r > y

112
We verify:

WP[[x != y]](true, A) ≡ x=y ∨ A

⇐ x > 0∧y > 0∧r = x+y
≡ C
WP[[r = x+y;]](C ) ≡ x > 0∧y > 0
⇐ B
WP[[x = x-y;]]( B) ≡ x > y∧y > 0∧r > x
WP[[y = y-x;]]( B) ≡ x > 0∧y > x∧r > y
WP[[y > x]](. . . , . . .) ≡ ( x > y ∧ y > 0 ∧ r > x) ∨
( x > 0 ∧ y > x ∧ r > y)
⇐ x 6= y ∧ x > 0 ∧ y > 0 ∧ r = x + y
≡ A

113
Orientation
Start no yes
x == 0
no yes
a = read(); y == 0 write(y);

write(x);
b = read();
r=x+y;
no yes
a<0
no yes
x = a; x = −a; 3 x != y 1 r>0

no yes
x<y
write(x);
no yes
b<0 x=x−y; y=y−x;

2
y = b; y = −b; r > x+y
r=x+y;
Stop

114
Further propagation of C through the control-flow graph completes
the locally consistent annotation with assertions.

115
Further propagation of C through the control-flow graph completes
the locally consistent annotation with assertions.

We conclude:

• At program points 1 and 2, the assertions r>0 and

r > x + y, respectively, hold.
• During every iteration, r decreases, but stays non-negative.
• Accordingly, the loop can only be iterated finitely often.
==⇒ the program terminates!

116
General Method

• For every occurring loop while (b) s we introduce a fresh

variable r.
• Then we transform the loop into:
r = e0;
while (b) {
assert(r>0);
s
assert(r > e1);
r = e1;
}
for suitable expressions e0, e1.

117
1.5 Modular Verification and Procedures

Tony Hoare, Microsoft Research, Cambridge

118
Idea

• Modularize the correctness proof in a way that sub-proofs for

replicated program fragments can be reused.
• Consider statements of the form:

{ A} p { B}

... this means:

If before the execution of program fragment p, assertion A

holds and program execution terminates, then
after execution of p assertion B holds.

119
Idea

• Modularize the correctness proof in a way that sub-proofs for

replicated program fragments can be reused.
• Consider statements of the form:

{ A} p { B}

... this means:

If before the execution of program fragment p, assertion A

holds and program execution terminates, then
after execution of p assertion B holds.

A : pre-condition
B : post-condition

120
Examples

{ x > y} z = x-y; { z > 0}

121
Examples

{ x > y} z = x-y; { z > 0}

{true} if (x<0) x=-x; { x ≥ 0}

122
Examples

{ x > y} z = x-y; { z > 0}

{true} if (x<0) x=-x; { x ≥ 0}

{ x > 7} while (x!=0) x=x-1; { x = 0}

123
Examples

{ x > y} z = x-y; { z > 0}

{true} if (x<0) x=-x; { x ≥ 0}

{ x > 7} while (x!=0) x=x-1; { x = 0}

{true} while (true); {false}

124
Modular verification can be used to prove the correctness of programs
using functions/methods.

Simplification
We only consider

• procedures, i.e., static methods without return values;

• global variables, i.e., all variables are static as well.
// will be generalized later

125
Example

int a, b, x, y; void mm() {

if (a>b) {
void main () { x = a;
a = read(); y = b;
b = read(); } else {
mm(); y = a;
write (x-y); x = b;
} }
}

126
Comment

• for simplicity, we have removed all qualifiers static.

• The procedure definitions are not recursive.
• The program reads two numbers.
• The procedure minmax stores the larger number in x, and the
smaller number in y.
• The difference of x and y is returned.
• Our goal is to prove:

{ a ≥ b} mm(); { a = x}

127
Approach

• For every procedure f(), we provide a triple

{ A} f(); { B}

• Relative to this global hypothesis H we verify for each

procedure definition void f() { ss } that

{ A} ss { B}

holds.
• Whereever a procedure call occurs in the program, we rely on the
triple from H ...

128
... in the Example

We verify:

mm() a≥b

no yes
a>b

x = b; x = a;
y = a; y = b;

Stop a=x

129
... in the Example

We verify:

mm() a≥b

no yes
a=b a>b true
x = b; x = a;
y = a; y = b;

Stop a=x

130
Discussion

• The approach also works in case the procedure has a return value:
that can be simulated by means of a global variable return which
receives the respective function results.
• It is not obvious, though, how pre- and post-conditions of procedure
calls can be chosen if a procedured is called in multiple places ...
• Even more complicated is the situation when a procedure is
recursive: the it has possibly unboundedly many distinct calls !?

131
Example

int x, m0, m1, t; void f() {

x = x-1;
void main () { if (x>1) f();
x = read(); t = m1;
m0 = 1; m1 = 1; m1 = m0+m1;
if (x > 1) f(); m0 = t;
write (m1); }
}

132
Comment

• The program reads a number.

• If the number is at most 1, the program returns 1 ...
• Otherwise, the program computes the Fibonacci function fib.
• After a call to f, the variables m0 and m1 have the values fib(i − 1)
and fib(i ), respectively ...

133
Problem

• In the logic, we must be able to distinguish between the ith and

the (i + 1)th call.
• This is easier, if we have logical auxiliaries l = l1 , . . . , ln at hand
to store (selected) values before the call ...

In the Example
{ A} f(); { B} where

A ≡ x = l ∧ x > 1 ∧ m0 = m1 = 1
B ≡ l > 1 ∧ m1 ≤ 2l ∧ m0 ≤ 2l −1

134
General Approach

• Again, we start with a global hypothesis H which provides a

description
{ A} f(); { B}
// both A and B may contain li
for each call of f();
• Given this global hypothesies H we verify for each procedure
definition void f() { ss } that

{ A} ss { B}

holds.

135
... in the Example
f() A

x = x−1;
x = l − 1 ∧ x > 0 ∧ m0 = m1 = 1
no yes
x>1
D
f();
C
t = m1;
m1=m1+m0;
m0 = t;

Stop B

136
• We start with an assertion for the end point:

B ≡ l > 1 ∧ m1 ≤ 2l ∧ m0 ≤ 2l −1

• The assertion C is obtained by means of WP[[. . .]] and

weakening ...

WP[[t=m1; m1=m1+m0; m0=t;]] ( B)

≡ l − 1 > 0 ∧ m1 + m0 ≤ 2l ∧ m1 ≤ 2l −1
⇐ l − 1 > 1 ∧ m1 ≤ 2l −1 ∧ m0 ≤ 2l −2
≡ C

137
Question
How can the global hypothesis be used to deal with a specific procedure
call ???

Idea
• The assertion { A} f(); { B} represents a value table for
f().
• This value table can be logically represented by the implication:

∀ l. ( A[h/ x] ⇒ B)

// h denotes a sequence of auxiliaries

The values of the variables x before the call are recorded in the
auxiliaries.

138
Examples

Funktion: void double () { x = 2*x;}

Spezifikation: { x = l } double(); { x = 2l }
Tabelle: ∀ l.(h = l ) ⇒ ( x = 2l )
≡ ( x = 2h)

For the Fibonacci function, we calculate:

∀ l. (h > 1 ∧ h = l ∧ h0 = h1 = 1) ⇒
l > 1 ∧ m1 ≤ 2l ∧ m0 ≤ 2l −1

≡ ( h > 1 ∧ h0 = h1 = 1 ) ⇒ m1 ≤ 2 h ∧ m0 ≤ 2 h−1

139
Another pair ( A1 , B1 ) of assertions forms a valid triple
{ A1 } f(); { B1 } , if we are able to prove that

∀ l. A[h/ x] ⇒ B A1 [ h/ x]
B1

140
Another pair ( A1 , B1 ) of assertions forms a valid triple
{ A1 } f(); { B1 } , if we are able to prove that

∀ l. A[h/ x] ⇒ B A1 [ h/ x]
B1

Example: double()

A ≡ x=l B ≡ x = 2l
A1 ≡ x≥3 B1 ≡ x≥6

141
Another pair ( A1 , B1 ) of assertions forms a valid triple
{ A1 } f(); { B1 } , if we are able to prove that

∀ l. A[h/ x] ⇒ B A1 [ h/ x]
B1

Example: double()

A ≡ x=l B ≡ x = 2l
A1 ≡ x≥3 B1 ≡ x≥6

We verify:
x = 2h h≥3
x≥6

142
Remarks

Valid pairs ( A1 , B1 ) are obtained, e.g.,

• by substituting logical variables:

{ x = l } double(); { x = 2l }
{ x = l − 1} double(); { x = 2(l − 1)}

143
Remarks

Valid pairs ( A1 , B1 ) are obtained, e.g.,

• by substituting logical variables:

{ x = l } double(); { x = 2l }
{ x = l − 1} double(); { x = 2(l − 1)}

• by adding a condition C to the logical variables:

{ x = l } double(); { x = 2l }
{ x = l ∧ l > 0} double(); { x = 2l ∧ l > 0}

144
Remarks (cont.)

Valid pairs ( A1 , B1 ) are also obtained,

• if the pre-condition is strengthened or the post-condition weakened:

{ x = l } double(); { x = 2l }
{ x > 0 ∧ x = l } double(); { x = 2l }

{ x = l } double(); { x = 2l }
{ x = l } double(); { x = 2l ∨ x = −1}

145
Application to Fibonacci
Our goal is to prove: { D } f(); {C }

A ≡ x > 1 ∧ l = x ∧ m0 = m1 = 1
A[(l − 1)/l ] ≡ x > 1 ∧ l − 1 = x ∧ m0 = m1 = 1
≡ D

146
Application to Fibonacci
Our goal is to prove: { D } f(); {C }

A ≡ x > 1 ∧ l = x ∧ m0 = m1 = 1
A[(l − 1)/l ] ≡ x > 1 ∧ l − 1 = x ∧ m0 = m1 = 1
≡ D

B ≡ l > 1 ∧ m1 ≤ 2l ∧ m0 ≤ 2l −1
B[(l − 1)/l ] ≡ l − 1 > 1 ∧ m1 ≤ 2l −1 ∧ m0 ≤ 2l −2
≡ C

147
Orientation
f() A

x = x−1;
x = l − 1 ∧ x > 0 ∧ m0 = m1 = 1
no yes
x>1
D
f();
C
t = m1;
m1=m1+m0;
m0 = t;

Stop B

148
For the conditional, we verify:

WP[[x>1]] ( B, D ) ≡ ( x ≤ 1 ∧ l > 1 ∧ m1 ≤ 2l ∧ m0 ≤ 2l −1 ) ∨
( x > 1 ∧ x = l − 1 ∧ m1 = m0 = 1)

⇐ x > 0 ∧ x = l − 1 ∧ m0 = m1 = 1

149
1.6 Procedures with Local Variables

• Procedures f() modify global variables.

• The values of local variables of the caller before and after the call
remain unchanged.

Example
{int y= 17; double(); write(y);}

Before and after the call of double() we have: y = 17.

150
• The values of local variables are automatically preserved, if the
global hypothesis has the following properties:

→ The pre- and post-conditions: { A}, { B} of procedures

only speak about global variables !
→ The h are only used for global variables !!

151
• The values of local variables are automatically preserved, if the
global hypothesis has the following properties:

→ The pre- and post-conditions: { A}, { B} of procedures

only speak about global variables !
→ The h are only used for global variables !!

• As a new specific instance of adaptation, we obtain:

{ A} f(); { B}
{ A ∧ C } f(); { B ∧ C }

if C only speaks about logical variables or local variables of the

caller.

152
Summary

• Every further language construct requires dedicated verification

techniques.
• How to deal with dynamic data-structures, objects, classes,
inheritance ?
• How to deal with concurrency, reactivity ??
• Do the presented methods allow to prove everything ==⇒
completeness ?
• In how far can verification be automated ?
• How much help must be provided by the programmer and/or the
verifier ?

153
Functional Programming

154
John McCarthy, Stanford
155
Robin Milner, Edinburgh

156
Xavier Leroy, INRIA, Paris

157
2 Basics

• Interpreter Environment
• Expressions
• Definitions of Values
• More Complex Datatypes
• Lists
• Definitions (cont.)
• User-defined Datatypes

158
2.1 The Interpreter Environment

The basic interpreter is called with ocaml.

seidl@linux:~> ocaml
OCaml version 4.13.1
...
#

Definitions of variables, functions, ... can now immediately be inserted.

Alternatively, they can be read from a file:

# #use "Hello.ml";;

159
2.2 Expressions
# 3+4;;
- : int = 7
# 3+
4;;
- : int = 7
#
→ At #, the interpreter is waiting for input.
→ The ;; causes evaluation of the given input.
→ The result is computed and returned together with its type.

Advantage: Individual functions can be tested without re-compilation !

160
Pre-defined Constants and Operators

Type Constants: examples Operators

int 0 3 -7 + - * / mod
float -3.0 7.0 +. -. *. /.
bool true false not || &&
string "hello" ^
char ’a’ ’b’

161
Type Comparison operators
int = <> < <= >= >
float = <> < <= >= >
bool = <> < <= >= >
string = <> < <= >= >
char = <> < <= >= >

162
 Type Comparison operators
int = <> < <= >= >
float = <> < <= >= >
bool = <> < <= >= >
string = <> < <= >= >
char = <> < <= >= >

# -3.0/.4.0;;
- : float = -0.75
# "So"^" "^"it"^" "^"goes";;
- : string = "So it goes"
# 1>2 || not (2.0<1.0);;
- : bool = true

163
2.3 Definitions of Values

By means of let, a variable can be assigned a value.

The variable retains this value for ever!

# let seven = 3+4;;

val seven : int = 7
# seven;;
- : int = 7

Caveat: Variable names are start with a small letter !!!

164
Another definition of seven does not assign a new value to seven, but
creates a new variable with the name seven.

# let seven = 42;;

val seven : int = 42
# seven;;
- : int = 42
# let seven = "seven";;
val seven : string = "seven"

The old variable is now hidden (but still there)!

Apparently, the new variable may even have a different type.

165
2.4 More Complex Datatypes

• Pairs
# (3,4);;
- : int * int = (3, 4)
# (1=2,"hello");;
- : bool * string = (false, "hello")

• Tuples
# (2,3,4,5);;
- : int * int * int * int = (2, 3, 4, 5)
# ("hello",true,3.14159);;
-: string * bool * float = ("hello", true, 3.14159)

166
Simultaneous Definition of Variables

# let (x,y) = (3,4.0);;

val x : int = 3
val y : float = 4.

# let (3,y) = (3,4.0);;

val y : float = 4.0

167
Simultaneous Definition of Variables

# let (x,y) = (3,4.0);;

val x : int = 3
val y : float = 4.

# let (3,y) = (3,4.0);;

val y : float = 4.0

The latter use, though, will beforehand trigger the warning

this pattern-matching is not exhaustive.

168
 Records: Example

# type person = {given:string; sur:string; age:int};;

type person = { given : string; sur : string; age : int; }
# let paul = { given="Paul"; sur="Meier"; age=24 };;
val paul : person = {given = "Paul"; sur = "Meier"; age = 24}
# let hans = { sur="kohl"; age=23; given="hans"};;
val hans : person = {given = "hans"; sur = "kohl"; age = 23}
# let hansi = {age=23; sur="kohl"; given="hans"}
val hansi : person = {given = "hans"; sur = "kohl"; age = 23}
# hans=hansi;;
- : bool = true

169
Remark

... Records are tuples with named components whose ordering,

therefore, is irrelevant.
... As a new type, a record must be introduced before its use by
means of a type declaration.
... Type names and record components start with a small letter.

170
Remark

... Records are tuples with named components whose ordering,

therefore, is irrelevant.
... As a new type, a record must be introduced before its use by
means of a type declaration.
... Type names and record components start with a small letter.

Access to Record Components

... via selection of components

# paul.given;;
- : string = "Paul"

171
... with pattern matching
# let {given=x;sur=y;age=z} = paul;;
val x : string = "Paul"
val y : string = "Meier"
val z : int = 24

... and if we are not interested in everything:

# let {given=x;_} = paul;;
val x : string = "Paul"

172
Case Distinction: match and if

match n
with 0 -> "null"
| 1 -> "one"
| _ -> "uncountable!"

match e
with true -> e1
| false -> e2

The second example can also be written as

if e then e1 else e2

173
Watch out for redundant and incomplete matches!

# let n = 7;;
val n : int = 7
# match n with 0 -> "zero";;
Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
1
Exception: Match_failure ("", 5, -13).
# match n
with 0 -> "zero"
| 0 -> "one"
| _ -> "uncountable!";;
Warning: this match case is unused.
- : string = "uncountable!"

174
2.5 Lists

Lists are constructed by means of [] and :: .

Short-cut: [42; 0; 16]

# let mt = [];;
val mt : ’a list = []
# let l1 = 1::mt;;
val l1 : int list = [1]
# let l = [1;2;3];;
val l : int list = [1; 2; 3]
# let l = 1::2::3::[];;
val l : int list = [1; 2; 3]

175
Caveat

All elements must have the same type:

# 1.0::1::[];;
This expression has type int but is here used with type float

176
Caveat

All elements must have the same type:

# 1.0::1::[];;
This expression has type int but is here used with type float

tau list describes lists with elements of type tau.

The type ’a is a type variable:
[] denotes an empty list for arbitrary element types.

177
Pattern Matching on Lists

# match l
with [] -> -1
| x::xs -> x;;
-: int = 1

178
2.6 Definition of Functions

# let double x = 2*x;;

val double : int -> int = <fun>
# (double 3, double (double 1));;
- : int * int = (6,4)

→ Behind the function name follow the parameters.

→ The function name is just a variable whose value is a function.

179
→ Alternatively, we may introduce a variable whose value is a
function.

# let double = fun x -> 2*x;;

val double : int -> int = <fun>

→ This function definition starts with fun, followed by the sequence

of formal parameters.
→ After -> follows the specification of the return value.
→ The variables from the left can be accessed on the right.

180
Caveat

Functions may additionally access the values of variables which have

been visible at their point of definition:

# let factor = 2;;

val factor : int = 2
# let double x = factor*x;;
val double : int -> int = <fun>
# let factor = 4;;
val factor : int = 4
# double 3;;
- : int = 6

181
Caveat

A function is a value:

# double;;
- : int -> int = <fun>

182
Recursive Functions

A function is recursive, if it calls itself (directly or indirectly).

# let rec fac n = if n<2 then 1 else n * fac (n-1);;

val fac : int -> int = <fun>
# let rec fib = fun x -> if x <= 1 then 1
else fib (x-1) + fib (x-2);;
val fib : int -> int = <fun>

For that purpose, Ocaml offers the keyword rec.

183
If functions call themselves indirectly via other other functions, they are
called mutually recursive.

# let rec even n = if n=0 then "even" else odd (n-1)

and odd n = if n=0 then "odd" else even (n-1);;
val even : int -> string = <fun>
val odd : int -> string = <fun>

We combine their definitions by means of the keyword and.

184
Definition by Case Distinction

# let rec len = fun l -> match l

with [] -> 0
| x::xs -> 1 + len xs;;
val len : ’a list -> int = <fun>
# len [1;2;3];;
- : int = 3

185
Definition by Case Distinction

# let rec len = fun l -> match l

with [] -> 0
| x::xs -> 1 + len xs;;
val len : ’a list -> int = <fun>
# len [1;2;3];;
- : int = 3

... can be shorter written as

# let rec len = function [] -> 0

| x::xs -> 1 + len xs;;
val len : ’a list -> int = <fun>
# len [1;2;3];;
- : int = 3

186
Case distinction for several arguments

# let rec app l y = match l

with [] -> y
| x::xs -> x :: app xs y;;
val app : ’a list -> ’a list -> ’a list = <fun>
# app [1;2] [3;4];;
- : int list = [1; 2; 3; 4]

187
Case distinction for several arguments

# let rec app l y = match l

with [] -> y
| x::xs -> x :: app xs y;;
val app : ’a list -> ’a list -> ’a list = <fun>
# app [1;2] [3;4];;
- : int list = [1; 2; 3; 4]

... can also be written as

# let rec app = function [] -> fun y -> y

| x::xs -> fun y -> x::app xs y;;
val app : ’a list -> ’a list -> ’a list = <fun>
# app [1;2] [3;4];;
- : int list = [1; 2; 3; 4]

188
Local Definitions

Definitions introduced by let may occur locally:

# let x = 5
in let sq = x*x
in sq+sq;;
- : int = 50
# let facit n = let rec
iter m yet = if m>n then yet
else iter (m+1) (m*yet)
in iter 2 1;;
val facit : int -> int = <fun>

189
2.7 User-defined Datatypes

Example: playing cards

How to specify color and value of a card?

First Idea: pairs of strings and numbers, e.g.,

("diamonds",10) ≡ diamonds ten

("clubs",11) ≡ clubs jack
("gras",14) ≡ gras ace

190
Disadvantages

• Testing of the color requires a comparison of strings

−→ inefficient!
• Representation of Jack as 11 is not intuitive
−→ incomprehensible program!
• Which card represents the pair ("culbs",9)?
(typos are not recognized by the compiler)

Better: Enumeration types of Ocaml.

191
Example: Playing cards

2. Idea: Enumeration Types

# type color = Diamonds | Hearts | Gras | Clubs;;

type color = Diamonds | Hearts | Gras | Clubs
# type value = Seven | Eight | Nine | Jack | Queen | King |
Ten | Ace;;
type value = Seven | Eight | Nine | Jack | Queen | King |
Ten | Ace
# Clubs;;
- : color = Clubs
# let gras_jack = (Gras,Jack);;
val gras_jack : color * value = (Gras,Jack)

192
Advantages
→ The representation is intuitive.
→ Typing errors are recognized:
# (Culbs,Nine);;
Unbound constructor Culbs
→ The internal representation is efficient.

Remark
→ By type, a new type is defined.
→ The alternatives are called constructors and are separated by |.
→ Every constructor starts with a capital letter and is uniquely
assigned to a type.

193
Enumeration Types (cont.)

Constructors can be compared:

# Clubs < Diamonds;;

- : bool = false;;
# Clubs > Diamonds;;
- : bool = true;;

Pattern Matching on constructors:

# let is_trump = function

| (Hearts,_) -> true
| (_,Jack) -> true
| (_,Queen) -> true
| (_,_) -> false

194
 val is_trump : color * value -> bool = <fun>

By that, e.g.,

# is_trump (Gras,Jack);;
- : bool = true
# is_trump (Clubs,Nine);;
- : bool = false

Another useful function:

195
 # let string_of_color = function
Diamonds -> "Diamonds"
| Hearts -> "Hearts"
| Gras -> "Gras"
| Clubs -> "Clubs";;
val string_of_color : color -> string = <fun>

Remark

The function string_of_color returns for a given color the

corresponding string in constant time (the compiler, hopefully, uses jump
tables).

196
Now, Ocaml can (almost) play cards:

# let takes c1 c2 = match (c1,c2) with

| ((f1,Queen),(f2,Queen)) -> f1 > f2
| ((_,Queen),_) -> true
| (_,(_,Queen)) -> false
| ((f1,Jack),(f2,Jack)) -> f1 > f2
| ((_,Jack),_) -> true
| (_,(_,Jack)) -> false
| ((Hearts,w1),(Hearts,w2)) -> w1 > w2
| ((Hearts,_),_) -> true
| (_,(Hearts,_)) -> false
| ((f1,w1),(f2,w2)) -> if f1=f2 then w1 > w2
else false;;

197
 ...
# let take card2 card1 =
if takes card2 card1 then card2 else card1;;

# let trick card1 card2 card3 card4 =

take card4 (take card3 (take card2 card1));;

# trick (Gras,Ace) (Gras,Nine) (Hearts,Ten) (Clubs,Jack);;

- : color * value = (Clubs,Jack)
# trick (Clubs,Eight) (Clubs,King) (Gras,Ten)
(Clubs,Nine);;
- : color * value = (Clubs,King)

198
Sum Types

Sum types generalize of enumeration types in that constructors now may

have arguments.

Example: Optional Values

type ’a option = None | Some of ’a

let is_some x = match x with
| Some _ -> true
| None -> false
...

199
...
let get x = match x with
| Some y -> y
let value x a = match x with
| Some y -> y
| None -> a
let map f x = match x with
| Some y -> Some (f y)
| None -> None
let join a = match a with
| Some a’ -> a’
| None -> None

200
 Option is a module, which collects useful functions and values for
option.
A constructor defined inside type t = Con of <type> | ...
has functionality Con : <type> -> t — must, however, always
occur applied ...

# Some;;
The constructor Some expects 1 argument(s),
but is here applied to 0 argument(s)
# None;;
- : ’a option = None
# Some 10;
- : int option = Some 10
# let a = Some "Hello!";;
val a : string option = Some "Hello!"

201
The type option is polymorphic – which means that it can be
constructed for any type ’a, in particular int or string.

Polymorphic types with parameters ’a, ’b, ’c are then introduced by

type (’a,’b,’c) t = ...

The option type is useful for defining partial functions

let rec get_value a l = match l with
| [] -> None
| (b,z)::rest -> if a=b then Some z
else get_value a rest

202
Datatypes can be recursive:

type sequence = End | Next of (int * sequence)

# Next (1, Next (2, End));;

- : sequence = Next (1, Next (2, End))

Note the similarity to lists!

203
Datatypes can be recursive:

type sequence = End | Next of (int * sequence)

# Next (1, Next (2, End));;

- : sequence = Next (1, Next (2, End))

Note the similarity to lists!

A corresponding polymorphic type could be

type ’a sequence = End | Next of (’a * ’a sequence)

# Next (1, Next (2, End));;

- : int sequence = Next (1, Next (2, End))

204
Recursive datatypes lead to recursive functions:

# let rec nth n s = match (n,s) with

| (_,End) -> None
| (0,Next (x,_)) -> Some x
| (n,Next (_, rest)) -> nth (n-1) rest;;
val nth : int -> int sequence -> int option = <fun>

# nth 4 (Next (1, Next (2, End)));;

- : int = None
# nth 2 (Next (1, Next(2, Next (5, Next (17, End)))));;
- : int = Some 5

205
Another Example

# let rec down = function

0 -> End
| n -> Next (n, down (n-1));;
val down : int -> int sequence = <fun>

# down 3;;
- : int sequence = Next (3, Next (2, Next (1, End)));;
# down (-1);;
Stack overflow during evaluation (looping recursion?).

206
3 A closer Look at Functions

• Tail Calls
• Higher-order Functions

→ Currying
→ Partial Application

• Polymorphic Functions
• Polymorphic Datatypes
• Anonymous Functions

207
3.1 Tail Calls

A tail call in the body e of a function is a call whose value provides the
value of e ...
let f x = x+5
let g y = let z = 7
in if y>5 then f (-y)
else z + f y
The first call is tail, the second is not.

==⇒ From a tail call, we need not return to the calling function.
==⇒ The stack space of the calling function can immediately be
recycled !!!

208
A recursive function f is called tail recursive, if all calls to f are last.

Examples
let rec fac1 = function
(1,acc) -> acc
| (n,acc) -> fac1 (n-1,n*acc);;

let rec loop x = if x<2 then x

else if x mod 2 = 0 then loop (x/2)
else loop (3*x+1);;

209
Discussion

• Tail-recursive functions can be executed as efficiently as loops in

imperative languages.
• The intermediate results are handed from one recursive call to the
next in accumulating parameters.
• From that, a stopping rule computes the result.
• Tail-recursive functions are particularly popular for list processing ...

210
Reversing a List – Version 1
let rec rev list = match list
with [] -> []
| x::xs -> app (rev xs) [x]

211
Reversing a List – Version 1
let rec rev list = match list
with [] -> []
| x::xs -> app (rev xs) [x]

rev [0;...;n-1] calls function app with

[]
[n-1]
[n-1; n-2]
...
[n-1; ...; 1]
as first argument ==⇒ quadratic running-time!

212
Reversing a List – Version 2
let rev list = let rec r a l =
match l
with [] -> a
| x::xs -> r (x::a) xs
in r [] list

213
Reversing a List – Version 2
let rev list = let rec r a l =
match l
with [] -> a
| x::xs -> r (x::a) xs
in r [] list

The local function r is tail-recursive !

==⇒
linear running-time !!

214
3.2 Higher Order Functions

Consider the two functions

let f (a,b) = a+b+1;;

let g a b = a+b+1;;

At first sight, f and g differ only in the syntax. But they also differ in
their types:

# f;;
- : int * int -> int = <fun>
# g;;
- : int -> int -> int = <fun>

215
• Function f has a single argument, namely, the pair (a,b). The
return value is given by a+b+1.
• Function g has the one argument a of type int. The result of
application to a is a function that, when applied to the other
argument b, returns the result a+b+1 :

# f (3,5);;
- : int = 9
# let g1 = g 3;;
val g1 : int -> int = <fun>
# g1 5;;
- : int = 9

216
Haskell B. Curry, 1900–1982

217
In honor of its inventor Haskell B. Curry, this principle is called Currying.

→ g is called a higher order function, because its result is again a

function.
→ The application of g to a single argument is called partial, because
the result takes another argument, before the body is evaluated.

The argument of a function can again be a function:

# let apply f a b = f (a,b);;

val apply : (’a * ’b -> ’c) -> ’a -> ’b -> ’c = <fun>
...

218
...
# let plus (x,y) = x+y;;
val plus : int * int -> int = <fun>
# apply plus;;
- : int -> int -> int = <fun>
# let plus2 = apply plus 2;;
val plus2 : int -> int = <fun>
# let plus3 = apply plus 3;;
val plus3 : int -> int = <fun>
# plus2 (plus3 4);;
- : int = 9

219
3.3 Some List Functions

let rec map f = function

[] -> []
| x::xs -> f x :: map f xs

let rec fold_left f a = function

[] -> a
| x::xs -> fold_left f (f a x) xs

let rec fold_right f = function

[] -> fun b -> b
| x::xs -> fun b -> f x (fold_right f xs b)

220
 let rec find_opt f = function
[] -> None
| x::xs -> if f x then Some x
else find_opt f xs
Remarks

→ These functions abstract from the behavior of the function f.

They specify the recursion according the list structure —
independently of the elements of the list.
→ Therefore, such functions are sometimes called recursion schemes
or (list) functionals.
→ List functionals are independent of the element type of the list.
That type must only be known to the function f.
→ Functions which operate on equally structured data of various
type, are called polymorphic.

221
3.4 Polymorphic Functions

The Ocaml system infers the following types for the given functionals:

map : (’a -> ’b) -> ’a list -> ’b list

fold_left : (’a -> ’b -> ’a) -> ’a -> ’b list -> ’a
fold_right : (’a -> ’b -> ’b) -> ’a list -> ’b -> ’b
find_opt : (’a -> bool) -> ’a list -> ’a option

→ ’a and ’b are type variables. They can be instantiated by any

type (but each occurrence with the same type).

222
→ By partial application, some of the type variables may be
instantiated:

# string_of_int;;
val : int -> string = <fun>
# map string_of_int;;
- : int list -> string list = <fun>

# fold_left (+);;
val it : int -> int list -> int = <fun>

223
→ If a functional is applied to a function that is itself polymorphic,
the result may again be polymorphic:

# let cons_r xs x = x::xs;;

val cons_r : ’a list -> ’a -> ’a list = <fun>
# let rev l = fold_left cons_r [] l;;
val rev : ’a list -> ’a list = <fun>
# rev [1;2;3];;
- : int list = [3; 2; 1]
# rev [true;false;false];;
- : bool list = [false; false; true]

224
Some of the Simplest Polymorphic Functions

let compose f g x = f (g x)
let twice f x = f (f x)
let rec iter f g x = if g x then x else iter f g (f x);;

val compose : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b = <fun>
val twice : (’a -> ’a) -> ’a -> ’a = <fun>
val iter : (’a -> ’a) -> (’a -> bool) -> ’a -> ’a = <fun>

# compose not not;;

- : bool -> bool = <fun>
# compose not not true;;
- : bool = true;;
# compose Char.chr plus2 65;;
- : char = ’C’
225
3.5 Polymorphic Datatypes

User-defined datatypes may be polymorphic as well:

type ’a tree = Leaf of ’a

| Node of (’a tree * ’a tree)

→ tree is called type constructor, because it allows to create a new

type from another type, namely its parameter ’a.
→ In the right-hand side, only those type variables may occur, which
have been listed on the left.
→ The application of constructors to data may instantiate type
variables:

226
 # Leaf 1;;
- : int tree = Leaf 1
# Node (Leaf (’a’,true), Leaf (’b’,false));;
- : (char * bool) tree = Node (Leaf (’a’, true),
Leaf (’b’, false))

Functions for polymorphic datatypes are, typically, again polymorphic ...

227
let rec size = function
| Leaf _ -> 1
| Node(t,t’) -> size t + size t’

let rec flatten = function

| Leaf x -> [x]
| Node(t,t’) -> flatten t @ flatten t’

let flatten1 t = let rec doit t xs = match t with

| Leaf x -> x :: xs
| Node(t,t’) -> let xs = doit t’ xs
in doit t xs
in doit t []
...

228
...
val size : ’a tree -> int = <fun>
val flatten : ’a tree -> ’a list = <fun>
val flatten1 : ’a tree -> ’a list = <fun>

# let t = Node(Node(Leaf 1,Leaf 5),Leaf 3);;

val t : int tree = Node (Node (Leaf 1, Leaf 5), Leaf 3)

# size t;;
- : int = 3
# flatten t;;
val : int list = [1;5;3]
# flatten1 t;;
val : int list = [1;5;3]

229
3.6 Application: Queues

Wanted

Datastructure ’a queue which supports the operations

enqueue : ’a -> ’a queue -> ’a queue

dequeue : ’a queue -> ’a option * ’a queue
is_empty : ’a queue -> bool
queue_of_list : ’a list -> ’a queue
list_of_queue : ’a queue -> ’a list

230
First Idea

• Represent the queue by a list:

type ’a queue = ’a list

The functions is_empty, queue_of_list, list_of_queue

then are trivial.

231
First Idea

• Represent the queue by a list:

type ’a queue = ’a list

The functions is_empty, queue_of_list, list_of_queue

then are trivial.
• Extraction means access to the topmost element:
let dequeue = function
[] -> (None, [])
| x::xs -> (Some x, xs)

232
First Idea

• Represent the queue by a list:

type ’a queue = ’a list

The functions is_empty, queue_of_list, list_of_queue

then are trivial.
• Extraction means access to the topmost element:
let dequeue = function
[] -> (None, [])
| x::xs -> (Some x, xs)
• Insertion means append:
let enqueue x xs = xs @ [x]

233
Discussion

• The operator @ concatenates two lists.

• The implementation is very simple.
• Extraction is cheap.
• Insertion, however, requires as many calls of @ as the queue has
elements.
• Can that be improved upon ??

234
Second Idea

• Represent the queue as two lists !!!

type ’a queue = Queue of ’a list * ’a list
let is_empty = function
Queue ([],[]) -> true
| _ -> false
let queue_of_list list = Queue (list,[])
let list_of_queue = function
Queue (first,[]) -> first
| Queue (first,last) ->
first @ List.rev last

• The second list represents the tail of the list and therefore in
reverse ordering ...

235
Second Idea (cont.)

• Insertion is in the second list:

let enqueue x (Queue (first,last)) =

Queue (first, x::last)

236
Second Idea (cont.)

• Insertion is in the second list:

let enqueue x (Queue (first,last)) =

Queue (first, x::last)

• Extracted are elements always from the first list:

Only if that is empty, the second list is consulted ...

let dequeue = function

Queue ([],last) -> (match List.rev last
with [] -> (None, Queue ([],[]))
| x::xs -> (Some x, Queue (xs,[])))
| Queue (x::xs,last) -> (Some x, Queue (xs,last))

237
Discussion

• Now, insertion is cheap!

• Extraction, however, can be as expensive as the number of
elements in the second list ...
• Averaged over the number of insertions, however, the extra costs
are only constant !!!

==⇒ amortized cost analysis

238
3.7 Anonymous Functions

As we have seen, functions are data. Data, e.g., [1;2;3] can be used
without naming them. This is also possible for functions:
# fun x y z -> x+y+z;;
- : int -> int -> int -> int = <fun>
• fun initiates an abstraction.
This notion originates in the λ-calculus.
• -> has the effect of = in function definitions.
• Recursive functions cannot be defined in this way, as the recurrent
occurrences in their bodies require names for reference.

239
Alonzo Church, 1903–1995

240
• Pattern matching can be used by applying match ... with
for the corresponding argument.
• In case of a single argument, function can be considered ...

# function None -> 0

| Some x -> x*x+1;;
- : int option -> int = <fun>

241
Anonymous functions are convenient if they are used just once in a
program. Often, they occur as arguments to functionals:

# map (fun x -> x*x) [1;2;3];;

- : int list = [1; 4; 9]

Often, they are also used for returning functions as result:

# let make_undefined () = fun x -> None;;

val make_undefined : unit -> ’a -> ’b option = <fun>
# let def_one (x,y) = fun x’ -> if x=x’ then Some y
else None;;
val def_one : ’a * ’b -> ’a -> ’b option = <fun>

242
4 A Larger Application:
Balanced Trees

Recap: Sorted Array

2 3 5 7 11 13 17

243
Properties

• Sorting algorithms allow to initialize with ≈ n · log(n) many

comparisons.
// n == size of the array
• Binary search allows to search for elements with ≈ log(n)
many comparisons.
• Arrays neither support insertion nor deletion of elements.

244
Wanted:

Datastructure ’a d which allows to maintain a dynamic sorted

sequence of elements, i.e., which supports the operations

insert : ’a -> ’a d -> ’a d

delete : ’a -> ’a d -> ’a d
extract_min : ’a d -> ’a option * ’a d
extract_max : ’a d -> ’a option * ’a d
extract : ’a * ’a -> ’a d -> ’a list * ’a d
list_of_d : ’a d -> ’a list
d_of_list : ’a list -> ’a d

245
First Idea

Use balanced trees ...

246
First Idea

Use balanced trees ...

3 13

2 5 11 17

247
Discussion

• Data are stored at internal nodes!

• A binary tree with n leaves has n − 1 internal nodes.
• In order to search for an element, we must compare with all
elements along a path ...
• The depth of a tree is the maximal number of internal nodes on a
path from the root to a leaf.
• A complete balanced binary tree with n = 2k leaves has depth
k = log(n).

248
Discussion

• Data are stored at internal nodes!

• A binary tree with n leaves has n − 1 internal nodes.
• In order to search for an element, we must compare with all
elements along a path ...
• The depth of a tree is the maximal number of internal nodes on a
path from the root to a leaf.
• A complete balanced binary tree with n = 2k leaves has depth
k = log(n).
• How do we insert further elements ??
• How do we delete elements ???

249
Second Idea

• Instead of balanced trees, we use almost balanced trees ...

• At each node, the depth of the left and right subtrees should be
almost equal !
• An AVL tree is a binary tree where the depths of left and right
subtrees at each internal node differs at most by 1 ...

250
An AVL Tree

251
An AVL Tree

252
Not an AVL Tree

253
G.M. Adelson-Velskij, 1922 E.M. Landis, Moskau, 1921-1997

254
We prove:

(1) Each AVL tree of depth k > 0 has at least

fib(k) ≥ Ak−1
√
5+1
nodes where A= 2 // golden cut

255
We calculate:
(1) Each AVL tree of depth k > 0 has at least

fib(k) ≥ Ak−1
√
5+1
nodes where A= 2 // golden cut
(2) Every AVL tree with n > 0 internal nodes has depth at most
1
· log(n) + 1
log( A)

256
We calculate:
(1) Each AVL tree of depth k > 0 has at least

fib(k) ≥ Ak−1
√
5+1
nodes where A= 2 // golden cut
(2) Every AVL tree with n > 0 internal nodes has depth at most
1
· log(n) + 1
log( A)

Proof: We only prove (1)

Let N (k) denote the minimal number of internal nodes of an AVL

tree of depth k .
Induction on the number k > 0 ...
257
k=1: N (1) = 1 = fib(1) = A0

k=2: N (2) = 2 = fib(2) ≥ A1

258
k=1: N (1) = 1 = fib(1) = A0

k=2: N (2) = 2 = fib(2) ≥ A1

k>2: Assume that the assertion holds for k−1 and k−2
...

==⇒ N (k) = N (k − 1) + N (k − 2) + 1
≥ fib(k − 1) + fib(k − 2)
= fib(k)

259
k=1: N (1) = 1 = fib(1) = A0

k=2: N (2) = 2 = fib(2) ≥ A1

k>2: Assume that the assertion holds for k−1 and k−2
...

==⇒ N (k) = N (k − 1) + N (k − 2) + 1
≥ fib(k − 1) + fib(k − 2)
= fib(k)
fib(k) = fib(k − 1) + fib(k − 2)
≥ Ak−2 + Ak−3
= Ak−3 · ( A + 1 )
= Ak−3 · A2
= Ak−1

260
Second Idea (cont.)

• If another element is inserted, the AVL property may get lost !

• If some element is deleted, the AVL property may get lost !
• Then the tree must be re-structured so that the AVL property is
re-established ...
• For that, we require for each node the depths of the left and right
subtrees, respectively ...

261
Representation

262
Representation

3 2

2 1 1

263
Third Idea

• Instead of the absolute depth, we store at each node only whether

the difference in depth of the two subtrees is negative, positive or
equal to zero !!!
• As datatype, we therefore define

type ’a avl = Null

| Neg of ’a avl * ’a * ’a avl
| Pos of ’a avl * ’a * ’a avl
| Eq of ’a avl * ’a * ’a avl

264
Representation

3 2

2 1 1

265
Representation

N P

P E E

266
Insertion

• If the tree is a leaf, i.e., empty, an internal node is created with two
new leaves.
• If the tree in non-empty, the new value is compared with the value
at the root.

→ If it is larger, it is inserted to the right.

→ Otherwise, it is inserted to the left.

• Caveat: Insertion may increase the depth and thus

Caveat: may destroy the AVL property !
• That must be subsequently dealt with ...

267
let rec insert x avl = match avl
with Null -> (Eq (Null,x,Null), true)
| Eq (left,y,right) -> if x < y then
let (left,inc) = insert x left
in if inc then (Neg (left,y,right), true)
else (Eq (left,y,right), false)
else let (right,inc) = insert x right
in if inc then (Pos (left,y,right), true)
else (Eq (left,y,right), false)
...

268
let rec insert x avl = match avl
with Null -> (Eq (Null,x,Null), true)
| Eq (left,y,right) -> if x < y then
let (left,inc) = insert x left
in if inc then (Neg (left,y,right), true)
else (Eq (left,y,right), false)
else let (right,inc) = insert x right
in if inc then (Pos (left,y,right), true)
else (Eq (left,y,right), false)
...

• Besides the new AVL tree, the function insert also returns
the information whether the depth of the result has increased.
• If the depth is not increased, the marking of the root need not be
changed.

269
| Neg (left,y,right) -> if x < y then
let (left,inc) = insert x left
in if inc then let (avl,_) = rotateRight (left,y,right)
in (avl,false)
else (Neg (left,y,right), false)
else let (right,inc) = insert x right
in if inc then (Eq (left,y,right), false)
else (Neg (left,y,right), false)
| Pos (left,y,right) -> if x < y then
let (left,inc) = insert x left
in if inc then (Eq (left,y,right), false)
else (Pos (left,y,right), false)
else let (right,inc) = insert x right
in if inc then let (avl,_) = rotateLeft (left,y,right)
in (avl,false)
else (Pos (left,y,right), false);;
270
Comments

• Insertion into the less deep subtree never increases the total depth.
The depths of the two subtrees, though, may become equal.
• Insertion into the deeper subtree may increase the difference in
depth to 2.
then the node at the root must be rotated in order to decrease the
difference ...

271
rotateRight

N P

E N

272
rotateRight

N E

N E

273
rotateRight

N E

P E E

274
rotateRight

N E

P E P

275
rotateRight

N E

P N E

276
let rotateRight (left, y, right) = match left
with Eq (l1,y1,r1) -> (Pos (l1, y1, Neg (r1,y,right)), false)
| Neg (l1,y1,r1) -> (Eq (l1, y1, Eq (r1,y,right)), true)
| Pos (l1, y1, Eq (l2,y2,r2)) ->
(Eq (Eq (l1,y1,l2), y2, Eq (r2,y,right)), true)
| Pos (l1, y1, Neg (l2,y2,r2)) ->
(Eq (Eq (l1,y1,l2), y2, Pos (r2,y,right)), true)
| Pos (l1, y1, Pos (l2,y2,r2)) ->
(Eq (Neg (l1,y1,l2), y2, Eq (r2,y,right)), true)

• The extra bit now indicates whether the depth of the tree after
rotation has decreased ...
• This is not the case only when the deeper subtree is of the form
Eq (...) — which does never occur here.

277
rotateLeft

P N

E P

278
rotateLeft

P E

P E

279
rotateLeft

P E

N E E

280
rotateLeft

P E

N E P

281
rotateLeft

P E

N N E

282
let rotateLeft (left, y, right) = match right
with Eq (l1,y1,r1) -> (Neg (Pos (left,y,l1), y1, r1), false)
| Pos (l1,y1,r1) -> (Eq (Eq (left,y,l1), y1, r1), true)
| Neg (Eq (l1,y1,r1), y2 ,r2) ->
(Eq (Eq (left,y,l1),y1, Eq (r1,y2,r2)), true)
| Neg (Neg (l1,y1,r1), y2 ,r2) ->
(Eq (Eq (left,y,l1),y1, Pos (r1,y2,r2)), true)
| Neg (Pos (l1,y1,r1), y2 ,r2) ->
(Eq (Neg (left,y,l1),y1, Eq (r1,y2,r2)), true)

• rotateLeft is analogous to rotateRight — only with the

roles of Pos and Neg exchanged.
• Again, the depth shrinks almost always.

283
Discussion

• Insertion requires at most as many calls of insert as the

depth of the tree.
• After returning from a call for a subtree, at most three nodes must
be re-arranged.
• The total effort therefore is bounded by a constand multiple to
log(n).
• In general, though, we are not interested in the extra bit at every
call. Therefore, we define:

let insert x tree = let (tree,_) = insert x tree

in tree

284
Extraction of the Minimum

• The minimum occurs at the leftmost internal node.

• It is found by recursively visiting the left subtree.
The leftmost node is found when the left subtree equals Null.
• Removal of a leaf may reduce the depth and thus may destroy the
AVL property.
• After each call, the tree must be locally repaired ...

285
let rec extract_min avl = match avl
with Null -> (None, Null, false)
| Eq (Null,y,right) -> (Some y, right, true)
| Eq (left,y,right) -> let (first,left,dec) = extract_min left
in if dec then (first, Pos (left,y,right), false)
else (first, Eq (left,y,right), false)
| Neg (left,y,right) -> let (first,left,dec) = extract_min left
in if dec then (first, Eq (left,y,right), true)
else (first, Neg (left,y,right), false)
| Pos (Null,y,right) -> (Some y, right, true)
| Pos (left,y,right) -> let (first,left,dec) = extract_min left
in if dec then let (avl,b) = rotateLeft (left,y,right)
in (first,avl,b)
else (first, Pos (left,y,right), false)

286
Discussion

• Rotation is only required when extracting from a tree of the form

Pos (...) and the depth of the left subtree is decreased.
• Altogether, the number of recursive calls is bounded by the depth.
For every call, at most three nodes are re-arranged.
• Therefore, the total effort is bounded by a constant multiple of
log(n).
• Functions for maximum or last element from an interval are
constructed analogously ...

287
5 Practical Features of Ocaml

• Exceptions
• Input and Output as Side-effects
• Sequences

288
5.1 Exceptions
In case of a runtime error, e.g., division by zero, the Ocaml system
generates an exception:

# 1 / 0;;
Exception: Division_by_zero.
# List.tl (List.tl [1]);;
Exception: Failure "tl".
# Char.chr 300;;
Exception: Invalid_argument "Char.chr".

Here, the exceptions Division_by_zero, Failure ¨tl¨ and

Invalid_argument ¨Char.chr¨ are generated.

289
Another reason for an exception is an incomplete match:

# match 1+1 with 0 -> "null";;

Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
1
Exception: Match_failure ("", 2, -9).

In this case, the exception Match_failure (¨¨, 2, -9) is

generated.

290
Pre-defined Constructors for Exceptions

Division_by_zero division by 0
Invalid_argument of string wrong usage
Failure of string general error
Match_failure of string * int * int incomplete match
Not_found not found
Out_of_memory memory exhausted
End_of_file end of file
Exit for the user ...

An exception is a first class citizen, i.e., a value from a datatype exn ...

291
 # Division_by_zero;;
- : exn = Division_by_zero
# Failure "complete nonsense!";;
- : exn = Failure "complete nonsense!"

Own exception are introduced by extending the datatype exn ...

# exception Hell;;
exception Hell
# Hell;;
- : exn = Hell

292
 # Division_by_zero;;
- : exn = Division_by_zero
# Failure "complete nonsense!";;
- : exn = Failure "complete nonsense!"

Own exception are introduced by extending the datatype exn ...

# exception Hell of string;;

exception Hell of string
# Hell "damn!";;
- : exn = Hell "damn!"

293
Handling of Exceptions

As in Java, exceptions can be raised and handled:

# let divide (n,m) = try Some (n / m)

with Division_by_zero -> None;;

# divide (10,3);;
- : int option = Some 3
# divide (10,0);;
- : int option = None

In this way, the member function can, e.g., be re-defined as

294
 let rec member x l = try if x = List.hd l then true
else member x (List.tl l)
with Failure _ -> false

# member 2 [1;2;3];;
- : bool = true
# member 4 [1;2;3];;
- : bool = false

Following the keyword with, the exception value can be inspected by

means of pattern matching for the exception datatype exn :

try <exp>
with <pat1> -> <exp1> | ... | <patN> -> <expN>

==⇒ several exceptions can be caught (and thus handled) at the

same time.
295
The programmer may trigger exceptions on his/her own
by means of the keyword raise ...

# 1 + (2/0);;
Exception: Division_by_zero.
# 1 + raise Division_by_zero;;
Exception: Division_by_zero.

An exception is an error value which can replace any expression.

Handling of an exception, results in the evaluation of another expression
(of the correct type) — or raises another exception.

296
 Exception handling may occur at any sub-expression, arbitrarily nested:

# let f (x,y) = x / (y-1);;

# let g (x,y) = try let n = try f (x,y)
with Division_by_zero ->
raise (Failure "Division by zero")
in string_of_int (n*n)
with Failure str -> "Error: "^str;;

# g (6,1);;
- : string = "Error: Division by zero"
# g (6,3);;
- : string = "9"

297
5.2 Textual Input and Output

• Reading from the input and writing to the output violates the
paradigm of purely functional programming !
• These operations are therefore realized by means of side-effects,
i.e., by means of functions whose return value is irrelevant (e.g.,
unit).
• During execution, though, the required operation is executed
==⇒ now, the ordering of the evaluation matters !!!

298
• Naturally, Ocaml allows to write to standard output:
# print_string "Hello World!\n";;
Hello World!
- : unit = ()
• Analogously, there is a function: read_line : unit -> string
...
# read_line ();;
Hello World!
- : string = "Hello World!"

299
In order to read from file, the file must be opened for reading ...

# let infile = open_in "test";;

val infile : in_channel = <abstr>
# input_line infile;;
- : string = "The file’s single line ...";;
# input_line infile;;
Exception: End_of_file

If there is no further line, the exception End_of_file is raised.

If a channel is no longer required, it should be explicitly closed ...

# close_in infile;;
- : unit = ()

300
Further Useful Values

stdin : in_channel
input_char : in_channel -> char
in_channel_length : in_channel -> int

• stdin is the standard input as channel.

• input_char returns the next character of the channel.
• in_channel_length returns the total length of the channel.

301
Output to files is analogous ...

# let outfile = open_out "test";;

val outfile : out_channel = <abstr>
# output_string outfile "Hello ";;
- : unit = ()
# output_string outfile "World!\n";;
- : unit = ()
...

The words written seperately, may only occur inside the file, once the file
has been closed ...

# close_out outfile;;
- : unit = ()

302
5.3 Sequences

In presence of side-effects, ordering matters!

Several actions can be sequenced by means of the sequence operator ;
:

# print_string "Hello";
print_string " ";
print_string "world!\n";;
Hello world!
- : unit = ()

303
Often, several strings must be output !
Given a list of strings, the list functional List.iter can be used:

# let rec iter f = function

[] -> ()
| x::[] -> f x
| x::xs -> f x; iter f xs;;

val iter : (’a -> unit) -> ’a list -> unit = <fun>

304
6 The Module System of OCAML

→ Modules
→ Signatures
→ Information Hiding
→ Functors
→ Separate Compilation

305
6.1 Modules

In order to organize larger software systems, Ocaml offers the concept of

modules:

module Pairs =
struct
type ’a pair = ’a * ’a
let pair (a,b) = (a,b)
let first (a,b) = a
let second (a,b) = b
end

306
On this input, the compiler answers with the type of the module, its
signature:

module Pairs :
sig
type ’a pair = ’a * ’a
val pair : ’a * ’b -> ’a * ’b
val first : ’a * ’b -> ’a
val second : ’a * ’b -> ’b
end

The definitions inside the module are not visible outside:

# first;;
Unbound value first

307
Access onto Components of a Module

Components of a module can be accessed via qualification:

# Pairs.first;;
- : ’a * ’b -> ’a = <fun>

Thus, several functions can be defined all with the same name:
# module Triples = struct
type ’a triple = Triple of ’a * ’a * ’a
let first (Triple (a,_,_)) = a
let second (Triple (_,b,_)) = b
let third (Triple (_,_,c)) = c
end;;
...

308
...
module Triples :
sig
type ’a triple = Triple of ’a * ’a * ’a
val first : ’a triple -> ’a
val second : ’a triple -> ’a
val third : ’a triple -> ’a
end
# Triples.first;;
- : ’a Triples.triple -> ’a = <fun>

309
... or several implementations of the same function:

# module Pairs2 =
struct
type ’a pair = bool -> ’a
let pair (a,b) = fun x -> if x then a else b
let first ab = ab true
let second ab = ab false
end;;

310
Opening Modules

In order to avoid explicit qualification, all definitions of a module can be

made directly accessible:

# open Pairs2;;
# pair;;
- : ’a * ’a -> bool -> ’a = <fun>
# pair (4,3) true;;
- : int = 4

the keyword include allows to include the definitions of another

module into the present module ...

311
# module A = struct let x = 1 end;;
module A : sig val x : int end
# module B = struct
open A
let y = 2
end;;
module B : sig val y : int end
# module C = struct
include A
include B
end;;
module C : sig val x : int val y : int end

312
Nested Modules

Modules may again contain modules:

module Quads = struct

module Pairs = struct
type ’a pair = ’a * ’a
let pair (a,b) = (a,b)
let first (a,_) = a
let second (_,b) = b
end
type ’a quad = ’a Pairs.pair Pairs.pair
let quad (a,b,c,d) =
Pairs.pair (Pairs.pair (a,b), Pairs.pair (c,d))
...

313
 ...
let first q = Pairs.first (Pairs.first q)
let second q = Pairs.second (Pairs.first q)
let third q = Pairs.first (Pairs.second q)
let fourth q = Pairs.second (Pairs.second q)
end

# Quads.quad (1,2,3,4);;
- : (int * int) * (int * int) = ((1,2),(3,4))
# Quads.Pairs.first;;
- : ’a * ’b -> ’a = <fun>

314
6.2 Module Types or Signatures

Signatures allow to restrict what a module may export.

Explicit indication of the signature allows

• to restrict the set of exported variables;
• to restrict the set of exported types ...

... an Example

315
module Sort = struct
let single list = map (fun x->[x]) list
let rec merge l1 l2 = match (l1,l2)
with ([],_) -> l2
| (_,[]) -> l1
| (x::xs,y::ys) -> if x<y then x :: merge xs l2
else y :: merge l1 ys
let rec merge_lists = function
[] -> [] | [l] -> [l]
| l1::l2::ll -> merge l1 l2 :: merge_lists ll
let sort list = let list = single list
in let rec doit = function
[] -> [] | [l] -> l
| l -> doit (merge_lists l)
in doit list
end

316
The implementation allows to access the auxiliary functions single,
merge and merge_lists from the outside:

# Sort.single [1;2;3];;
- : int list list = [[1]; [2]; [3]]

In order to hide the functions single and merge_lists, we introduce the

signature

module type Sort = sig

val merge : ’a list -> ’a list -> ’a list
val sort : ’a list -> ’a list
end

317
The functions single and merge_lists are no longer exported:

# module MySort : Sort = Sort;;

module MySort : Sort
# MySort.single;;
Unbound value MySort.single

318
Signatures and Types

The types mentioned in the signature must be Instances of the types for
the exported definitions.
In that way, these types are spezialized:
module type A1 = sig
val f : ’a -> ’b -> ’b
end
module type A2 = sig
val f : int -> char -> int
end
module A = struct
let f x y = x
end

319
# module A1 : A1 = A;;
Signature mismatch:
Modules do not match: sig val f : ’a -> ’b -> ’a end
is not included in A1
Values do not match:
val f : ’a -> ’b -> ’a
is not included in
val f : ’a -> ’b -> ’b
# module A2 : A2 = A;;
module A2 : A2
# A2.f;;
- : int -> char -> int = <fun>

320
6.3 Information Hiding

For reasons of modularity, we often would like to prohibit that the

structure of exported types of a module are visible from the outside.

Example
module ListQueue = struct
type ’a queue = ’a list
let empty_queue () = []
let is_empty = function
[] -> true | _ -> false
let enqueue xs y = xs @ [y]
let dequeue (x::xs) = (x,xs)
end

321
A signature allows to hide the implementation of a queue:

module type Queue = sig

type ’a queue
val empty_queue : unit -> ’a queue
val is_empty : ’a queue -> bool
val enqueue : ’a queue -> ’a -> ’a queue
val dequeue : ’a queue -> ’a * ’a queue
end

322
 # module Queue : Queue = ListQueue;;
module Queue : Queue
# open Queue;;
# is_empty [];;
This expression has type ’a list but is here used with type
’b queue = ’b Queue.queue

==⇒

The restriction via signature is sufficient to obfuscate the true nature of

the type queue.

323
If the datatype should be exported together with all constructors, its
definition is repeated in the signature:

module type Queue =

sig
type ’a queue = Queue of (’a list * ’a list)
val empty_queue : unit -> ’a queue
val is_empty : ’a queue -> bool
val enqueue : ’a -> ’a queue -> ’a queue
val dequeue : ’a queue -> ’a option * ’a queue
end

324
6.4 Functors

Since (almost) everything in Ocaml is higher order, it is no surprise that

there are modules of higher order: Functors.

• A functor receives a sequence of modules as parameters.

• The functor’s body is a module where the functor’s parameters can
be used.
• The result is a new module, which is defined relative to the
modules passed as parameters.

325
First, we specify the functor’s argument and result by means of
signatures:

module type Decons = sig

type ’a t
val decons : ’a t -> (’a * ’a t) option
end
module type GenFold = functor (X:Decons) -> sig
val fold_left : (’b -> ’a -> ’b) -> ’b -> ’a X.t -> ’b
val fold_right : (’a -> ’b -> ’b) -> ’a X.t -> ’b -> ’b
val size : ’a X.t -> int
val list_of : ’a X.t -> ’a list
val iter : (’a -> unit) -> ’a X.t -> unit
end
...

326
 ...
module Fold : GenFold = functor (X:Decons) ->
struct
let rec fold_left f b t = match X.decons t
with None -> b
| Some (x,t) -> fold_left f (f b x) t
let rec fold_right f t b = match X.decons t
with None -> b
| Some (x,t) -> f x (fold_right f t b)
let size t = fold_left (fun a x -> a+1) 0 t
let list_of t = fold_right (fun x xs -> x::xs) t []
let iter f t = fold_left (fun () x -> f x) () t
end;;

Now, we can apply the functor to the module to obtain a new module ...

327
module MyQueue = struct open Queue
type ’a t = ’a queue
let decons = function
Queue([],xs) -> (match rev xs
with [] -> None
| x::xs -> Some (x, Queue(xs,[])))
| Queue(x::xs,t) -> Some (x, Queue(xs,t))
end

module MyAVL = struct open AVL

type ’a t = ’a avl
let decons avl = match extract_min avl
with (None,avl) -> None
| Some (a,avl) -> Some (a,avl)
end

328
 module FoldAVL = Fold (MyAVL)
module FoldQueue = Fold (MyQueue)

By that, we may define

let sort list = FoldAVL.list_of (

AVL.from_list list)

Caveat

A module satisfies a signature whenever it implements it !

It is not required to explicitly declare that !!

329
6.5 Separate Compilation

• In reality, deployed Ocaml programs will not run within the

interactive shell.
• Instead, there is a compiler ocamlc ...
> ocamlc Test.ml
that interpretes the contents of the file Test.ml as a sequence
of definitions of a module Test.
• As a result, the compiler ocamlc generates the files

Test.cmo bytecode for the module

Test.cmi bytecode for the signature
a.out executable program

330
• If there is already a file Test.mli this is interpreted as the
signature for Test. Then we call
> ocamlc Test.mli Test.ml
• Given a module A and a module B, then these should be
compiled by
> ocamlc B.mli B.ml A.mli A.ml
• If a re-compilation of B should be omitted, ocamlc may
receive a pre-compiled file
> ocamlc B.cmo A.mli A.ml
• For practical management of required re-compilation after
modification of files, Linux offers the tool make. The script of
required actions then is stored in a Makefile.
• ... alternatively, dune can be used.

331
7 Formal Verification for Ocaml

Question
How can we make sure that an Ocaml program behaves as it should ???

We require:
• a formal semantics
• means to prove assertions about programs ...

332
7.1 MiniOcaml

In order to simplify life, we only consider a fragment of Ocaml.

We consider ...
• only base types int, bool as well as tuples and lists
• recursive function definitions only at top level

We rule out ...

• modifiable datatypes
• input and output
• local recursive functions

333
This fragment of Ocaml is called MiniOcaml.
Expressions in MiniOcaml can be described by the grammar

E :: = const | name | op1 E | E1 op2 E2 |

(E1 , . . . , Ek ) | let name = E1 in E0 |
match E with P1 -> E1 | ... | Pk -> Ek |
fun name -> E | E E1

P :: = const | name | (P1 , . . . , Pk ) | P1 :: P2

334
This fragment of Ocaml is called MiniOcaml.
Expressions in MiniOcaml can be described by the grammar

E :: = const | name | op1 E | E1 op2 E2 |

(E1 , . . . , Ek ) | let name = E1 in E0 |
match E with P1 -> E1 | ... | Pk -> Ek |
fun name -> E | E E1

P :: = const | name | (P1 , . . . , Pk ) | P1 :: P2

Short-cut
fun x1 -> ...fun xk -> e ≡ fun x1 . . . xk -> e

335
Caveat

• The set of admissible expressions must be further restricted to

those which are well typed, i.e., for which the Ocaml compiler
infers a type ...
(1, [true; false]) well typed
(1 [true; false]) not well typed
([1; true], false) not well typed
• We also rule out if ... then ... else ... , since it can be
simulated by match ... with true -> ... | false ->
....
• We could also have omitted let ... in ... (why?)

336
A program then consists of a sequence of mutally recursive global
definitions of variables f 1 , . . . , f m :

let rec f1 = E1
and f2 = E2
...
and fm = Em

337
7.2 A Semantics for MiniOcaml

Question
Which value is returned for the expression E ??

A value is an expression that cannot be further evaluated.

The set of all values can also be specified by means of a grammar:

V :: = const | fun name1 . . . namek -> E |

(V1 , . . . , Vk ) | [] | V1 :: V2

338
A MiniOcaml Program ...
let rec comp = fun f g x -> f (g x)
and map = fun f list -> match list
with [] -> []
| x::xs -> f x :: map f xs

339
A MiniOcaml Program ...
let rec comp = fun f g x -> f (g x)
and map = fun f list -> match list
with [] -> []
| x::xs -> f x :: map f xs

Examples of Values ...

1
(1, [true; false])
fun x -> 1 + 1
[fun x -> x+1; fun x -> x+2; fun x -> x+3]

340
Idea

• We define a relation e ⇒ v between expressions and their

values ==⇒ big-step operational semantics.
• The relation is defined by means of axioms and rules that follow
the structure of e.
• Apparently, v⇒v holds for every value v.

341
Tuples

e1 ⇒ v1 ... ek ⇒ vk
(TU)
(e1 , . . . , ek ) ⇒ (v1 , . . . , vk )

Lists
e1 ⇒ v1 e2 ⇒ v2
(LI)
e1 :: e2 ⇒ v1 :: v2

Global definitions
f =e e ⇒ v
(GD)
f ⇒ v

342
Local definitions

e1 ⇒ v1 e0 [v1 / x] ⇒ v0
(LD)
let x = e1 in e0 ⇒ v0

Function calls

e ⇒ fun x -> e0 e1 ⇒ v1 e0 [v1 / x] ⇒ v0

(APP)
e e1 ⇒ v0

343
By repeated application of the rule for function calls, a rule for functions
with multiple arguments can be derived:

e0 ⇒ fun x1 . . . xk -> e e1 ⇒ v1 . . . ek ⇒ vk e[v1 / x1 , . . . , vk / xk ] ⇒ v

(APP)
e0 e1 . . . ek ⇒ v

This derived rule makes proofs somewhat simpler.

344
Pattern Matching

e 0 ⇒ v ′ ≡ pi [ v 1 / x 1 , . . . , v k / x k ] ei [ v 1 / x 1 , . . . , v k / x k ] ⇒ v
(PM)
match e0 with p1 -> e1 | ... | pm -> em ⇒ v

— given that v′ does not match any of the patterns p 1 , . . . , pi −1

;-)

Built-in operators

e1 ⇒ v1 e2 ⇒ v2 v1 op v2 ⇒ v
(OP)
e1 op e2 ⇒ v

Unary operators are treated analogously.

345
The built-in equality operator
v=v ⇒ true

v1 = v2 ⇒ false

given that v, v1 , v2 are values that do not contain functions, and

v1 , v2 are syntactically different.

Example 1

17 ⇒ 17 4 ⇒ 4 17+4 ⇒ 21
17+4 ⇒ 21 21 ⇒ 21 21=21 ⇒ true
17 + 4 = 21 ⇒ true

346
The built-in equality operator
v=v ⇒ true

v1 = v2 ⇒ false

given that v, v1 , v2 are values that do not contain functions, and

v1 , v2 are syntactically different.

Example 1 — omitting axioms v⇒v

17+4 ⇒ 21
17+4 ⇒ 21 21=21 ⇒ true
17 + 4 = 21 ⇒ true

347
 Example 2

let rec f = fun x -> x+1

and s = fun y -> y*y

f = fun x -> x+1 16+1 ⇒ 17 s = fun y -> y*y 2*2 ⇒ 4

f ⇒ fun x -> x+1 16+1 ⇒ 17 s ⇒ fun y -> y*y 2*2 ⇒ 4
f 16 ⇒ 17 s 2 ⇒ 4 17+4 ⇒ 21
f 16 + s 2 ⇒ 21

// uses of v ⇒ v have mostly been omitted

348
Example 3

let rec app = fun x y -> match x

with [] -> y
| h::t -> h :: app t y

Claim: app (1::[]) (2::[]) ⇒ 1::2::[]

349
Proof

app = fun x y -> ... [] ⇒ [] 2::[] ⇒ 2::[]

app ⇒ fun x y -> ... match [] ... ⇒ 2::[]
app [] (2::[]) ⇒ 2::[]
app = fun x y -> ... 1 :: app [] (2::[]) ⇒ 1::2::[]
app ⇒ fun x y -> ... match 1::[] ... ⇒ 1::2::[]
app (1::[]) (2::[]) ⇒ 1::2::[]

// uses of v ⇒ v have mostly been omitted

350
Discussion

• The big-step operational semantics is not well suited for tracking

step-by-step how evaluation by MiniOcaml proceeds.
• It is quite convenient, though, for proving that the evaluation of a
function for particular argument values terminates:
For that, it suffices to prove that there are values to which the
corresponding function calls can be evaluated . . .

351
Example Claim
app l1 l2 terminates for all list values l1 , l2 .

Proof
Induction on the length n of the list l1 .

n=0 I.e., l1 = []. Then

app = fun x y -> · · ·

app ⇒ fun x y -> · · · match [] with [] -> l2 | ... ⇒ l2
app [] l2 ⇒ l2

352
n>0: I.e., l1 = h::t.

In particular, we assume that the claim already holds for all shorter lists.
Then we have:
app t l2 ⇒ l
for some l. We deduce
app t l2 ⇒ l
app = fun x y -> . . . h :: app t l2 ⇒ h :: l
app ⇒ fun x y -> . . . match h::t with · · · ⇒ h :: l
app (h::t) l2 ⇒ h :: l

353
Discussion (cont.)

• The big-step semantis also allows to verify that optimizing

transformations are correct, i.e., preserve the semantics.
• Finally, it can be used to prove the correctness of assertions about
functional programs !
• The big-step operational semantics suggests to consider expressions
as specifications of values.
• Expressions which evaluate to the same values, should be
interchangeable ...

354
Caveat

• In MiniOcaml, equality between values can only be tested if these

do not contain functions !!
• Such values are called comparable. They are of the form

C :: = const | (C1 , . . . , Ck ) | [] | C1 :: C2

355
Caveat

• In MiniOcaml, equalitiy between values can only be tested if these

do not contain functions !!
• Such values are called comparable. They are of the form

C :: = const | (C1 , . . . , Ck ) | [] | C1 :: C2

• Apparently, a value of MiniOcaml is comparable if and only iff its

type does not contain functions:

c :: = bool | int | unit | c1 ∗ . . . ∗ ck | c list

356
Discussion

• For program optimization, we sometimes may want to exchange

functions, e.g.,

comp (map f) (map g) = map (comp f g)

• Apparently, the functions to the right and left of the equality sign
cannot be compared by Ocaml for equality.

==⇒

Reasoning in logic requires an extended notion of equality!

357
Extension of Equality

The equality = of Ocaml is extended to expression which may not

terminate, and functions.

Non-termination
e1 , e2 both not terminating
e1 = e2

Termination
e1 ⇒ v1 e2 ⇒ v2 v1 = v2
e1 = e2

358
Structured values
v1 = v′1 . . . vk = v′k
(v1 , . . . , vk ) = (v′1 , . . . , v′k )

v1 = v′1 v2 = v′2
v1 :: v2 = v′1 :: v′2

Functions
e1 [v/ x1 ] = e2 [v/ x2 ] for all v
fun x1 -> e1 = fun x2 -> e2

==⇒ extensional equality

359
We have:
e ⇒ v
e = v

Assume that the type of e1 , e2 is functionfree. Then

e1 = e2 e1 terminates
e1 = e2 ⇒ true

e1 = e2 ⇒ true
e1 = e2 ei terminates

The crucial tool for our proofs is the ...

360
Substitution Lemma

e1 = e2
e[e1 / x] = e[e2 / x]

We deduce for functionfree expressions e:

e1 = e2 e[e1 / x] terminate
e[e1 / x] = e[e2 / x] ⇒ true

361
Discussion

• The lemma tells us that in every context, all occurrences of the

expression e1 can be replaced by the expression e2 — whenever e1
and e2 represent the same values.
• The lemma can be proven by induction on the depth of the
required derivations (which we omit).
• The exchange of expressions proven equal, allows us to design a
calculus for proving the equivalence of expressions ...

362
We provide us with a repertoir of rewrite rules for reducing the equality
of expressions to the equality of, possibly simpler expressions ...

Simplification of local definitions

e1 terminates
let x = e1 in e = e[e1 / x]

363
We provide us with a repertoir of rewrite rules for reducing the equality
of expressions to the equality of, possibly simpler expressions ...

Simplification of local definitions

e1 terminates
let x = e1 in e = e[e1 / x]

Simplification of function calls

e0 = fun x -> e e1 terminates

e0 e1 = e[e1 / x]

364
Proof of the let rule
Since e1 terminates, there is a value v1 with

e1 ⇒ v1

Due to the Substitution Lemma, we have:

e[v1 / x] = e[e1 / x]

Case 1: e[v1 / x] terminates.

Then a value v exists with

e[v1 / x] ⇒ v

365
Then
e[e1 / x] = e[v1 / x] = v
Because of the big-step semantics, however, we have:

let x = e1 in e ⇒ v and therefore,

let x = e1 in e = e[e1 / x]

Case 2: e[v1 / x] does not terminate.

Then e[e1 / x] does not terminate and neither does let x = e1 in e.

Accordingly,
let x = e1 in e = e[e1 / x]

366
By repeated application of the rule for function calls, an extra rule for
functions with multiple arguments can be deduced:

e0 = fun x1 . . . xk -> e e1 , . . . , ek terminate

e0 e1 . . . ek = e[e1 / x1 , . . . , ek / xk ]

This derived rule allows to shorten some proofs considerably.

367
Rule for pattern matching

e0 = []
match e0 with [] -> e1 | ... | pm -> em = e1

e0 terminates e0 = e′1 :: e′2

match e0 with [] -> e1 | x :: xs -> e2 = e2 [e′1 / x, e′2 / xs]

368
Rule for pattern matching

e0 = []
match e0 with [] -> e1 | ... | pm -> em = e1

e0 terminates e0 = e′1 :: e′2

match e0 with [] -> e1 | x :: xs -> e2 = e2 [e′1 / x, e′2 / xs]

We are now going to apply these rules ...

369
7.3 Proofs for MiniOcaml Programs

Example 1
let rec app = fun x -> fun y -> match x
with [] -> y
| h::t -> h :: app t y

We want to verify that

(1) app x [] = x for all lists x.
(2) app x (app y z) = app (app x y) z
for all lists x, y, z.

370
Idea: Induction on the length n of x

n=0 Then x = [] holds.

We deduce:

app x [] = app [] []
= match [] with [] -> [] | h::t -> h :: app t []
= []
= x

371
n>0 Then: x = h::t where t has length n − 1.

We deduce:

app x [] = app (h::t) []

= match h::t with [] -> [] | h::t -> h :: app t []
= h :: app t []
= h :: t by induction hypothesis
= x

372
Analogously we proceed for assertion (2) ...

n=0 Then: x = []

We deduce:

app x (app y z) = app [] (app y z)

= match [] with [] -> app y z | h::t -> ...
= app y z
= app (match [] with [] -> y | ...) z
= app (app [] y) z
= app (app x y) z

373
 n>0 Then x = h::t where t has length n − 1.

We deduce:

app x (app y z) = app (h::t) (app y z)

= match h::t with [] -> app y z
| h::t -> h :: app t (app y z)
= h :: app t (app y z)
= h :: app (app t y) z by induction hypothesis
= app (h :: app t y) z
= app (match h::t with [] -> []
| h::t -> h :: app t y) z
= app (app (h::t) y) z
= app (app x y) z
374
Discussion

• For the correctness of our induction proofs, we require that all

occurring function calls terminate.
• In the example, it suffices to prove that for all x, y, there exists
some v such that:

app x y ⇒ v

... which we have already proven, as usual, by induction.

375
Example 2

let rec rev = fun x -> match x

with [] -> []
| h::t -> app (rev t) [h]
let rec rev1 = fun x -> fun y -> match x
with [] -> y
| h::t -> rev1 t (h::y)

Claim

rev x = rev1 x [] for all lists x.

376
More generally,
app (rev x) y = rev1 x y for all lists x, y.

Proof: Induction on the length n of x

n=0 Then: x = []. We deduce:

app (rev x) y = app (rev []) y

= app (match [] with [] -> [] | ...) y
= app [] y
= y
= match [] with [] -> y | ...
= rev1 [] y
= rev1 x y

377
 n>0 Then x = h::t where t has length n − 1.

We deduce (ommitting simple intermediate steps):

app (rev x) y = app (rev (h::t)) y

= app (app (rev t) [h]) y
= app (rev t) (app [h] y) by example 1
= app (rev t) (h::y)
= rev1 t (h::y) by induction hypothesis
= rev1 (h::t) y
= rev1 x y

378
Discussion

• Again, we have implicitly assumed that all calls of app, rev and
rev1 terminate.
• Termination of these can be proven by induction on the length of
their first arguments.
• The claim:
rev x = rev1 x []
follows from:
app (rev x) y = rev1 x y

by setting: y = [] and assertion (1) from example 1.

379
Example 3
let rec sorted = fun x -> match x
with h1::h2::t -> (match h1 <= h2
with true -> sorted (h2::t)
| false -> false)
| _ -> true

and merge = fun x -> fun y -> match (x,y)

with ([],y) -> y
| (x,[]) -> x
| (x1::xs,y1::ys) -> (match x1 <= y1
with true -> x1 :: merge xs y
| false -> y1 :: merge x ys

380
Claim

sorted x ∧ sorted y → sorted (merge x y)

for all lists x, y.

Proof: Induction on the sum n of lengthes of x, y.

Assume that sorted x ∧ sorted y holds.

n=0 Then: x = [] = y

We deduce:
sorted (merge x y) = sorted (merge [] [])
= sorted []
= true

381
n>0

Case 1: x = [].

We deduce:
sorted (merge x y) = sorted (merge [] y)
= sorted y
= true

Case 2: y = [] analogous.

382
Case 3: x = x1::xs ∧ y = y1::ys ∧ x1 ≤ y1.

We deduce:
sorted (merge x y) = sorted (merge (x1::xs) (y1::ys))
= sorted (x1 :: merge xs y)
= ...

Case 3.1: xs = []

We deduce:
... = sorted (x1 :: merge [] y)
= sorted (x1 :: y)
= sorted y
= true

383
Case 3.2: xs = x2::xs’ ∧ x2 ≤ y1.

In particular: x1 ≤ x2 ∧ sorted xs.

We deduce:
... = sorted (x1 :: merge (x2::xs’) y)
= sorted (x1 :: x2 :: merge xs’ y)
= sorted (x2 :: merge xs’ y)
= sorted (merge xs y)
= true by induction hypothesis

384
Case 3.3: xs = x2::xs’ ∧ x2 > y1.

In particular: x1 ≤ y1 < x2 ∧ sorted xs.

We deduce:
... = sorted (x1 :: merge (x2::xs’) (y1::ys))
= sorted (x1 :: y1 :: merge xs ys)
= sorted (y1 :: merge xs ys)
= sorted (merge xs y)
= true by induction hypothesis

385
Case 4: x = x1::xs ∧ y = y1::ys ∧ x1 > y1.

We deduce:
sorted (merge x y) = sorted (merge (x1::xs) (y1::ys))
= sorted (y1 :: merge x ys)
= ...

Case 4.1: ys = []

We deduce:
... = sorted (y1 :: merge x [])
= sorted (y1 :: x)
= sorted x
= true

386
Case 4.2: ys = y2::ys’ ∧ x1 > y2.

In particular: y1 ≤ y2 ∧ sorted ys.

We deduce:
... = sorted (y1 :: merge x (y2::ys’))
= sorted (y1 :: y2 :: merge x ys’)
= sorted (y2 :: merge x ys’)
= sorted (merge x ys)
= true by induction hypothesis

387
Case 4.3: ys = y2::ys’ ∧ x1 ≤ y2.

In particular: y1 < x1 ≤ y2 ∧ sorted ys.

We deduce:
... = sorted (y1 :: merge (x1::xs) (y2::ys’))
= sorted (y1 :: x1 :: merge xs ys)
= sorted (x1 :: merge xs ys)
= sorted (merge x ys)
= true by induction hypothesis

388
Discussion

• Again, we have assumed for the proof that all calls of the functions
sorted and merge terminate.
• As an additional techniques, we required a thorough case
distinction over the various possibilities for arguments in calls.
• The case distinction made the proof longish and cumbersome.
// The case n=0 is in fact superfluous.
// since it is covered by the cases 1 and 2

389
8 Parallel Programming

John H. Reppy, University of Chicago

390
When your program requires multiple threads, use
ocamlc -I +threads unix.cma threads.cma <my files>
ocamlopt -I +threads unix.cmxa threads.cmxa <my files>

When you want to play with it within utop, use the following sequence
of commands:
#thread;;
#directory "+threads";;
#load "unix.cma";;
#load "threads.cma";;

391
Example

module Echo = struct open Thread

let echo () = print_string (
read_line () ^
"\n")
let main = let t1 = create echo ()
in join t1;
print_int (id (self ()));
print_string "\n"
end

392
Comments

• The module Thread collects basic functionality for the creation

of concurrency.
• The function create: (’a -> ’b) -> ’a -> t creates a
new thread with the following properties:

✷ The thread evaluates the function for its argument.

✷ The creating thread receives the thread id as the return value
and proceeds independently.
✷ By means of the functions: self : unit -> t and id
: t -> int, the own thread id can be queried and turned
into an int, respectively.

393
Further useful Functions

• The function join: t -> unit blocks the current thread until
the evaluation of the given thread has terminated.
• The function kill: t -> unit stops a given thread (not
implemented);
• The function delay: float -> unit delays the current
thread by a time period in seconds;
• The function exit: unit -> unit terminates the current
thread.

394
... running the compiled code yields:
> ./a.out
> abcdefghijk
> abcdefghijk
> 0
>

• Ocaml threads are only emulated by the runtime system.

• The creation of threads is cheap.
• Program execution terminates with the termination of the thread
with the id 0 .

395
8.1 Channels

Threads communicate via channels.

The module Event provides basic functionality for the creation of
channels, sending and receiving:

type ’a channel
new_channel : unit -> ’a channel
type ’a event
always : ’a -> ’a event
sync : ’a event -> ’a
send : ’a channel -> ’a -> unit event
receive : ’a channel -> ’a event

396
• Each call new_channel() creates another channel.
• Arbitrary data may be sent across a channel !!!
• always wraps a value into an event.
• Sending and receiving generates events ...
• Synchronization on evente returns their values.

module Exchange = struct open Thread open Event

let thread ch = let x = sync (receive ch) in
print_string (x ^ "\n");
sync (send ch "got it!")
let main = let ch = new_channel () in
let _ = create thread ch in
print_string "main is running ...\n";
sync (send ch "Greetings!");
print_string ("He " ^ sync (receive ch) ^ "\n")
end
397
Discussion

• sync (send ch str) exposes the event of sending to the

outside world and blocks the sender, until another thread has read
the value from the channel ...
• sync (receive ch) blocks the receiver, until a value has been
made available on the channel. Then this value is returned as the
result.
• Synchronous communication is one alternative for exchange of data
between threads as well as for orchestration of concurrency
==⇒ rendezvous
• In particular, it can be use to realize asynchronous communication
between threads.

398
In the example, main spawns a thread. Then it sends it a string and
waits for the answer. Accordingly, the new thread waits for the transfer
of a string value over the channel. As soon as the string is received, an
answer is sent on the same channel.

Caveat
If the ordering of send and receive is not carefully designed, threads
easily get blocked ...

Execution of the program yields:

> ./a.out
main is running ...
Greetings!
He got it!
>
399
Example: A global memory cell

A global memory cell, in particular in presence of multiple threads, can

be realized by implementing the signature Cell:

module type Cell = sig

type ’a cell
val new_cell : ’a -> ’a cell
val get : ’a cell -> ’a
val put : ’a cell -> ’a -> unit
end

The implementation must take care that the get and put calls are
sequentialized.

400
This task is delegated to a server thread that reacts to get and put:

type ’a req = Get of ’a channel | Put of ’a

type ’a cell = ’a req channel

The channel transports requests to the memory cell, which either provide
the new value or the back channel ...

401
 let get cell = let reply = new_channel ()
in sync (send cell (Get reply));
sync (receive reply)

The function get sends a new back channel on the channel cell. If the
latter is received, it waits for the return value.

let put cell x = sync (send cell (Put x))

The function put sends a Put element which contains the new value for
the memory cell.

402
Of interest now is the implementation of the cell itself:

let new_cell x = let cell = new_channel ()

in let rec serve x = match sync (receive cell)
with Get reply -> sync (send reply x);
serve x
| Put y -> serve y
in let _ = create serve x
in cell

403
Creation of the cell with initial value x spawns a server thread that
evaluates the call serve x.

Caveat

The server thread is possibly non-terminating!

This is why it can respond to arbitrarily many requests.
Only because it is tail-recursive, it does not successively consume the
whole storage ...

404
 let main = let x = new_cell 1
in print_int (get x); print_string "\n";
put x 2;
print_int (get x); print_string "\n"

Now, the execution yields

> ./a.out
1
2
>

Instead of get and put, also more complex query or update operations
could be executed by the cell server ...

405
Example: Locks

Often, only one at a time out of several active threads should be allowed
access to a given resource. In order to realize such a mutual exclusion,
locks can be applied:

module type Lock = sig

type lock
type ack
val new_lock : unit -> lock
val acquire : lock -> ack
val release : ack -> unit
end

406
Execution of the operation acquire returns an element of type
ack which is used to return the lock:

type ack = unit channel

type lock = ack channel

For simplicity, ack is chosen itself as the channel by which the lock
is returned.

let acquire lock = let ack = new_channel ()

in sync (send lock ack);
ack

407
The unlock channel is created by acquire itself

let release ack = sync (send ack ())

... and used by the operation release.

let new_lock () = let lock = new_channel ()

in let rec acq_server () =
rel_server (sync (receive lock))
and rel_server ack =
sync (receive ack);
acq_server ()
in let _ = create acq_server ()
in lock

408
Core of the implementation are the two mutually recursive functions
acq_server and rel_server.

acq_server expects an element ack, i.e., a channel, and upon

reception, calls rel_server.
rel_server expects a signal on the received channel indicated that the
lock is released ...

Now we are in the position to realize a decent deadlock:

let dead = let l1 = new_lock ()

in let l2 = new_lock ()
...

409
 in let th (l1,l2) = let a1 = acquire l1
in let _ = delay 1.0
in let a2 = acquire l2
in release a2; release a1;
print_int (id (self ()));
print_string " finished\n"
in let t1 = create th (l1,l2)
in let t2 = create th (l2,l1)
in join t1

The result is
> ./a.out

Ocaml waits for ever ...

410
Example: Semaphores

Occasionally, there is more than one copy of a resource. Then

semaphores are the method of choice ...

module type Sema = sig

type sema
new_sema : int -> sema
up : sema -> unit
down : sema -> unit
end

411
Idea

Again, a server is realized using an accumulating parameter, now

maintaining the number of free resources or, if negative, the number of
waiting threads ...

module Sema = struct open Thread open Event

type sema = unit channel option channel
let up sema = sync (send sema None)
let down sema = let ack = (new_channel() : unit channel)
in sync (send sema (Some ack));
sync (receive ack)
...

412
 let new_sema n = let sema = new_channel ()
in let rec serve (n,q) =
match sync (receive sema)
with None -> (match dequeue q
with (None,q) -> serve (n+1,q)
| (Some ack,q) -> sync (send ack ());
serve (n,q))
| Some ack -> if n>0 then (sync (send ack ());
serve (n-1,q))
else serve (n, enqueue ack q)
in let _ = create serve (n,new_queue())
in sema
end

Apparently, the queue does not maintain the waiting threads, but only
their back channels.
413
8.2 Selective Communication

A thread need not necessarily know which of several possible

communication rendezvous will occur or will occur first.
Required is a non-deterministic choice between several actions ...

Example: The function

add : int channel * int channel * int channel -> unit

is meant to read integers from two channels and send their sum to the
third.

414
First Attempt
let forever f init =
let rec loop x = loop (f x)
in let _ = create loop init
in ()
let add1 (in1, in2, out) = forever (fun () ->
sync (send out (sync (receive in1) +
sync (receive in2))
)) ()

Disadvantage
If a value arrives at the second input channel first, the thread
nonetheless must wait.

415
Second Attempt
let add (in1, in2, out) = forever (fun () ->
let (a,b) = select [
wrap (receive in1) (fun a -> (a, sync (receive in2)));
wrap (receive in2) (fun b -> (sync (receive in1), b))
]
in sync (send out (a+b))
) ()

This program must be digested slowly ...

416
Idea

→ Initiating input or output operations, generates events.

→ Events are data objects of type ’a event.
→ The function

wrap : ’a event -> (’a -> ’b) -> ’b event

applies a function a posteriori to the value of an event — given

that it occurs.

417
The list thus consists of (int*int) events.
The functions
choose : ’a event list -> ’a event
select : ’a event list -> ’a
non-deterministically choose an event from the event list.
select synchronizes with the selected event, i.e., performs the
corresponding communication task and returns the event:
let select = comp sync choose
Typically, that event is occurs that finds its communication partner first.

418
Further Examples
The function
copy : ’a channel * ’a channel * ’a channel -> unit
is meant to copy a read element into two channels:

419
 let copy (in, out1, out2) = forever (fun () ->
let x = sync (receive in)
in select [
wrap (send out1 x)
(fun () -> sync (send out2 x));
wrap (send out2 x)
(fun () -> sync (send out1 x))
]
) ()
Apparently, the event list may also consist of send events — or contain
both kinds.
type ’a cell = ’a channel * ’a channel
...

420
...
let get (get_chan,_) = sync (receive get_chan)
let put (_,put_chan) x = sync (send put_chan x)
let new_cell x = let get_chan = new_channel ()
in let put_chan = new_channel ()
in let rec serve x = select [
wrap (send get_chan x) (fun () -> serve x);
wrap (receive put_chan) serve
]
in let _ = create serve x
in (get_chan, put_chan)

421
In general, there could be a tree of events:

sync

f3 f4

send c3 x send c4 y
f1 f2

receive c1 receive c2

422
→ The leaves are basic events.
→ A wrapper function may be applied to any given event.
→ Several events of the same type may be combined into a choice.
→ Synchronization on such an event tree activates a single leaf
event. The result is obtained by successively applying the wrapper
functions from the path to the root.

423
Example: A Swap Channel

Upon rendezvous, a swap channel is meant to exchange the values of the

two participating threads. The signature is given by

module type Swap = sig

type ’a swap
val new_swap : unit -> ’a swap
val swap : ’a swap -> ’a -> ’a event
end

In the implementation with ordinary channels, every participating thread

must offer the possibility to receive and to send.

424
As soon as a thread successfully completed to send (i.e., the other
thread successfully synchronized on a receive event), the second value
must be transmitted in opposite direction.
Together with the first value, we therefore transmit a channel for the
second value:

module Swap =
struct open Thread open Event
type ’a swap = (’a * ’a channel) channel
let new_swap () = new_channel ()
...

425
 ...
let swap ch x = let c = new_channel ()
in choose [
wrap (receive ch) (fun (y,c) ->
sync (send c x); y);
wrap (send ch (x,c)) (fun () ->
sync (receive c))
]

A specific exchange can be realized by replacing choose with select.

426
Timeouts

Often, our patience is not endless.

Then, waiting for a send or receive event should be terminated ...

module type Timer = sig

set_timer : float -> unit event
timed_receive : ’a channel -> float -> ’a option event
timed_send : ’a channel -> ’a -> float -> unit option event
end

427
module Timer = stuct open Thread open Event
let set_timer t = let ack = new_channel ()
in let serve () = delay t;
sync (receive ack)
in let _ = create serve ()
in send ack ()

let timed_receive ch time = choose [

wrap (receive ch) (fun a -> Some a);
wrap (set_timer time) (fun () -> None)
]
let timed_send ch x time = choose [
wrap (send ch x) (fun a -> Some ());
wrap (set_timer time) (fun () -> None)
]
end

428
8.3 Threads and Exceptions

An exception must be handled within the thread where it has been

raised.
module Explode = struct open Thread
let thread x = (x / 0);
print_string "thread terminated regularly ...\n"
let main = let _ = create thread 0
in delay 1.0;
print_string "main terminated regularly ...\n"
end

429
... yields
> /.a.out
Thread 1 killed on uncaught exception Division_by_zero
main terminated regularly ...
The thread was killed, the Ocaml program terminated nonetheless.

Also, uncaught exceptions within the wrapper function terminate the

running thread:

module ExplodeWrap = struct open Thread open Event open Timer

let main = try sync (wrap (set_timer 1.0) (fun () -> 1 / 0))
with _ -> 0;
print_string "... this is the end!\n"
end

430
Then we have

> ./a.out
Fatal error: exception Division_by_zero

Caveat

Exceptions can only be caught in the body of the wrapper function itself,
not behind the sync !

431
8.4 Buffered Communication

A channel for buffered communication allows to send without blocking.

Receiving still may block, if no messages are available. For such
channels, we realize a module Mailbox:
module type Mailbox = sig
type ’a mbox
val new_mailbox : unit -> ’a mbox
val send : ’a mbox -> ’a -> unit
val receive : ’a mbox -> ’a event
end
For the implementation, we rely on a server which maintains a queue of
sent but not yet received messages.

432
Then we implement:

module Mailbox =
struct open Thread open Queue open Event
type ’a mbox = ’a channel * ’a channel
let send (in_chan,_) x = sync (send in_chan x)
let receive (_,out_chan) = receive out_chan
let new_mailbox () = let in_chan = new_channel ()
and out_chan = new_channel ()
...

433
 ...
in let rec serve q = if (is_empty q) then
serve (enqueue (
sync (Event.receive in_chan)) q)
else select [
wrap (Event.receive in_chan)
(fun y -> serve (enqueue y q));
wrap (Event.send out_chan (first q))
(fun () -> let (_,q) = dequeue q
in serve q)
]
in let _ = create serve (new_queue ())
in (in_chan, out_chan)
end
... where first : ’a queue -> ’a returns the first element in the
queue without removing it.

434
8.5 Multicasts

For sending a message to many receivers, a module Multicast is

provided that implements the signature Multicast:
module type Multicast = sig
type ’a mchannel and ’a port
val new_mchannel : unit -> ’a mchannel
val new_port : ’a mchannel -> ’a port
val multicast : ’a mchannel -> ’a -> unit
val receive : ’a port -> ’a event
end

435
The operation new_port generates a fresh port where a message
can be received.
The (non-blocking) operation multicast sends to all registered
ports.

module Multicast = struct open Thread open Event

module M = Mailbox
type ’a port = ’a M.mbox
type ’a mchannel = ’a channel * ’a port channel

let new_port (_, req) = let m = M.new_mailbox() in

sync (send req m); m
let multicast (send_ch,_) x = sync (send send_ch x)
let receive port = M.receive port
...

436
The operation multicast sends the message on channel send_ch. The
Operation receive reads from the mailbox of the port.
The multicast channel’s server thread maintains the list of ports:

let new_mchannel () = let send_ch = new_channel ()

in let req = new_channel ()
in let send_port x port = M.send port x
in let rec serve ports = select [
wrap (Event.receive req) (fun p ->
serve (p :: ports));
wrap (Event.receive send_ch) (fun x ->
let _ = create (List.iter (send_port x)) ports
in serve ports)
]
in let _ = create serve []
in (send_ch, req)

437
Note that the server thread must respond both to port requests over the
channel req and to send requests over send_ch.

Caveat
Our implementation supports addition, but not removal of obsolete ports.
For an example run, we use a test expression main:

438
 ...
let main = let mc = new_mchannel ()
in let thread i = let p = new_port mc
in while true do let x = sync (receive p)
in print_int i; print_string ": ";
print_string (x^"\n")
done
in let _ = create thread 1
in let _ = create thread 2
in let _ = create thread 3
in delay 1.0;
multicast mc "Hello!";
multicast mc "World!";
multicast mc "... the end.";
delay 10.0
end
end
439
We obtain
- ./a.out
3: Hello!
2: Hello!
1: Hello!
3: World!
2: World!
1: World!
3: ... the end.
2: ... the end.
1: ... the end.

440
Summary

• The programming language Ocaml offers convenient possibilities to

orchestrate concurrent programs.
• Channels with synchronous communication allow to simulate other
concepts of concurrency such as asynchronous communication,
global variables, locks for mutual exclusion and semaphors.
• Concurrent functional programs can be as obfuscated and
incomprehensible as concurrent Java programs.
• Methods are required in order to systematically verify the
correctness of such programs ...

441
Perspectives

• Beyond the language concepts discussed in the lecture, Ocaml has

diverse further concepts, which also enable object oriented
programming.
• Moreover, Ocaml has elegant means to access functionality of the
operating system, to employ graphical libraries and to communicate
with other computers ...

==⇒ Ocaml is an interesting alternative to Java.

442
9 Datalog: Computing with Relations

Example 1: The Study Program of a TU

Lecturer Module Student

+ Name offers + Title attends + Matr.nr.
+ Telefon + Room + Name
+ Email + Time + Sem.

==⇒ entity-relationship diagram

443
Discussion

• Many application domains can be described by entity-relationship

diagrams.
• Entities in the example: lecturer, module, student.
• The set of all occurring entities, i.e., of all instances can be
decribed by a table ...

Lecturer:
Name Telefon Email
Esparza 17204 esparza@in.tum.de
Nipkow 17302 nipkow@in.tum.de
Seidl 18155 seidl@in.tum.de

444
Module:
Title Room Time
Discrete Structures MI 1 Thu 12:15-13, Fri 10-11:45
Pearls of Informatics III MI 3 Thu 8:30-10
Funct. Programming and Verification MI 1 Tue 16-18
Optimization MI 2 Mon 12-14, Di 12-14

Student:
Matr.nr. Name Sem.
123456 Hans Dampf 03
007042 Fritz Schluri 11
543345 Anna Blume 03
131175 Effi Briest 05

445
Discussion (cont.)
• The rows correspond to the instances.
• The columns correspond to the attributes.
• Assumption: the first attribute identifies the instance
==⇒ primary key
Consequence: Relationships are tables as well ...

offers:
Name Title
Esparza Discrete Structures
Nipkow Pearls of Informatics III
Seidl Funct. Programming and Verification
Seidl Optimization

446
attends:

Matr.nr. Title
123456 Funct. Programming and Verification
123456 Optimization
123456 Discrete Structures
543345 Funct. Programming and Verification
543345 Discrete Structures
131175 Optimization

447
Possible Queries

• In which semester are students attending the module “Discrete

Structures” ?
• Who attends a module of lecturer “Seidl” ?
• Who attends both “Discrete Structures” and “Funct.
Programming and Verification” ?

==⇒ Datalog

448
Idea: Table ⇐=⇒ Relation

A relation R is a set of tuples, i.e.,

R ⊆ U1 × . . . × Un

where Ui is the set of all possible values for the ith component. In
our example, there are:
int, string, possibly enumeration types
// unary relations represent sets.

Relations can be described by predicates ...

449
Predicates can be defined by enumeration of facts ...

... in the Example

offers ("Esparza", "Discrete Structures").
offers ("Nipkow", "Pearls of Informatics III").
offers ("Seidl", "Funct. Programming and Verification").
offers ("Seidl", "Optimization").

attends (123456, "Optimization").

attends (123456, "Funct. Programming and Verification").
attends (123456, "Discrete Structures").
attends (543345, "Funct. Programming and Verification").
attends (543345, "Discrete Structures").
attends (131175, "Optimization").

450
Rules can be used to deduce further facts ...

... in the Example

has_attendant (X,Y) :- offers (X,Z), attends (M,Z),
student (M,Y,_).
semester (X,Y) :- attends (Z,X), student (Z,_,Y).

• :- represents the logical implication “ ⇐”.

• The comma-separated list collects the assumptions.
• The left-hand side, the head of the rule, represents the conclusion.
• Variables start with a capital letter.
• The anonymous variable _ refers to irrelevant values.

451
The knowledge base consisting of facts and rules now can be queried ...

... in the Example

?- has_attendant ("Seidl", Z).

• Datalog finds all values for Z so that the query can be deduced
from the given facts by means of the rules.
• In our examples these are:

Z = "Hans Dampf"
Z = "Anna Blume"
Z = "Effi Briest"

452
Further Queries

?- semester ("Discrete Structures", X).

X = 2
X = 4

?- attends (X, "Funct. Programming and Verification"),

attends (X, "Discrete Structures").
X = 123456
X = 543345

453
Further Queries

?- semester ("Discrete Structures", X).

X = 2
X = 4

?- attends (X, "Funct. Programming and Verification"),

attends (X, "Discrete Structures").
X = 123456
X = 543345

Caveat
A query may contain none, one or several variables.

454
An Example Proof
The rule
has_attendant (X,Y) :- offers (X,Z), attends (M,Z),
student (M,Y,_).
holds for all X, M, Y, Z.

455
An Example Proof
The rule
has_attendant (X,Y) :- offers (X,Z), attends (M,Z),
student (M,Y,_).
holds for all X, M, Y, Z. By means of the substitution
"Seidl"/X "Funct. Programming ..."/Z
543345/M "Anna Blume"/Y
we prove
offers ("Seidl", "Funct. Programming ...")
attends (543345, "Funct. Programming ...")
student (543345, "Anna Blume", 3)
has_attendant ("Seidl", "Anna Blume")

456
Example 2: A Weblog

Eintrag
Weblog
edits contains + ID
Group + Title + Contents
+ Date

Person
has member + Account owns
+ Name
− Password
trusts

457
Task: Specification of access rights

• Every member of the group of editors is entitled to add an entry.

• Only the owner of an entry is allowed to delete it.
• Everybody trusted by the owner, is entitled to modify.
• Every member of the group as well as everybody directly or
indirectly trusted by a memober of the group, is allowed to read ...

458
Specification in Datalog

may_add (X,W) :- edits (Z,W),

has_member (Z,X).
may_delete (X,E) :- owns (X,E).
may_modify (X,E) :- owns (X,E).
may_modify (X,E) :- owns (Y,E),
trusts (Y,X).
may_read (X,E) :- contains (W,E),
may_add (X,W).
may_read (X,E) :- may_read (Y,E),
trusts (Y,X).

459
Remark

• All available predicates or even fresh auxiliary predicates can be

used for the definition of new predicates.
• Apparently, predicate definitions may be recursive.
• Together with a person X owning an entry, also all persons are
entitled to modify trusted by X.
• Together with a person Y entitled to read, also all persons are
entitled to read trusted by Y.

460
9.1 Answering a Query

Given: a set of facts and rules

Wanted: the set of all provable facts

Problem
equals (X,X).

==⇒ the set of all provable facts is infinite.

461
Theorem

Assume that W is a finite set of facts and rules with the following
properties:

(1) Facts do not contain variables.

(2) Every variable in the head, also occurs in the body.

Then the set of provable facts is finite.

462
Theorem

Assume that W is a finite set of facts and rules with the following
properties:

(1) Facts do not contain variables.

(2) Every variable in the head, also occurs in the body.

Then the set of provable facts is finite.

Proof Sketch

For every provable fact p(a1,...,ak), it is shown that each constant

ai already occurs in W.

463
Calculation of All Provable Facts

Successively compute the sets R (i ) of all facts having proofs of depth

at most i ...

R(0) = ∅ R (i + 1 ) = F ( R (i ) )

where the operator F is defined by

F ( M) = {h[ a/ X ] | ∃ h :- l1 , . . . , lk . ∈ W :
l1 [ a/ X ], . . . , lk [ a/ X ] ∈ M }

// [ a/ X ] a substitution of the variables X

// k can be equal to 0.

464
We have: R(i) = F i (∅) ⊆ F i+1 (∅) = R(i+1)

465
We have: R(i) = F i (∅) ⊆ F i+1 (∅) = R(i+1)

The set R of all implied facts is given by

S
R= i≥0 R (i ) = R ( n )

for a suitable n — since R is finite.

466
We have: R(i) = F i (∅) ⊆ F i+1 (∅) = R(i+1)

The set R of all implied facts is given by

S
R= i≥0 R (i ) = R ( n )

for a suitable n — since R is finite.

Example
edge (a,b).
edge (a,c).
edge (b,d).
edge (d,a).
t (X,Y) :- edge (X,Y).
t (X,Y) :- edge (X,Z), t (Z,Y).

467
Relation edge :
a b c d
a
b
c
d

468
t (0) a b c d t (1) a b c d
a a
b b
c c
d d

469
t (2) a b c d t (3) a b c d
a a
b b
c c
d d

470
Discussion

• Our considerations are strong enough to calculate all facts implied

by a Datalog program.
• From that, the set of answer substitutions can be extracted.

471
Discussion

• Our considerations are strong enough to calculate all facts implied

by a Datalog program.
• From that, the set of answer substitutions can be extracted.
• The naive approach, however, is hopelessly inefficient.
• Smarter approaches try to avoid multiple calculations of the ever
identical same facts ...
• In particular, only those facts need be proven which are useful for
answering the query ==⇒ compiler construction, databases

472
9.2 Operations on Relations

• We use predicates in order to describe relations.

• There are natural operations on relations which we would like to
express in Datalog, i.e., define for predicates.

473
1. Union

474
... in Datalog:

r( X1 , . . . , Xk ) :- s1 ( X1 , . . . , Xk ).
r( X1 , . . . , Xk ) :- s2 ( X1 , . . . , Xk ).

Example

attends_Esparza_or_Seidl (X) :- has_attendant ("Esparza", X).

attends_Esparza_or_Seidl (X) :- has_attendant ("Seidl", X).

475
2. Intersection

476
... in Datalog:

r( X1 , . . . , Xk ) :- s1 ( X1 , . . . , Xk ),
s2 ( X1 , . . . , Xk ).

Example

attends_Esparza_and_Seidl (X) :- has_attendant ("Esparza", X),

has_attendant ("Seidl", X).

477
3. Relative Complement

478
... in Datalog:

r( X1 , . . . , Xk ) :- s1 ( X1 , . . . , Xk ), not(s2 ( X1 , . . . , Xk )).

i.e., r( a1 , . . . , ak ) follows when s1 ( a1 , . . . , ak ) holds but

s2 ( a1 , . . . , ak ) is not provable.

Example

does_not_attend_Seidl (X) :- student (_,X,_),

not (has_attendant ("Seidl", X)).

479
Caveat
The query
p("Hello!").
?- not (p(X)).
results in infinitely many answers.

==⇒ we allow negated literals only if all occurring variables

==⇒ have already occurred to the left in non-negated literals.
p("Hello!").
q("Damn ...").
?- q(X), not (p(X)).
X = "Damn ..."

480
Caveat (cont.):
Negation is only meaningful when s does not recursively depend on
r ...

p(X) :- not (p(X)).

... is not easy to interpret.

==⇒ We allow not(s(. . .)) only in rules for

==⇒ predicates r of which s is independent
==⇒ stratified negation

// Without recursive predicates, every negation is stratified.

481
4. Cartesian Product

S1 × S2 = {( a1 , . . . , ak , b1 , . . . , bm ) | ( a1 , . . . , ak ) ∈ S1 ,
(b1 , . . . , bm ) ∈ S2 }

... in Datalog:

r( X1 , . . . , Xk , Y1 , . . . , Ym ) :- s1 ( X1 , . . . , Xk ), s2 (Y1 , . . . , Ym ).

482
 a b c d
a a a
b b b
c c c
d d d

483
Example
lecturer_student (X,Y) :- lecturer (X,_,_),
student (_,Y,_).

Comments

• The product of independent relations is very expensive.

• It should be avoided whenever possible ;-)

484
5. Projection

πi1 ,...,ik ( S) = {( ai1 , . . . , aik ) | ( a1 , . . . , am ) ∈ S}

... in Datalog:

r( Xi1 , . . . , Xik ) :- s( X1 , . . . , Xm ).

485
 a b c d
a a
b b
1 c c
d d

486
 a b c d a b c d
a a
b b
1,1 c c
d d

487
6. Join

S1 ✶ S2 = {( a1 , . . . , ak , b1 , . . . , bm ) | ( a1 , . . . , ak+1 ) ∈ S1 ,
(b1 , . . . , bm ) ∈ S2 ,
ak+1 = b1 }

... in Datalog:

r( X1 , . . . , Xk , Y1 , . . . , Ym ) :- s1 ( X1 , . . . , Xk , Y1 ), s2 (Y1 , . . . , Ym ).

488
Discussion
Joins can be defined by means of the other operations ...

S1 ✶ S2 = π1,...,k,k+2,...,k+1+m (
S1 × S2 ∩
U k × π1,1 (U ) × U m−1 )

// For simplicity, we have assumed that U is the

// joint universe of all components.

Joins often allow to avoid expensive cartesian products.

The presented operations on relations form the basis of Relational

Algebra ...

489
Background

Relational Algebra ...

+ is the basis underlying the query languages of Relational Databases

==⇒ SQL
+ allows optimization of queries.
Idea: Replace expensive sub-expressions of the query with cheaper
expressions of the same semantics !

490
Background

Relational Algebra ...

+ is the basis underlying the query languages of relational databases

==⇒ SQL
+ allows optimization of queries.
Idea: Replace expensive sub-expressions of the query with cheaper
expressions of the same semantics !

− is rather cryptic
− does not support recursive definitions.

491
Example

The Datalog predicate

semester (X,Y) :- attends (Z,X), student (Z,_,Y)

... can be expressed in SQL by

SELECT attends.Title, Student.Semester

FROM attends, Student
WHERE attends.Matrikelnumber = Student.Matrikelnumber

492
Perspective

• Besides a query language, a realistic database language must also

offer the possibility for insertion / modification / deletion.
• The implementation of a database must be able to handle not just
toy applications like our examples, but to deal with gigantic mass
data !!!
• It must be able to reliably execute multiple concurrent transactions
without messing up individual tasks.
• A database also should be able to survive power supply failure
==⇒ Database Lecture

493