From 66d229c49305e4a0722f1df78aa22acf7ac06fc3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 21:51:53 -0700 Subject: [PATCH] Prove that multi-statement evaluation "preserves" the validity of the analysis Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 9983432..784fc99 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -230,3 +230,8 @@ module WithProg (prog : Program) where k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs' in ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁ + + updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂ + updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ + updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ = + updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)