# HG changeset patch # User Shinji KONO # Date 1680907781 -32400 # Node ID e152d7afbb58f979e21549fb4a85381c3c39d6cb # Parent 4c93248d5ec6aece518ab137d5d8cc8586da4575 add readme diff -r 4c93248d5ec6 -r e152d7afbb58 Readme.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Readme.md Sat Apr 08 07:49:41 2023 +0900 @@ -0,0 +1,145 @@ +-title: Hoare Logic + +-- files + + Hoare.agda Hoare logic data structre + HoareSoundness.agda Hoare logic soundness + RelOp.agda Set theoretic operation + whileTestPrim.agda definition of simple program and conditions as a Hoare logic command + whileTestPrimProof.agda proof using HoareSoundness + + whileTestGears.agda Gears form of proof + simple.agda + utilities.agda + +-- Hoare logic Programm commands + + data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm -> Comm + Seq : Comm -> Comm -> Comm + If : Cond -> Comm -> Comm -> Comm + While : Cond -> Comm -> Comm + +-- Example + + record Env : Set where + field + varn : ℕ + vari : ℕ + + program : ℕ → Comm + program c10 = + Seq ( PComm (λ env → record env {varn = c10})) --- n = c10 ; + $ Seq ( PComm (λ env → record env {vari = 0})) --- i = 0 ; + $ While (λ env → lt zero (varn env ) ) --- while ( 0 < n ) { + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) --- i = i + 1 + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) --- n = n - 1 } + +This is a syntax tree of a program. + +-- Interpretation of the example + + {-# TERMINATING #-} + interpret : Env → Comm → Env + interpret env Skip = env + interpret env Abort = env + interpret env (PComm x) = x env + interpret env (Seq comm comm1) = interpret (interpret env comm) comm1 + interpret env (If x then else) with x env + ... | true = interpret env then + ... | false = interpret env else + interpret env (While x comm) with x env + ... | true = interpret (interpret env comm) (While x comm) + ... | false = env + +-- Hoare logic Programm commands with Post and Pre conditions + +A syntax tree of a program with conditions. + + data HTProof : Cond -> Comm -> Cond -> Set where + PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> + (pr : Axiom bPre pcm bPost) -> + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) -> HTProof b Skip b + AbortRule : (bPre : Cond) -> (bPost : Cond) -> + HTProof bPre Abort bPost + WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> + {bPost' : Cond} -> {bPost : Cond} -> + Tautology bPre bPre' -> + HTProof bPre' cm bPost' -> + Tautology bPost' bPost -> + HTProof bPre cm bPost + SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> + {cm2 : Comm} -> {bPost : Cond} -> + HTProof bPre cm1 bMid -> + HTProof bMid cm2 bPost -> + HTProof bPre (Seq cm1 cm2) bPost + IfRule : {cmThen : Comm} -> {cmElse : Comm} -> + {bPre : Cond} -> {bPost : Cond} -> + {b : Cond} -> + HTProof (bPre and b) cmThen bPost -> + HTProof (bPre and neg b) cmElse bPost -> + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> + HTProof (bInv and b) cm bInv -> + HTProof bInv (While b cm) (bInv and neg b) + +-- Example of proposition + + proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) + proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + +This defines a connected sequence of conditions. + +-- Semantics of commands + + SemComm : Comm -> Rel State (Level.zero) + SemComm Skip = RelOpState.deltaGlob + SemComm Abort = RelOpState.emptyRel + SemComm (PComm pc) = PrimSemComm pc + SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) + SemComm (If b c1 c2) + = RelOpState.union + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm c1)) + (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm c2)) + SemComm (While b c) + = RelOpState.unionInf + (λ (n : ℕ) -> + RelOpState.comp (RelOpState.repeat n + (RelOpState.comp (RelOpState.delta (SemCond b)) (SemComm c))) (RelOpState.delta (NotP (SemCond b)))) + +This defines a proposition of Hoare conditions. It is not proved yet. + +The semantics of while-command is defined as any countable sequence of the body. + +-- Soundness + + Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost + +The proof of the soundness of the semantics of HTProof. + +-- An example of the soundness + + proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) + + PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost + PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht + + proofOfProgram : (c10 : ℕ) → (input output : Env ) + → initCond input ≡ true + → (SemComm (program c10) input output) + → termCond {c10} output ≡ true + proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem + diff -r 4c93248d5ec6 -r e152d7afbb58 ReadmeGears.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ReadmeGears.md Sat Apr 08 07:49:41 2023 +0900 @@ -0,0 +1,70 @@ +-title: GearsAgda + +-- files + + whileTestGears.agda Gears form of proof + +-- Continuation form makes Hoare logic simple + +Write a program in Gears form, which is a lightweight continuation style. + + code : {t : Set} -> (next : t -> t ) -> t + +-- Gears version of a program + + record Env : Set where + field + varn : ℕ + vari : ℕ + open Env + + {-# TERMINATING #-} + whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t + whileLoop env next with lt 0 (varn env) + whileLoop env next | false = next env + whileLoop env next | true = + whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next + +We need TERMINATING, because Agda does not understand the termination. + +-- A Segmented code gear with a condition + + whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) + → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) -- next with PostCondition + → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t + +It includes a reduction sequence "varn e1 < varn env → t)". + +The invariant is directly described in the program, we don't need sytax tree of a code nor a code with conditions. + +-- Specification + + whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ + whileTestSpec1 _ _ x = tt + +This is the condition to be proved. + +-- while loop in GearsAgda + + TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) + → (r : Index) → (p : Invraiant r) → t + +TerminatingLoopS defines a loop connective, which define the loop and it also gives a correctness of exit condition. + + whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t + + conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t + + proofGearsTermS : {c10 : ℕ } → ⊤ + proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → + TerminatingLoopS Env (λ env → varn env) + (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) + +This a proof, because it is a value not a type. whileTestSpec get a proof of specification. + + + + + diff -r 4c93248d5ec6 -r e152d7afbb58 Todo --- a/Todo Tue Nov 02 07:30:50 2021 +0900 +++ b/Todo Sat Apr 08 07:49:41 2023 +0900 @@ -1,3 +1,7 @@ +Sat Apr 8 07:48:50 JST 2023 + + Invariant と 実際の入力をわけない + Sun Dec 16 07:32:06 JST 2018 Gears の方に term condition を入れる diff -r 4c93248d5ec6 -r e152d7afbb58 whileTestGears.agda --- a/whileTestGears.agda Tue Nov 02 07:30:50 2021 +0900 +++ b/whileTestGears.agda Sat Apr 08 07:49:41 2023 +0900 @@ -103,7 +103,7 @@ -- ↓PreCondition(Invaliant) whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) - → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) + → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) -- next with PostCondition → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t whileLoopSeg env proof next exit with ( suc zero ≤? (varn env) ) whileLoopSeg {_} {_} {c10} env proof next exit | no p = exit env ( begin