FIT5138: Advanced Software Engineering

Revision of Basic Discrete Maths

Yuan-Fang Li, 2020

Lecture 8

Based on the slides Summary of Mathematical Notation

by Jean-Raymond Abrial (ETHZ), 2008.

!

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 1 / 89

Reading: seL4

Outline

1 Reading: seL4

2 A Quick Review of Propositional Calculus

3 A Quick Review of First-order Predicate Calculus

4 A Quick Review of Set Theory

5 A Quick Review of Arithmetic

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 2 / 89

seL4: Formal Verification of an Operating-System Kernel

Gerwin Klein1,2, June Andronick1,2, Kevin Elphinstone1,2, Gernot Heiser1,2,3

David Cock1, Philip Derrin1⇤, Dhammika Elkaduwe1,2‡, Kai Engelhardt1,2

Rafal Kolanski1,2, Michael Norrish1,4, Thomas Sewell1, Harvey Tuch1,2†, Simon Winwood1,2

1 NICTA, 2 UNSW, 3 Open Kernel Labs, 4 ANU

[email protected]

ABSTRACT

We report on the formal, machine-checked verification of

the seL4 microkernel from an abstract specification down to

its C implementation. We assume correctness of compiler,

assembly code, hardware, and boot code.

seL4 is a third-generation microkernel of L4 provenance,

comprising 8,700 lines of C and 600 lines of assembler. Its

performance is comparable to other high-performance L4

kernels.

We prove that the implementation always strictly follows

our high-level abstract specification of kernel behaviour. This

encompasses traditional design and implementation safety

properties such as that the kernel will never crash, and it

will never perform an unsafe operation. It also implies much

more: we can predict precisely how the kernel will behave in

every possible situation.

1. INTRODUCTION

Almost every paper on formal verification starts with the

observation that software complexity is increasing, that this

leads to errors, and that this is a problem for mission and

safety critical software. We agree, as do most.

Here, we report on the full formal verification of a critical

system from a high-level model down to very low-level C

code. We do not pretend that this solves all of the software

complexity or error problems. We do think that our approach

will work for similar systems. The main message we wish to

convey is that a formally verified commercial-grade, general-

purpose microkernel now exists, and that formal verification

is possible and feasible on code sizes of about 10,000 lines of C.

It is not cheap; we spent significant e↵ort on the verification,

but it appears cost-e↵ective and more a↵ordable than other

methods that achieve lower degrees of trustworthiness.

To build a truly trustworthy system, one needs to start at

the operating system (OS) and the most critical part of the

OS is its kernel. The kernel is defined as the software that

executes in the privileged mode of the hardware, meaning

that there can be no protection from faults occurring in the

⇤Philip Derrin is now at Open Kernel Labs.

†Harvey Tuch is now at VMware.

‡Dhammika Elkaduwe is now at University of Peradeniya

Permission to make digital or hard copies of all or part of this work for

personal or classroom use is granted without fee provided that copies are

not made or distributed for profit or commercial advantage and that copies

bear this notice and the full citation on the first page. To copy otherwise, to

republish, to post on servers or to redistribute to lists, requires prior specific

permission and/or a fee.

Copyright 2008 ACM 0001-0782/08/0X00 ...$5.00.

Figure 1: Call graph of the seL4 microkernel. Ver-

tices represent functions, and edges invocations.

kernel, and every single bug can potentially cause arbitrary

damage. The kernel is a mandatory part of a system’s

trusted computing base (TCB)—the part of the system that

can bypass security [10]. Minimising this TCB is the core

concept behind microkernels, an idea that goes back 40 years.

A microkernel, as opposed to the more traditional mono-

lithic design of contemporary mainstream OS kernels, is

reduced to just the bare minimum of code wrapping hard-

ware mechanisms and needing to run in privileged mode. All

OS services are then implemented as normal programs, run-

ning entirely in (unprivileged) user mode, and therefore can

potentially be excluded from the TCB. Previous implemen-

tations of microkernels resulted in communication overheads

that made them unattractive compared to monolothic ker-

nels. Modern design and implementation techniques have

managed to reduced this overhead to very competitive limits.

A microkernel makes the trustworthiness problem more

tractable. A well-designed high-performance microkernel,

such as the various representatives of the L4 microkernel

family, consists of the order of 10,000 lines of code (10 kloc).

This radical reduction to a bare minimum comes with a price

in complexity. It results in a high degree of interdependency

between di↵erent parts of the kernel, as indicated in Fig. 1.

Despite this increased complexity in low-level code, we have

demonstrated that with modern techniques and careful de-

Reading: seL4

seL4: Formal Verification of an Operating System Kernel

Klein, Gerwin, et al. “seL4: formal verification of an OS kernel”.

Proceedings of the ACM SIGOPS 22nd symposium on Operating systems

principles, pp. 207-220, ACM 2009.

Kernel: “the software that executes in the privileged mode of the

hardware”—faults in kernel can be disastrous

Microkernel: “bare minimum of code wrapping hardware

mechanisms and needing to run in privileged mode”

seL4: 10,000 LOC (C + assembly)

Formally verified from an abstract specification down to its

implementation in C: proof of functional correctness

Using a theorem proving approach (Isabelle/HOL)

Interactive, however, stronger than model checking

The system is proved to have no code injection attacks, buffer

overflows, NULL pointer access, memory leaks, non-termination,

arithmetic exceptions, unchecked user arguments

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 3 / 89

Reading: seL4

Presentation of the Mathematical Language

It will be done by successive refinements:

1 Propositional language

2 First-order predicate language

3 Equality & pairs

4 Set theory

5 Arithmetic

Each additional language is built on top of the previous ones

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 4 / 89

A Quick Review of Propositional Calculus

Outline

1 Reading: seL4

2 A Quick Review of Propositional Calculus

3 A Quick Review of First-order Predicate Calculus

4 A Quick Review of Set Theory

5 A Quick Review of Arithmetic

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 5 / 89

A Quick Review of Propositional Calculus

Basic Constructs of Propositional Calculus

Given predicates P & Q, we can construct:

Negation: ¬P

Conjunction: P ∧ Q

Implication: P ⇒ Q

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 6 / 89

A Quick Review of Propositional Calculus

Syntax

Predicate ::= ¬Predicate

Predicate ∧ Predicate

Predicate ⇒ Predicate

This syntax is ambiguous

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 7 / 89

A Quick Review of Propositional Calculus

More on Syntax

Pairs of matching parentheses can be added freely

Operator ∧ is associative: P ∧ Q ∧ R is allowed

Operator ⇒ is not associative: P ⇒ Q ⇒ R is not allowed

Write explicitly either (P ⇒ Q)⇒ R or P ⇒ (Q ⇒ R)

Operators have precedence in this decreasing order: ¬, ∧, ⇒

Example:

¬P ⇒ Q ∧ R is to be read as (¬P)⇒ (Q ∧ R)

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 8 / 89

A Quick Review of Propositional Calculus

Extensions: Falsity, Truth, Disjunction & Equivalence

Falsity: ⊥

Truth: >

Disjunction: P ∨ Q

Equivalence: P ⇔ Q

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 9 / 89

A Quick Review of Propositional Calculus

Syntax

predicate ::=⊥

>

¬predicate

predicate ∧ predicate

predicate ∨ predicate

predicate ⇒ predicate

predicate ⇔ predicate

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 10 / 89

A Quick Review of Propositional Calculus

More on Syntax

Pairs of matching parentheses can be added freely

Operators ∧, ∨ and ⇔ are associative

Operator ⇒ is not associative

Precedence decreasing order: ¬, ∧ and ∨, ⇒ and ⇔

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 11 / 89

A Quick Review of Propositional Calculus

Exercise: associativity

Give an example that shows logical implication (⇒) is not associative.

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 12 / 89

A Quick Review of Propositional Calculus

More on Syntax (cont’ed)

The mixing of ∧ and ∨ without parentheses is not allowed

You have to write either P ∧ (Q ∨ R) or (P ∧ Q) ∨ R

The mixing of ⇒ and ⇔ without parentheses is not allowed

You have to write either P ⇒ (Q ⇔ R) or (P ⇒ Q)⇔ R

Example:

R ∧ (¬P ⇒ Q)⇔ (P ∨ Q) ∧ R

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 13 / 89

A Quick Review of Propositional Calculus

Definitions of the New Constructs

⊥ == P ∧ ¬P

> == ¬⊥

P ∨ Q == ¬P ⇒ Q

P ⇔ Q == (P ⇒ Q) ∧ (Q ⇒ P)

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 14 / 89

A Quick Review of First-order Predicate Calculus

Outline

1 Reading: seL4

2 A Quick Review of Propositional Calculus

3 A Quick Review of First-order Predicate Calculus

4 A Quick Review of Set Theory

5 A Quick Review of Arithmetic

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 15 / 89

A Quick Review of First-order Predicate Calculus

Syntax of our Predicate Language so far

predicate ::=⊥

>

¬predicate

predicate ∧ predicate

predicate ∨ predicate

predicate ⇒ predicate

predicate ⇔ predicate

The letters P, Q etc. we have used are generic variables

Each of them stands for a predicate

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 16 / 89

A Quick Review of First-order Predicate Calculus

Refining our Language: Predicate Calculus

predicate ::=⊥

>

¬predicate

predicate ∧ predicate

predicate ∨ predicate

predicate ⇒ predicate

predicate ⇔ predicate

∀var list · predicate

expression ::=variable

variable ::=identifier

var list ::=variable

variable, var list

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 17 / 89

A Quick Review of First-order Predicate Calculus

On Predicates & Expressions

A Predicate is a formal text that can be proved

A Predicate denotes nothing.

An Expression is a formal text denoting an object.

An Expression cannot be proved.

Predicates and Expressions are incompatible.

Expressions will be considerably extended in the set-theoretic and

arithmetic notations.

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 18 / 89

A Quick Review of First-order Predicate Calculus

Refining our Language: Existential Quantification

predicate ::= ⊥

. . .

∀var list · predicate

∃var list · predicate

expression ::= variable

variable ::= identifier

varl ist ::= variable

variable, var list

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 19 / 89

A Quick Review of First-order Predicate Calculus

Definition of Existential Quantification

∃x · P == ¬(∀x · ¬P)

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 20 / 89

A Quick Review of First-order Predicate Calculus

Exercise: quantifications

True predicates

Give an example of a true existentially quantified predicate.

Given an example of a true universally quantified predicate.

False predicates

Give an example of a false existentially quantified predicate.

Given an example of a false universally quantified predicate.

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 21 / 89

A Quick Review of First-order Predicate Calculus

Summary of Logical Operators

¬P

P ∧ Q P ∨ Q

P ⇒ Q P ⇔ Q

∀x · P ∃x · P

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 22 / 89

A Quick Review of First-order Predicate Calculus

Refining our Language: Equality & Pairs

predicate ::= ⊥

. . .

∃var list · predicate

expression = expression . equality

expression ::= variable

expression 7→ expression . pair

variable ::= . . .

var list ::= . . .

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 23 / 89

A Quick Review of Set Theory

Outline

1 Reading: seL4

2 A Quick Review of Propositional Calculus

3 A Quick Review of First-order Predicate Calculus

4 A Quick Review of Set Theory

5 A Quick Review of Arithmetic

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 24 / 89

A Quick Review of Set Theory

Refining our Language: Set Theory (1)

predicate ::= ⊥

>

predicate ∧ predicate

predicate ∨ predicate

predicate ⇒ predicate

predicate ⇔ predicate

∀var list · predicate

∃var list · predicate

expression = expression

expression ∈ set . set membership

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 25 / 89

A Quick Review of Set Theory

Refining our Language: Set Theory (2)

expression ::= variable

expression 7→ expression

set

variable ::= . . .

set ::= set × set . Cartesian product

P(set) . power set

{var list · predicate|expression} . set comprehension

when expression is the same as var list, the last construct can be written

{var list|predicate}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 26 / 89

A Quick Review of Set Theory Basic operators

Set Theory: Membership

Set theory deals with a new predicate, the membership predicate:

E ∈ S

where E is an expression and S is a set

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 27 / 89

A Quick Review of Set Theory Basic operators

Set Theory: Basic Constructs

There are 3 basic constructs:

Cartesian product: S × T

Power set: P(S)

Comprehension 1: {x · x ∈ S ∧ P(x)|F (x)}

Comprehension 2: {x |x ∈ S ∧ P(x)}

where S & T are sets, x is a variable & P is a predicate

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 28 / 89

A Quick Review of Set Theory Basic operators

Cartesian Product

Cartesian Product 55

S T

S x T

a1

a2

b1

b2

b3

55

Definition: E 7→ F ∈ S × T ⇔ E ∈ S ∧ F ∈ T

S × T = {(a1, b1), (a1, b2), (a1, b3), (a2, b1), (a2, b2), a2, b3)} =

{a1 7→ b1, a1 7→ b2, a1 7→ b3, a2 7→ b1, a2 7→ b2, a2 7→ b3}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 29 / 89

A Quick Review of Set Theory Basic operators

Powerset Power Set 56

a2a1

a1 a2 a3

a1

a2

a3

S

a3a1 a2

a3a1 a3a2

P(S)

56

Definition: S ∈ P(T )⇔ ∀x · x ∈ S ⇒ x ∈ T

S = {a1, a2, a3}

P(S) = {∅, {a1}, {a2}, {a3}, {a1, a2}, {a1, a3}, {a2, a3}, {a1, a2, a3}}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 30 / 89

A Quick Review of Set Theory Basic operators

Set Comprehension 2

Set Comprehension 57

a1

a8

a7

a3

a2

a6

a5

a4

S

Subset of S

57

Definition: E ∈ {x |x ∈ S ∧ P(x)} ⇔ E ∈ S ∧ P(E )

S = {a1, a2, a3, a4, a5, a6, a7, a8}

T = {x |x ∈ S ∧ x ∈ {a4, a5, a6}} (T is a subset of S)

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 31 / 89

A Quick Review of Set Theory Basic operators

Basic Set Operator Membership

The following axioms are equivalent

Left part Right part

E 7→ F ∈ S × T E ∈ S ∧ F ∈ T

S ∈ P(T ) ∀x · x ∈ S ⇒ x ∈ T

E ∈ {x · x ∈ S ∧ P(x)|F (x)} ∃x · x ∈ S ∧ P(x) ∧ E = F (x)

E ∈ {x |x ∈ S ∧ P(x)} E ∈ S ∧ P(E )

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 32 / 89

A Quick Review of Set Theory Basic operators

Exercise: basic set operators

Cartesian product

Let Personnel = {yuanfang , lito,wud}, Roles = {lecturer , tutor}.

Personnel × Roles =

Comprehension

Let S = {1, 2, 3, . . . , 20}.

“Divisible by 4” expressed as a set comprehension expression:

“The square of those divisible by 4” expressed as a set comprehension

expression:

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 33 / 89

A Quick Review of Set Theory Basic operators

Set Inclusion & Extensionality Axiom

Left part Right part

S ⊆ T S ∈ P(T )

S = T S ⊆ T ∧ T ⊆ S

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 34 / 89

A Quick Review of Set Theory Basic operators

Elementary Set Operators

Union: S ∪ T

Intersection: S ∩ T

Differenece: S \ T

Extension: {a, . . . , b} (or enumeration)

Empty set: ∅

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 35 / 89

A Quick Review of Set Theory Basic operators

Union, Difference, Intersection

Union, Difference, Intersection 61

Intersection

DifferenceUnion

61

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 36 / 89

A Quick Review of Set Theory Basic operators

Elementary Set Operator Membership

Left part Right part

E ∈ S ∪ T E ∈ S ∨ E ∈ T

E ∈ S ∩ T E ∈ S ∧ E ∈ T

E ∈ S \ T E ∈ S ∧ E /∈ T

E ∈ {a, . . . , b} E = a ∨ . . .E = b

E ∈ ∅ ⊥

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 37 / 89

A Quick Review of Set Theory Basic operators

Summary of Basic & Elementary Operators

S × T S ∪ T

P(S) S ∩ T

{x |x ∈ S ∧ P} S \ T

S ⊆ T {a, . . . , b}

S = T ∅

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 38 / 89

A Quick Review of Set Theory Generalisations of elementary operators

Generalisations of Elementary Operators

Generalised union: union(S) or

⋃

(S)

Generalised intersection: inter(S) or

⋂

(S)

Intuition: To flatten a set of sets

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 39 / 89

A Quick Review of Set Theory Generalisations of elementary operators

Generalised UnionG neralized Union 65

a1

a2

a3

a4

a5

a1

a3

a2

a3

a5

a4

a2

a1

S union(S)

65

Definition: E ∈ union(S)⇔ ∃s · s ∈ S ∧ E ∈ s

union(S) = {a1, a2, a3, a4, a5}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 40 / 89

A Quick Review of Set Theory Generalisations of elementary operators

Generalised IntersectionG neralized Intersection 66

a2

a4

a1

S

a3

a4

a3

a5

a1

a1

a3

a2

a1

a3

inter(S)

66

Definition: E ∈ inter(S)⇔ ∀s · s ∈ S ⇒ E ∈ s

inter(S) = {a1, a3}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 41 / 89

A Quick Review of Set Theory Generalisations of elementary operators

Generalisation of Elementary Operators Membership

E ∈ union(S) ∃s · s ∈ S ∧ E ∈ s

E ∈ inter(S) ∀s · s ∈ S ⇒ E ∈ s

Well-definedness condition for inter(S): S 6= ∅

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 42 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operators (1)

Binary relations: S ↔ T

Domain: dom(r)

Range: ran(r)

Converse: r−1

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 43 / 89

A Quick Review of Set Theory Binary Relation Operators

Example: a Binary Relation r between a Set A and a Set B

A Binary Relation r from a Set A to a Set B 70

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a1

a4

r

r A B

70

Definition: r ∈ A↔ B ⇔ r ⊆ A× B

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 44 / 89

A Quick Review of Set Theory Binary Relation Operators

Exercise: basic relationsA Binary Relation r from a Set A to a Set B 70

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a1

a4

r

r A B

70

Given r ∈ A↔ B,

What is represented by r?

What is represented by A↔ B?

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 45 / 89

A Quick Review of Set Theory Binary Relation Operators

Domain of Binary Relation rDomain of Binary Rel tion r 71

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a4

r

a1

dom(r) = {a1, a3, a5, a7}

71

Definition: E ∈ dom(r)⇔ ∃y · E 7→ y ∈ r

dom(r) = {a1, a3, a5, a7}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 46 / 89

A Quick Review of Set Theory Binary Relation Operators

Range of Binary Relation rRange of Binary Relation r 72

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a1

a4

r

ran(r) = {b1, b2, b4, b6}

72

Definition: F ∈ ran(r)⇔ ∃x · x 7→ F ∈ r

ran(r) = {b1, b2, b4, b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 47 / 89

A Quick Review of Set Theory Binary Relation Operators

Converse of Binary Relation rConverse of Binary Relation r 73

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a1

a4

r

r1 = {b1 ✏⌃ a3, b2 ✏⌃ a1, b2 ✏⌃ a5, b2 ✏⌃ a7, b4 ✏⌃ a3, b6 ✏⌃ a7}

73

Definition: E 7→ F ∈ r−1 ⇔ F 7→ E ∈ r

r−1 = {b1 7→ a3, b2 7→ a1, b2 7→ a5, b2 7→ a7, b4 7→ a3, b6 7→ a7}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 48 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operator Membership (1)

Left part Right part

r ∈ S ↔ T r ⊆ S × T

E ∈ dom(r) ∃y · E 7→ y ∈ r

F ∈ ran(r) ∃x · x 7→ F ∈ r

E 7→ F ∈ r−1 F 7→ E ∈ r

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 49 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operators (2)

Partial surjective binary relations: S ↔→ T

Every element in T has a mapping by r

Total binary relations: S ←↔ T

Every element in S has a mapping by r

Total surjective binary relations: S ↔ T

Every element in S and T has a mapping by r

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 50 / 89

A Quick Review of Set Theory Binary Relation Operators

Example: a Partial Surjective RelationA Partial Surjective Relation 76

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a1

a4

r

r ∈ A↔→B

76

Definition: r ∈ A↔→ B ⇔ r ∈ A↔ B ∧ ran(r) = B

r ∈ A↔→ B = {a1 7→ b2, a3 7 b1, a3 7→ b3, a3 7→ b4,

a5 7→ b2, a5 7→ b5, a7 7→ b2, a7 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 51 / 89

A Quick Review of Set Theory Binary Relation Operators

Example: a Total RelationA Total Relation 77

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a1

a4

r

r ∈ A←↔B

77

Definition: r ∈ A←↔ B ⇔ r ∈ A↔ B ∧ dom(r) = A

r ∈ A←↔ B = {a1 7→ b2, a2 7→ b6, a3 7→ b3, a4 7→ b3,

a5 7→ b2, a6 7→ b1, a7 7→ b2, a7 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 52 / 89

A Quick Review of Set Theory Binary Relation Operators

Example: a Total Surjective RelationA Total Surjective Relation 78

A B

a3a2

a6

a7

b1

b3

b4

b5

b6

b2

a5

a1

a4

r

r ∈ A↔ B

78

Definition: r ∈ A↔ B ⇔ r ∈ A↔→ B ∧ r ∈ A←↔ B

r ∈ A↔ B = {a1 7→ b2, a2 7→ b6, a3 7→ b1, a3 7→ b3, a3 7→ b4, a4 7→ b3,

a5 7→ b2, a5 7→ b5, a6 7→ b1, a7 7→ b2, a7 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 53 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operator Membership (2)

Left part Right part

r ∈ S ↔→ T r ∈ S ↔ T ∧ ran(r) = T

r ∈ S ←↔ T r ∈ S ↔ T ∧ dom(r) = S

r ∈ S ↔ T r ∈ S ↔→ T ∧ r ∈ S ←↔ T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 54 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operators (3)

For a relation r ∈ S ↔ T :

Domain restriction: S C r

Range restriction: r B T

Domain subtraction: S C− r

Range subtraction: r B− T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 55 / 89

A Quick Review of Set Theory Binary Relation Operators

The Domain Restriction OperatorThe Domain Restricti n Operator 81

A B

a3a2

a6

a7

b1

F

b3

b4

b5

b6

b2

a5

a1

a4

{a3, a7} F

81

Definition: x 7→ y ∈ AC r ⇔ x ∈ A ∧ x 7→ y ∈ r

{a3, a7}C F = {a3 7→ b4, a7 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 56 / 89

A Quick Review of Set Theory Binary Relation Operators

The Range Restriction OperatorThe Range Restriction Operator 82

A B

a3a2

a6

a7

b1

F

b3

b4

b5

b6

b2

a5

a1

a4

F ⇤ {b2, b4}

82

Definition: x 7→ y ∈ r B B ⇔ x 7→ y ∈ r ∧ y ∈ B

F B {b2, b4} = {a1 7→ b2, a5 7→ b2, a3 7→ b4}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 57 / 89

A Quick Review of Set Theory Binary Relation Operators

The Domain Subtraction OperatorThe Domain Restriction Operator 83

A B

a3a2

a6

a7

b1

F

b3

b4

b5

b6

b2

a5

a1

a4

{a3, a7} F

83

Definition: x 7→ y ∈ AC− r ⇔ x /∈ A ∧ x 7→ y ∈ r

{a3, a7}C− F = {a1 7→ b2, a5 7→ b2}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 58 / 89

A Quick Review of Set Theory Binary Relation Operators

The Range Subtraction OperatorThe Range Restri tion Operator 84

A B

a3a2

a6

a7

b1

F

b3

b4

b5

b6

b2

a5

a1

a4

F ⇤ {b2, b4}

84

Definition: x 7→ y ∈ r B− B ⇔ x 7→ y ∈ r ∧ y /∈ B

F B− {b2, b4} = {a7 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 59 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operator Membership (3)

Left part Right part

E 7→ F ∈ S C r E ∈ S ∧ E 7→ F ∈ r

E 7→ F ∈ r B T E 7→ F ∈ r ∧ F ∈ T

E 7→ F ∈ S C− r E /∈ S ∧ E 7→ F ∈ r

E 7→ F ∈ r B− T E 7→ F ∈ r ∧ F /∈ T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 60 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operators (4)

Image: r [w ]

Composition: p ; q

Overriding: p C− q

Identity: id(S)

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 61 / 89

A Quick Review of Set Theory Binary Relation Operators

Image of {a, b} under r

Image of {a, b} under r 87

S T

r

b

a

m

d

c

s

r

q

n

p

r[{a, b}] = {m,n, p}

87

F ∈ r [w ]⇔ ∃x · x ∈ w ∧ x 7→ F ∈ r

r [{a, b}] = {m, n, p}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 62 / 89

A Quick Review of Set Theory Binary Relation Operators

Forward CompositionForward Composition 88

S T U

S U

F G

F ; G

88

E 7→ F ∈ (p ; q)⇔ ∃x · E 7→ x ∈ p ∧ x 7→ F ∈ q

F ; G ∈ S ↔ U

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 63 / 89

A Quick Review of Set Theory Binary Relation Operators

The Overriding Operator

The Overriding Operator 90

F G

F G

90

a

b

x

y

a

b

x

y

c

c

z

z

w

w

p C− q ⇔ (dom(q)C− p) ∪ q

F C− G = F \ {a 7→ w , b 7→ w} ∪ {a 7→ x , b 7→ y , c 7→ z}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 64 / 89

A Quick Review of Set Theory Binary Relation Operators

The Identity Relation

The Identity Relation 93

a1

a2

a3

a4

a1

a2

a3

a4

S S

93

E 7→ F ∈ id(S)⇔ E ∈ S ∧ F = E

id(S) = {a1 7→ a1, . . . , a4 7→ a4}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 65 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operator Membership (4)

Left part Right part

F ∈ r [w ] ∃x · x ∈ w ∧ x 7→ F ∈ r

E 7→ F ∈ (p ; q) ∃x · E 7→ x ∈ p ∧ x 7→ F ∈ q

p C− q (dom(q)C− p) ∪ q

E 7→ F ∈ id(S) E ∈ S ∧ F = E

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 66 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operators (5)

First projection: prj1(S ,T )

Second projection: prj2(S ,T )

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 67 / 89

A Quick Review of Set Theory Binary Relation Operators

Binary Relation Operator Membership (5)

Left part Right part

(E 7→ F ) 7→ G ∈ prj1(S ,T ) E ∈ S ∧ F ∈ T ∧ G = E

(E 7→ F ) 7→ G ∈ prj2(S ,T ) E ∈ S ∧ F ∈ T ∧ G = F

Alternatively, for row 1, prj1(E 7→ F ) = E

Alternatively, for row 2, prj2(E 7→ F ) = F

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 68 / 89

A Quick Review of Set Theory Binary Relation Operators

Exercise: binary relation operators

Let A = {a, b, c , d},B = {l ,m, n},

Projections

prj1(a 7→ (b 7→ n)) = prj2(a 7→ (b 7→ n)) =

prj1((a 7→ b) 7→ n) = prj2((a 7→ b) 7→ n) =

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 69 / 89

A Quick Review of Set Theory Binary Relation Operators

Summary of Binary Relation Operators

S ↔ T S C r r [w ] prj1(S ,T )

dom(r) r B T p ; q prj2(S ,T )

ran(r) S C− r p C− q id(S)

r−1 r B− T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 70 / 89

A Quick Review of Set Theory Binary Relation Operators

Classical Results with Relation Operators

(r−1)−1 = r

dom(r−1) = ran(r)

(S C r)−1 = r−1 B S

(p ; q)−1 = q−1 ; p−1

(p ; q) ; r = p ; (q ; r)

(p ; q)[w ] = q[p[w ]]

p ; (q ∪ r) = (p ; q) ∪ (p ; r)

r [a ∪ b] = r [a] ∪ r [b]

. . .

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 71 / 89

A Quick Review of Set Theory Function Operators

Function Operators (1)

Partial functions: S 7→ T

Total functions: S → T

Partial injections: S 7 T

Total injections: S T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 72 / 89

A Quick Review of Set Theory Function Operators

A Partial Function F from a Set A to a Set BA Partial Function from a Set A to a Set B 102

A B

a3a2

a6

a7

b1

F

b3

b4

b5

b6

b2

a5

a1

a4

F A ✏ B

102

Definition: F ∈ A 7→ B ⇔ F ∈ A↔ B ∧ (F−1 ; F ) = id(ran(F ))

F = {a1 7→ b2, a3 7→ b4, a5 7→ b2, a7 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 73 / 89

A Quick Review of Set Theory Function Operators

A Total Function F from a Set A to a Set BA Total Function F from a Set A to a Set B 103

A B

a3a2

a6

a7

b1

F

b3

b4

b5

b6

b2

a5

a1

a4

F A B

103

Definition: F ∈ A→ B ⇔ F ∈ A 7→ B ∧ A = dom(F )

F = {a1 7→ b2, a2 7→ b1, a3 7→ b4, a4 7→ b5, a5 7→ b2, a6 7→ b5, a7 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 74 / 89

A Quick Review of Set Theory Function Operators

A Partial Injection F from a Set A to a Set BA Partial Injection F from a Set A to a Set B 104

A B

a3

a6

F

b4

b5

b6

b2

a1 b3

a5

a4

F A ✏⇢B

104

Definition: F ∈ A 7 B ⇔ F ∈ A 7→ B ∧ F−1 ∈ B 7→ A

F = {a1 7→ b2, a3 7→ b4, a6 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 75 / 89

A Quick Review of Set Theory Function Operators

A Total Injection F from a Set A to a Set BA Total Injection F from a Set A to a Set B 105

A B

a3

a6

F

b4

b5

b6

b2

a1 b3

F A⇢B

105

Definition: F ∈ A B ⇔ F ∈ A→ B ∧ F−1 ∈ B 7→ A

F = {a1 7→ b2, a3 7→ b4, a6 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 76 / 89

A Quick Review of Set Theory Function Operators

Function Operator Memberships (1)

Left part Right part

f ∈ S 7→ T f ∈ S ↔ T ∧ (f −1 ; f ) = id(ran(f ))

f ∈ S → T f ∈ S 7→ T ∧ S = dom(f )

f ∈ S 7 T f ∈ 7→ ∧ f −1 ∈ T 7→ S

f ∈ S T f ∈ S → T ∧ f −1 ∈ T 7→ S

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 77 / 89

A Quick Review of Set Theory Function Operators

Function Operators (2)

Partial surjections: S 7 T

Total surjections: S T

Bijections: S T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 78 / 89

A Quick Review of Set Theory Function Operators

A Partial Surjection F from a Set A to a Set BA P rtial Surjection from a Set A to a Set B 108

A B

a3

a6

F

b4

b6

b2

a1

a5

a4

a2

F A ✏⇣B

108

Definition: F ∈ A 7 B ⇔ F ∈ A 7→ B ∧ B = ran(F )

F = {a1 7→ b2, a3 7→ b4, a5 7→ b2, a6 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 79 / 89

A Quick Review of Set Theory Function Operators

A Total Surjection F from a Set A to a Set BA Total Surjection F from a Set A to a Set B 109

A B

a3

a6

F

b4

b6

b2

a1

a5

a4

a2

F A⇣B

109

Definition: F ∈ A B ⇔ F ∈ A→ B ∧ B = ran(F )

F = {a1 7→ b2, a3 7→ b4, a4 7→ b4, a5 7→ b2, a6 7→ b6, a2 7→ b2}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 80 / 89

A Quick Review of Set Theory Function Operators

A Total Bijection F from a Set A to a Set BA Bijection F from a Set A to a Set B 110

A B

a3

a6

F

b4

b5

b6

b2

a1 b3

a5

a4

F A⇢⇣B

110

Definition: F ∈ A B ⇔ F ∈ A B ∧ F ∈ A B

F = {a1 7→ b2, a3 7→ b4, a4 7→ b3, a5 7→ b5, a6 7→ b6}

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 81 / 89

A Quick Review of Set Theory Function Operators

Function Operator Memberships (1)

Left part Right part

f ∈ S 7 T f ∈ S 7→ T ∧ T = ran(f )

f ∈ S T f ∈ S → T ∧ T = ran(f )

f ∈ S T f ∈ S T ∧ f ∈ S T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 82 / 89

A Quick Review of Set Theory Function Operators

Summary of Function Operators

S 7→ T S 7 T

S → T S T

S 7 T S T

S T

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 83 / 89

A Quick Review of Set Theory Function Operators

Applying a Function

Given a partial function f , we have

Left part Right part

F = f (E ) E 7→ F ∈ f

Well-definedness condition: if f is a partial function, then E ∈ dom(f )

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 84 / 89

A Quick Review of Arithmetic

Outline

1 Reading: seL4

2 A Quick Review of Propositional Calculus

3 A Quick Review of First-order Predicate Calculus

4 A Quick Review of Set Theory

5 A Quick Review of Arithmetic

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 85 / 89

A Quick Review of Arithmetic

Arithmetic and Summary of Syntax (1)

predicate ::= ⊥

>

. . .

expression = expression

expression ∈ set

number < number

number ≤ number

number > number

number ≥ number

finite(set) . finiteness

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 86 / 89

A Quick Review of Arithmetic

Arithmetic and Summary of Syntax (2)

expression ::= variable

expression 7→ expression

set

number

variable ::= . . .

set ::= set × set

P(set)

{var list · predicate|expression}

Z . integers

N . natural numbers

number .. number . a set of integers

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 87 / 89

A Quick Review of Arithmetic

Arithmetic and Summary of Syntax (3)

number ::= 0

. . .

− number

number + number

number − number

number ∗ number

number/number

number mod number

number ̂ number

card(set) . set cardinality

min(set) . min element of a set

max(set) . max element of a set

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 88 / 89

A Quick Review of Arithmetic

Summary of the Well-definedness Conditions

Expression Condition

inter(S) S 6= ∅

f (E ) f is a partial function, E ∈ dom(f )

E/F F 6= 0

E mod F F 6= 0

card(S) finite(S)

min(S) S ⊆ Z ∧ ∃x · x ∈ Z ∧ (∀n · n ∈ S ⇒ x ≤ n)

max(S) S ⊆ Z ∧ ∃x · x ∈ Z ∧ (∀n · n ∈ S ⇒ x ≥ n)

Yuan-Fang Li, 2020 FIT5138 (part 2)—Discrete Maths Lecture 8 89 / 89