From f6b347eb05542d423ade4bd62f2b438013a65735 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 1 Dec 2024 22:19:08 -0800 Subject: [PATCH] Fix slugs and add example of constant propagation Signed-off-by: Danila Fedorin --- content/blog/00_spa_agda_intro.md | 4 ++-- content/blog/08_spa_agda_forward/index.md | 4 ++++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md index cb9890c..b4c6dc4 100644 --- a/content/blog/00_spa_agda_intro.md +++ b/content/blog/00_spa_agda_intro.md @@ -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" >}} diff --git a/content/blog/08_spa_agda_forward/index.md b/content/blog/08_spa_agda_forward/index.md index f9bbaf1..3928e30 100644 --- a/content/blog/08_spa_agda_forward/index.md +++ b/content/blog/08_spa_agda_forward/index.md @@ -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" >}}).