-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