lectures.alex.balgavy.eu

commit 87a0d873c79055e49efc369911cfb202ff6c5bfa
parent 0c9993eb9c5e3a62245d405d5f0ec78c0eff23cb
Author: Alex Balgavy <alex@balgavy.eu>
Date:   Wed, 16 Dec 2020 16:58:53 +0100

Finalized lecture notes for this period

Diffstat:
M
content/logical-verification/Hoare Logic.md
 | 
2
--
M
content/logical-verification/_index.md
 | 
1
-
M
content/software-architecture/Introduction/index.md
 | 
1
-

3 files changed, 0 insertions(+), 4 deletions(-)
diff --git a/content/logical-verification/Hoare Logic.md b/content/logical-verification/Hoare Logic.md
@@ -17,8 +17,6 @@ Examples:
 {b ≥ 5} b := b + 1 {b ≥ 6}
 ```
 
-## Hoare rules
-
 ## Semantic approach to Hoare Logic
 We can define Hoare triples semantically in Lean.
 Use predicates on states (`state → Prop`) to represent pre and postconditions.
diff --git a/content/logical-verification/_index.md b/content/logical-verification/_index.md
@@ -45,7 +45,6 @@ There is a [Git repository](https://github.com/blanchette/logical_verification_2
     - [Properties of small-step semantics](operational-semantics#properties-of-small-step-semantics)
 - [Hoare logic](hoare-logic)
     -  [Hoare triples](hoare-logic#hoare-triples)
-    -  [Hoare rules](hoare-logic#hoare-rules)
     -  [Semantic approach to Hoare Logic](hoare-logic#semantic-approach-to-hoare-logic)
     -  [Verification condition generator](hoare-logic#verification-condition-generator)
     -  [Hoare triples for total correctness](hoare-logic#hoare-triples-for-total-correctness)
diff --git a/content/software-architecture/Introduction/index.md b/content/software-architecture/Introduction/index.md
@@ -1,7 +1,6 @@
 +++
 title = 'Introduction'
 +++
-
 # Introduction
 What is software architecture?
 - fundamental concepts/properties of system in its environment