blob: 8c6b45ac3c85ed9a66210f1a70a1ba31ff71be1a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Definition of Hoare triples
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
import Helium.Semantics.Core as Core
module Helium.Semantics.Axiomatic.Triple
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
(rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
(2≉0 : Core.2≉0 rawPseudocode)
where
private
open module C = RawPseudocode rawPseudocode
import Data.Bool as Bool
open import Data.Fin using (fromℕ; suc; inject₁)
open import Data.Fin.Patterns
open import Data.Nat using (ℕ; suc)
open import Data.Vec using (Vec; _∷_)
open import Data.Vec.Relation.Unary.All as All using (All)
open import Function using (_∘_)
open import Helium.Data.Pseudocode.Core
open import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Asrt
open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (↓_)
open import Level using (_⊔_; lift; lower) renaming (suc to ℓsuc)
open import Relation.Nullary.Decidable.Core using (toWitness)
open Term.Term
open Semantics 2≉0
private
variable
i j k m n : ℕ
t : Type
Σ Γ Δ ts : Vec Type n
P Q R S : Assertion Σ Γ Δ
ref : Reference Σ Γ t
e val : Expression Σ Γ t
es : All (Expression Σ Γ) ts
s s₁ s₂ : Statement Σ Γ
ℓ = b₁ ⊔ i₁ ⊔ r₁
infix 4 _⊆_
record _⊆_ (P : Assertion Σ Γ Δ) (Q : Assertion Σ Γ Δ) : Set ℓ where
constructor arr
field
implies : ∀ σ γ δ → ⟦ P ⟧ σ γ δ → ⟦ Q ⟧ σ γ δ
open _⊆_ public
data HoareTriple {Σ : Vec Type i} {Γ : Vec Type j} {Δ : Vec Type k} : Assertion Σ Γ Δ → Statement Σ Γ → Assertion Σ Γ Δ → Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁)) where
seq : ∀ Q → HoareTriple P s Q → HoareTriple Q s₁ R → HoareTriple P (s ∙ s₁) R
skip : P ⊆ Q → HoareTriple P skip Q
assign : subst P ref (↓ val) ⊆ Q → HoareTriple P (ref ≔ val) Q
declare : HoareTriple (Var.weaken 0F P ∧ equal (var 0F) (Term.Var.weaken 0F (↓ e))) s (Var.weaken 0F Q) → HoareTriple P (declare e s) Q
invoke : ∀ (Q R : Assertion Σ ts Δ) → P ⊆ Var.elimAll Q (All.map ↓_ es) → HoareTriple Q s R → Var.inject Γ R ⊆ Var.raise ts S → HoareTriple P (invoke (s ∙end) es) S
if : HoareTriple (P ∧ pred (↓ e)) s Q → P ∧ pred (↓ inv e) ⊆ Q → HoareTriple P (if e then s) Q
if-else : HoareTriple (P ∧ pred (↓ e)) s Q → HoareTriple (P ∧ pred (↓ inv e)) s Q → HoareTriple P (if e then s) Q
for : ∀ (I : Assertion _ _ (fin _ ∷ _)) → P ⊆ Meta.elim 0F I (↓ lit 0F) → HoareTriple {Δ = fin _ ∷ Δ} (Var.weaken 0F (Meta.elim 1F (Meta.weaken 0F I) (fin inject₁ (cons (meta 0F) nil)))) s (Var.weaken 0F (Meta.elim 1F (Meta.weaken 0F I) (fin suc (cons (meta 0F) nil)))) → Meta.elim 0F I (↓ lit (fromℕ m)) ⊆ Q → HoareTriple P (for m s) Q
some : HoareTriple P s Q → HoareTriple (some P) s (some Q)
|
