Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix slugs and add example of constant propagation

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-12-01 22:19:08 -08:00
parent c1b27a13ae
commit f6b347eb05
2 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
content/blog/00_spa_agda_intro.md
View File

@ -106,5 +106,5 @@ Here are the posts that I’ve written so far for this series:
* {{< draftlink "Our Programming Language" "05_spa_agda_semantics" >}}
* {{< draftlink "Control Flow Graphs" "06_spa_agda_cfg" >}}
* {{< draftlink "Connecting Semantics and Control Flow Graphs" "07_spa_agda_semantics_and_cfg" >}}
* {{< draftlink "Forward Analysis" "08_spa_forward" >}}
* {{< draftlink "Verifying the Forward Analysis" "09_spa_verified_forward" >}}
* {{< draftlink "Forward Analysis" "08_spa_agda_forward" >}}
* {{< draftlink "Verifying the Forward Analysis" "09_spa_agda_verified_forward" >}}

4
content/blog/08_spa_agda_forward/index.md
View File

@ -415,6 +415,10 @@ plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ
we can defined a constant-propagation analysis.
```
{"neg" ↦ -1, "pos" ↦ 1, "unknown" ↦ 0, "zero" ↦ 0, }
```
However, we haven't proved our analysis correct, and we haven't yet made use of
the CFG-semantics equivalence that we
[proved in the previous section]({{< relref "07_spa_agda_semantics_and_cfg" >}}).