Mercurial > hg > Members > ryokka > HoareLogic
view ReadmeGears.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: 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.