Mercurial > hg > Members > ryokka > HoareLogic
view Readme.md @ 98:2d2b0b06945b default tip
simplfied version
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 08 Apr 2023 17:00:53 +0900 |
parents | e152d7afbb58 |
children |
line wrap: on
line source
-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