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 Oper
ators ∧, ∨ 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 Theor
y 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 r 1 = {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 Oper
ator 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 Arithme
tic 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
