commit c2fab7f260f7a290ffc497f43b74571529ec8e2c
parent 53950e129904c31cb495eada32dd855d46f30003
Author: Alex Balgavy <alex@balgavy.eu>
Date: Wed, 4 Nov 2020 21:43:56 +0100
Update current lecture notes
Diffstat:
8 files changed, 202 insertions(+), 0 deletions(-)
diff --git a/content/logical-verification/Functional programming.md b/content/logical-verification/Functional programming.md
@@ -0,0 +1,115 @@
++++
+title = 'Functional programming'
++++
+# Functional programming
+## Inductive types
+Mottoes:
+- no junk: type contains no values except those expressible using constructors
+ - e.g. for `nat`, there aren't values that can't be expressed using finite combination of `zero` and `succ`
+- no confusion: values built in different ways are different
+ - e.g. for `nat`, `zero` ≠ `succ x`
+
+## Structural induction
+generalization of math induction to inductive types.
+- to prove property `P[n]` for natural numbers `n`, prove:
+ - base case `P[0]`
+ - induction step `∀k, P[k] → P[k+1]`
+- similarly for lists:
+ - base case `P[[]]`
+ - induction step `∀y ys, P[ys] → P[y :: ys]`
+
+Example proof:
+
+```lean
+lemma nat.succ_neq_self (n : Ν) :
+ nat.succ n ≠ n :=
+begin
+ induction' n,
+ { simp },
+ { simp [ih] }
+end
+```
+
+You can use `case` to supply custom names and/or reorder cases.
+
+## Structural recursion
+Form of recursion where you can peel off constructors from value.
+Hence only call themselves finitely many times.
+
+Example:
+
+```lean
+def fact : Ν → Ν
+| 0 := 1
+| (n+1) := (n+1) * fact n
+```
+
+## Pattern matching
+`match` lets you do nonrecursive pattern matching
+
+```
+match term_1, term_2, ..., term_n with
+| pattern_1, ..., pattern_m := result_1
+...
+| pattern_k1, ..., pattern_km := result_k
+end
+```
+
+## Structures
+You can define records/structures, essentially nonrecursive single-constructor inductive types.
+
+```lean
+structure rgb := (red green blue : Ν)
+def red : rgb :=
+{ red := 0xff,
+ green := 0x00,
+ blue := 0x00 }
+
+structure rgba extends rgb := (alpha : Ν)
+def semitransparent_red : rgba :=
+{ alpha := 0x7f,
+ ..pure_red }
+```
+
+`cases` does a case distinction on a term, giving rise to as many subgoals as constructors in definition of term's type.
+
+
+## Type classes
+Structure type combining abstract constants and their properties.
+Type can be declared instance of type class by (1) providing concrete definitions for constants and (2) proving that properties hold.
+
+for example, for class:
+
+```lean
+class inhabited (α : Sort u) := (default [] : α)
+```
+
+you can declare an instance like this:
+
+```lean
+@[instance] def nat.inhabited : inhabited Ν := { default := 0 }
+
+@[instance] def list.inhabited : {α : Type} : inhabited (list α) := { default := [] }
+```
+
+## Lists
+Inductive polymorphic types constructed from `nil` and `cons`.
+
+`cases'` can be used on hypothesis of form `l = r`. Matches `r` against `l`, replaces all occurrences of vars in `r` with corresponding terms in `l` globally across goal.
+it can also do case distinction on proposition, yielding one subgoal where the prop is true, and one where it's false.
+
+`list.map` applies function element-wise to list.
+`list.tail` gets everything but first element.
+`list.head` gets first element.
+`list.zip` takes two lists, and creates list of pairs.
+`list.length` returns number of elements.
+
+## Binary trees
+Inductive types with constructors taking recursive arguments.
+Have nodes with max two children.
+
+```lean
+inductive btree (α : Type) : Type
+| empty {} : btree
+| node : α → btree → btree → btree
+```+
\ No newline at end of file
diff --git a/content/logical-verification/_index.md b/content/logical-verification/_index.md
@@ -10,3 +10,4 @@ There is a [Git repository](https://github.com/blanchette/logical_verification_2
- [Basics](basics)
- [Backward proofs](backward-proofs/)
- [Forward proofs](forward-proofs/)
+- [Functional programming](functional-programming/)
diff --git a/content/software-architecture/Requirements/02efe4c6962a45acb18af0a8190c0eba.png b/content/software-architecture/Requirements/02efe4c6962a45acb18af0a8190c0eba.png
Binary files differ.
diff --git a/content/software-architecture/Requirements/9db20224d3104417a9bc0658af70d85e.png b/content/software-architecture/Requirements/9db20224d3104417a9bc0658af70d85e.png
Binary files differ.
diff --git a/content/software-architecture/Requirements/c38c9e7dc12745b580ec4a2b3bcb60fe.png b/content/software-architecture/Requirements/c38c9e7dc12745b580ec4a2b3bcb60fe.png
Binary files differ.
diff --git a/content/software-architecture/Requirements/e93dae14295c4b9ea44923fadf19695c.png b/content/software-architecture/Requirements/e93dae14295c4b9ea44923fadf19695c.png
Binary files differ.
diff --git a/content/software-architecture/Requirements/index.md b/content/software-architecture/Requirements/index.md
@@ -0,0 +1,84 @@
++++
+title = 'Requirements'
++++
+# Requirements
+## Types of requirements
+- Functional requirements
+ - what the system must do, how to react to runtime events
+ - satisfied by assigning appropriate seq of responsibilities throughout design
+- Quality attribute requirements
+ - qualifications of functional requirements, e.g. how fast something must be done
+ - satisfied by structures designed into architecture, and behaviors/interactions of elements in those structures
+- Constraints
+ - design decisions where you have no freedom, e.g. using a certain programming language or reusing certain module
+ - satisfied by dealing with it (in fancy language, "reconciling the design decision with other affected design decisions")
+
+Neither functions nor quality attributes stand on their own
+
+Two categories of quality attributes:
+- development time qualities
+- runtime qualities
+
+## Architecturally significant requirements
+Architectures mostly driven by quality attribute requirements, features/functionality not as much
+Something like "the system must be modular" isn't enough; what's the reason? Has to be quantified and specific.
+
+Finding ASRs:
+- requirements documents (but often little info, architecture can't wait for requirements to be finished)
+- interviewing stakeholders (tells you what they want, but often they have no idea, and you might get random numbers from them)
+- understanding business goals (often lead to quality attribute requirements, may directly affect architecture)
+
+## Business goals
+Business goals often lead to QA requirements, may directly affect architecture.
+Some may be satisfied without using the architecture (e.g. to reduce cost, stop heating the offices when everyone's working from home)
+
+There are some standard categories, e.g. meeting financial/personal objectives, meeting responsibility to employees/society/state/shareholders, managing market position, managing change in environmental factors
+
+Expressing business goals:
+
+> "For {system being developed}, {goal subject} desires that {goal object} achieve {goal} (in the context of {environment}) and will be satisfied if {goal measure}."
+
+## Requirements and goals
+Goals are the "why", requirements are the "how".
+
+
+
+## Quality attribute scenarios
+Specifies quality-attribute-specific requirement.
+
+Six parts:
+1. stimulus: event arriving at system (input)
+2. Source of stimulus
+3. Response of system (output)
+4. Response measure - how you determine that response is satisfactory
+5. Environment - conditions when stimulus happens
+6. Artefact - which portions of system does requirement apply to
+
+
+
+## Capturing ASRs in utility tree
+Utility as root (expression of overall 'goodness' of system).
+Elaborated into QAs, decomposed into attribute refinements, expressed in ASRs (usually as QA scenarios)
+
+For example:
+
+
+
+Assess the ASRs in terms of business impact and architectural impact (high, medium, low):
+
+
+
+Checks based on utility tree:
+- have all QAs been refined and expressed in ASRs?
+- where are the risks? (H,H) ratings
+- are all concerns addressed?
+
+## Usability
+How easy it is for user to accomplish tasks, what support system provides for user.
+
+Dimensions:
+- learning features
+- using it efficiently
+- minimizing impact of errors
+- adapting to user's needs
+- increasing confidence and satisfaction
diff --git a/content/software-architecture/_index.md b/content/software-architecture/_index.md
@@ -4,3 +4,4 @@ title = 'Software Architecture'
# Software Architecture
- [Case Study Overview](case-study/)
- [Introduction](introduction/)
+- [Requirements](requirements/)
