Theory Pointer_Examples

(* Title: Verification Component Based on KAD: Programs with Pointers
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection‹KAD Component for Pointer Programs›

theory Pointer_Examples
  imports VC_KAD_Examples2 "HOL-Hoare.Heap"

begin

text ‹This component supports the verification of simple while programs
with pointers in a partial correctness setting.›

text‹All we do here is integrating Nipkow's implementation of pointers and heaps.›

type_synonym 'a state = "string  ⇒ ('a ref + ('a ⇒ 'a ref))"

lemma list_reversal:
  "PRE (λs :: 'a state. List (projr (s ''h'')) (projl (s ''p'')) Ps 
        ∧ List (projr (s ''h'')) (projl (s ''q'')) Qs 
        ∧ set Ps ∩ set Qs = {})
    (WHILE (λs. projl (s ''p'') ≠ Null) 
     INV (λs. ∃ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps 
              ∧ List (projr (s ''h'')) (projl (s ''q'')) qs 
              ∧ set ps ∩ set qs = {} ∧ rev ps @ qs = rev Ps @ Qs)
     DO
      (''r'' ::= (λs. s ''p''));
      (''p'' ::= (λs. Inl (projr (s ''h'') (addr (projl (s ''p''))))) );
      (''h'' ::= (λs. Inr ((projr (s ''h''))(addr (projl (s ''r'')) := projl (s ''q''))) ));
      (''q'' ::= (λs. s ''r''))
     OD)
  POST (λs. List (projr (s ''h'')) (projl (s ''q'')) (rev Ps @ Qs))"
  apply hoare 
  apply auto[2]
  by (clarsimp, fastforce intro: notin_List_update[THEN iffD2])

end