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