1
Software System Design and Implementation
Introduction
Dr. Christine Rizkallah
UNSW Term 2 2021
Who are we?
2
I am Dr. Christine Rizkallah, currently a lecturer at UNSW. I lead the Cogent team and my research specialty involves formal methods and programming languages for building reliable software.
Who are we?
3
I am Dr. Christine Rizkallah, currently a lecturer at UNSW. I lead the Cogent team and my research specialty involves formal methods and programming languages for building reliable software.
Curtis Millar, is a UNSW academic who works on, among other things, projects involving trustworthy systems and formal methods.
Who are we?
4
I am Dr. Christine Rizkallah, currently a lecturer at UNSW. I lead the Cogent team and my research specialty involves formal methods and programming languages for building reliable software.
Curtis Millar, is a UNSW academic who works on, among other things, projects involving trustworthy systems and formal methods.
Credits
5
We thank the former lecturers of this course for developing and continuously refining this course material. The course material offered greatly benefits from their contributions.
Dr. Liam O’Connor, who now a lecturer at the University of Edinburgh, and whose research involves programming languages for trustworthy systems.
Prof. Gabriele Keller, who now works at Utrecht University, and whose research expertise is on programming languages for formal methods and high performance computing.
Prof. Manuel Charkavarty, who now works at IOHK with a focus on research and development of programming languages and compilers for functional programming.
Contacting Us
Forum
http://www.cse.unsw.edu.au/~cs3141
There is a Discourse forum available on the website. Questions about course content should typically be made there. You can ask us private questions to avoid spoiling solutions to other students.
Administrative questions should be sent to cs3141@cse.unsw.edu.au. 6
What is this course?
Software must be high quality: Software must developed
correct, safe and secure. cheaply and quickly
7
Safety-uncritical Applications
8
; Video games: Some bugs are acceptable, to save developer effort.
9
Safety-critical Applications
Remember a particularly painful uni group work assignment.
Safety-critical Applications
Remember a particularly painful uni group work assignment.
Now imagine you. . .
Are travelling on a plane
Are travelling in a self-driving car
Are working on a Mars probe
Have invested in a new hedge fund
Are running a cryptocurrency exchange
Are getting treatment from a radiation therapy machine Intend to launch some nuclear missiles at your enemies
. . . running on software written by the person next to you on the participant list. 10
Safety-critical Applications
11
What is this course?
12
Maths COMP3141 Software
Maths?
Logic
Set Theory Proofs Induction Algebra (a bit) No calculus
Maths COMP3141 Software
What is this course?
13
N.B: MATH1081 is neither necessary nor sufficient for COMP3141.
Software?
Programming Reasoning Design Testing Types Haskell
Maths COMP3141 Software
What is this course?
14
N.B: Haskell knowledge is not a prerequisite for COMP3141.
15
This course is not:
a Haskell course
What isn’t this course?
16
This course is not:
a Haskell course
What isn’t this course?
a verification course (for that, see COMP6721, COMP4161)
17
This course is not:
a Haskell course
What isn’t this course?
a verification course (for that, see COMP6721, COMP4161) an OOP software design course (see COMP2511, COMP1531)
18
This course is not:
a Haskell course
What isn’t this course?
a verification course (for that, see COMP6721, COMP4161) an OOP software design course (see COMP2511, COMP1531) a programming languages course (see COMP3161).
19
This course is not:
a Haskell course
What isn’t this course?
a verification course (for that, see COMP6721, COMP4161) an OOP software design course (see COMP2511, COMP1531) a programming languages course (see COMP3161).
a WAM booster cakewalk (hopefully).
a soul-destroying nightmare (hopefully).
Warning
Assessment
For many of you, this course will present a lot of new topics. Even if you are a seasoned programmer, you may have to learn as if from scratch.
20
Warning
Assessment
For many of you, this course will present a lot of new topics. Even if you are a seasoned programmer, you may have to learn as if from scratch.
Class Mark (out of 100)
Two programming assignments, each worth 20 marks.
Weekly online quizzes, worth 20 marks.
Weekly programming exercises, worth 40 marks.
Final Exam Mark (out of 100)
This includes 10 marks for active participation throughout the term. You will be
provided with various methods and opportunities to demonstrate participation
throughout the term.
result = class + exam 2
21
22
Lectures
The lectures will be held on zoom. As there is a limit of 300 attendees on zoom, we will live stream the lectures to YouTube, in case we hit the zoom limit.
I, Christine, or someone qualified whom I nominate, will run lectures introducing new material on Wednesdays.
Curtis will reinforce this new material with questions and examples on Fridays.
Curtis has kindly agreed to offer three help sessions throughout the term. The dates and times for these sessions will be announced at least one week in advance on the course website.
You must attend lectures or watch recordings as they come out. Recordings will be available from the course website.
Online quizzes are due one week after the lectures they examine, but do them early!
Books
23
There are no set textbooks for this course, however, there are various books that are useful for learning Haskell listed on the course website.
I can also provide more specialised text recommendations for specific topics.
Haskell
In this course we use Haskell, because it is the most widespread language with good support for mathematically structured programming.
f ::Int -> Bool
Function Name
Haskell
In this course we use Haskell, because it is the most widespread language with good support for mathematically structured programming.
“of type”
f ::Int -> Bool
Function Name
Haskell
In this course we use Haskell, because it is the most widespread language with good support for mathematically structured programming.
“of type”
f ::Int -> Bool
Function Name Domain
Haskell
In this course we use Haskell, because it is the most widespread language with good support for mathematically structured programming.
“of type” Codomain
f ::Int -> Bool
Function Name Domain
27
Haskell
In this course we use Haskell, because it is the most widespread language with good support for mathematically structured programming.
f ::Int -> Bool
f x = (x > 0)
Input Output
28
Haskell
In this course we use Haskell, because it is the most widespread language with good support for mathematically structured programming.
f ::Int -> Bool
f x = (x > 0)
Input Output
In mathematics, we would apply a function by writing f (x ). In Haskell we write f x. Demo: GHCi, basic functions
29
30
Currying
In mathematics, we treat log10(x) and log2(x) and ln(x) as separate functions.
In Haskell, we have a single function logBase that, given a number n, produces a function for logn(x).
log10 :: Double -> Double log10 = logBase 10
log2 :: Double -> Double log2 = logBase 2
ln :: Double -> Double
ln = logBase 2.71828 What’s the type of logBase?
Currying and Partial Application
31
logBase :: Double -> (Double -> Double) (parentheses optional above)
Currying and Partial Application
32
logBase :: Double -> (Double -> Double) (parentheses optional above)
Function application associates to the left in Haskell, so: logBase 2 64 ≡ (logBase 2) 64
Currying and Partial Application
33
logBase :: Double -> (Double -> Double) (parentheses optional above)
Function application associates to the left in Haskell, so: logBase 2 64 ≡ (logBase 2) 64
Functions of more than one argument are usually written this way in Haskell, but it is possible to use tuples instead…
Tuples
34
Tuples are another way to take multiple inputs or produce multiple outputs:
toCartesian :: (Double, Double) -> (Double, Double) toCartesian (r, theta) = (x, y)
where x = r * cos theta y = r * sin theta
N.B: The order of bindings doesn’t matter. Haskell functions have no side effects, they just return a result.
Higher Order Functions
35
In addition to returning functions, functions can take other functions as arguments:
twice :: (a -> a) -> (a -> a) twice f a = f (f a)
double :: Int -> Int double x = x * 2
quadruple :: Int -> Int quadruple = twice double
Lists
36
Haskell makes extensive use of lists, constructed using square brackets. Each list element must be of the same type.
[True, False, True]
[3, 2, 5+1]
[sin, cos]
[ (3,’a’),(4,’b’) ]
:: [Bool]
:: [Int]
:: [Double -> Double] :: [(Int, Char)]
Map
37
A useful function is map, which, given a function, applies it to each element of a list:
map not [True, False, True] = [False, True, False] map negate [3, -2, 4] = [-3, 2, -4]
map (\x -> x + 1) [1, 2, 3] = [2, 3, 4]
Map
38
A useful function is map, which, given a function, applies it to each element of a list:
map not [True, False, True] = [False, True, False] map negate [3, -2, 4] = [-3, 2, -4]
map (\x -> x + 1) [1, 2, 3] = [2, 3, 4]
The last example here uses a lambda expression to define a one-use function without giving it a name.
What’s the type of map?
Map
A useful function is map, which, given a function, applies it to each element of a list:
map not [True, False, True] = [False, True, False] map negate [3, -2, 4] = [-3, 2, -4]
map (\x -> x + 1) [1, 2, 3] = [2, 3, 4]
The last example here uses a lambda expression to define a one-use function without giving it a name.
What’s the type of map?
map :: (a -> b) -> [a] -> [b] 39
Strings
40
The type String in Haskell is just a list of characters: type String = [Char]
This is a type synonym, like a typedef in C.
Thus:
“hi!” == [‘h’, ‘i’, ‘!’]
Word Frequencies
Let’s solve a problem to get some practice:
Example (First Demo Task)
Given a number n and a string s, generate a report (in String form) that lists the n most common words in the string s.
41
Word Frequencies
Let’s solve a problem to get some practice:
Example (First Demo Task)
Given a number n and a string s, generate a report (in String form) that lists the n most common words in the string s.
We must:
1 Break the input string into words.
2 Convert the words to lowercase.
3 Sort the words.
4 Count adjacent runs of the same word.
5 Sort by size of the run.
6 Take the first n runs in the sorted list.
7 Generate a report.
42
Function Composition
43
We used function composition to combine our functions together. The mathematical (f ◦ g)(x) is written (f . g) x in Haskell.
In Haskell, operators like function composition are themselves functions. You can define your own!
— Vector addition
(.+) :: (Int, Int) -> (Int, Int) -> (Int, Int) (x1, y1) .+ (x2, y2) = (x1 + x2, y1 + y2)
(2,3) .+ (1,1) == (3,4)
Function Composition
44
We used function composition to combine our functions together. The mathematical (f ◦ g)(x) is written (f . g) x in Haskell.
In Haskell, operators like function composition are themselves functions. You can define your own!
— Vector addition
(.+) :: (Int, Int) -> (Int, Int) -> (Int, Int) (x1, y1) .+ (x2, y2) = (x1 + x2, y1 + y2)
(2,3) .+ (1,1) == (3,4)
You could even have defined function composition yourself if it didn’t already exist:
(.) :: (b -> c) -> (a -> b) -> (a -> c) (f . g) x = f (g x)
Lists
45
How were all of those list functions we just used implemented?
Lists
46
How were all of those list functions we just used implemented?
Lists are singly-linked lists in Haskell. The empty list is written as [] and a list node is written as x : xs. The value x is called the head and the rest of the list xs is called the tail. Thus:
“hi!” == [‘h’, ‘i’, ‘!’] == ‘h’:(‘i’:(‘!’:[])) == ‘h’ : ‘i’ : ‘!’ : []
Lists
47
How were all of those list functions we just used implemented?
Lists are singly-linked lists in Haskell. The empty list is written as [] and a list node is written as x : xs. The value x is called the head and the rest of the list xs is called the tail. Thus:
“hi!” == [‘h’, ‘i’, ‘!’] == ‘h’:(‘i’:(‘!’:[])) == ‘h’ : ‘i’ : ‘!’ : []
When we define recursive functions on lists, we use the last form for pattern matching:
map :: (a -> b) -> [a] -> [b] map f [] = []
map f (x:xs) = f x : map f xs
Equational Evaluation
48
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
Equational Evaluation
49
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!” ≡ map toUpper (‘h’:”i!”)
Equational Evaluation
50
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!” ≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
Equational Evaluation
51
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!” ≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
Equational Evaluation
52
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!” ≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
Equational Evaluation
53
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
≡ ‘H’ : toUpper ‘i’ : map toUpper “!”
Equational Evaluation
54
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
≡ ‘H’ : toUpper ‘i’ : map toUpper “!” ≡ ‘H’ : ‘I’ : map toUpper “!”
Equational Evaluation
55
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
≡ ‘H’ : toUpper ‘i’ : map toUpper “!” ≡ ‘H’ : ‘I’ : map toUpper “!”
≡ ‘H’ : ‘I’ : map toUpper (‘!’:””)
Equational Evaluation
56
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
≡ ‘H’ : toUpper ‘i’ : map toUpper “!” ≡ ‘H’ : ‘I’ : map toUpper “!”
≡ ‘H’ : ‘I’ : map toUpper (‘!’:””)
≡ ‘H’:’I’:’!’:maptoUpper””
Equational Evaluation
57
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
≡ ‘H’ : toUpper ‘i’ : map toUpper “!” ≡ ‘H’ : ‘I’ : map toUpper “!”
≡ ‘H’ : ‘I’ : map toUpper (‘!’:””)
≡ ‘H’:’I’:’!’:maptoUpper””
≡ ‘H’:’I’:’!’:maptoUpper[]
Equational Evaluation
58
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
≡ ‘H’ : toUpper ‘i’ : map toUpper “!” ≡ ‘H’ : ‘I’ : map toUpper “!”
≡ ‘H’ : ‘I’ : map toUpper (‘!’:””)
≡ ‘H’:’I’:’!’:maptoUpper””
≡ ‘H’:’I’:’!’:maptoUpper[]
≡ ‘H’:’I’:’!’:[]
Equational Evaluation
59
map f [] = []
map f (x:xs) = f x : map f xs We can evaluate programs equationally:
map toUpper “hi!”
≡ map toUpper (‘h’:”i!”)
≡ toUpper ‘h’ : map toUpper “i!”
≡ ‘H’ : map toUpper “i!”
≡ ‘H’ : map toUpper (‘i’:”!”)
≡ ‘H’ : toUpper ‘i’ : map toUpper “!” ≡ ‘H’ : ‘I’ : map toUpper “!”
≡ ‘H’ : ‘I’ : map toUpper (‘!’:””)
≡ ‘H’:’I’:’!’:maptoUpper””
≡ ‘H’:’I’:’!’:maptoUpper[]
≡ ‘H’:’I’:’!’:[]
≡ “HI!”
60
Higher Order Functions
The rest of this lecture will be spent introducing various list functions that are built into Haskell’s standard library by way of live coding.
Functions to cover:
1 map
2 filter
3 concat
4 sum
5 foldr
6 foldl
In the process, we will introduce let and case syntax, guards and if, and the $ operator.
61
Homework
1 Get Haskell working on your development environment. Instructions are on the course website.
2 Using Haskell documentation and GHCi, answer the questions in this week’s quiz (assessed!).
3 Attend Curtis’ online lecture on Friday!