Start end-to-end proof of correctness
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
4ac9dffa9b
commit
838aaf9c58
|
@ -80,6 +80,7 @@ module WithProg (prog : Program) where
|
||||||
renaming
|
renaming
|
||||||
( FiniteMap to StateVariables
|
( FiniteMap to StateVariables
|
||||||
; isLattice to isLatticeᵐ
|
; isLattice to isLatticeᵐ
|
||||||
|
; _≈_ to _≈ᵐ_
|
||||||
; _∈k_ to _∈kᵐ_
|
; _∈k_ to _∈kᵐ_
|
||||||
; locate to locateᵐ
|
; locate to locateᵐ
|
||||||
; _≼_ to _≼ᵐ_
|
; _≼_ to _≼ᵐ_
|
||||||
|
@ -92,6 +93,11 @@ module WithProg (prog : Program) where
|
||||||
renaming
|
renaming
|
||||||
( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
|
( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
|
||||||
)
|
)
|
||||||
|
open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
|
||||||
|
using ()
|
||||||
|
renaming
|
||||||
|
( ≈-sym to ≈ᵐ-sym
|
||||||
|
)
|
||||||
|
|
||||||
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
|
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
|
||||||
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
|
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
|
||||||
|
@ -107,6 +113,9 @@ module WithProg (prog : Program) where
|
||||||
variablesAt : State → StateVariables → VariableValues
|
variablesAt : State → StateVariables → VariableValues
|
||||||
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
|
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
|
||||||
|
|
||||||
|
variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
|
||||||
|
variablesAt-≈ = {!!}
|
||||||
|
|
||||||
-- build up the 'join' function, which follows from Exercise 4.26's
|
-- build up the 'join' function, which follows from Exercise 4.26's
|
||||||
--
|
--
|
||||||
-- L₁ → (A → L₂)
|
-- L₁ → (A → L₂)
|
||||||
|
@ -270,3 +279,14 @@ module WithProg (prog : Program) where
|
||||||
updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
|
updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
|
||||||
updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
|
updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
|
||||||
updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
|
updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
|
||||||
|
|
||||||
|
walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
|
||||||
|
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
|
||||||
|
let
|
||||||
|
-- I'd use rewrite, but Agda gets a memory overflow (?!).
|
||||||
|
⟦joinAll-result⟧ρ₁ = subst (λ vs → ⟦ vs ⟧ᵛ ρ₁) (sym (variablesAt-joinAll s₁ result)) ⟦joinForKey-s₁⟧ρ₁
|
||||||
|
⟦analyze-result⟧ρ₂ = updateAll-matches {sv = joinAll result} ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
|
||||||
|
analyze-result≈result = ≈ᵐ-sym {result} {updateAll (joinAll result)} result≈analyze-result
|
||||||
|
analyze-s₁≈s₁ = variablesAt-≈ s₁ (updateAll (joinAll result)) result (analyze-result≈result)
|
||||||
|
in
|
||||||
|
⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂
|
||||||
|
|
|
@ -2,6 +2,7 @@ module Language where
|
||||||
|
|
||||||
open import Language.Base public
|
open import Language.Base public
|
||||||
open import Language.Semantics public
|
open import Language.Semantics public
|
||||||
|
open import Language.Traces public
|
||||||
open import Language.Graphs public
|
open import Language.Graphs public
|
||||||
open import Language.Properties public
|
open import Language.Properties public
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user