Theory IMP_concur

chapter‹‹IMP⇩c⇩o⇩n⇩c⇩u⇩r›-A Shallow Embedding in HOL-CSP›

theory IMP_concur
imports "HOL-CSPM" (* changeset 16909:83221a878a3a, 28.8.26 *) 

begin

section‹Introduction›

text‹
‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› is intended to provide a more common (though still theoretic)
programming-language aspect to CSP, and could be an interesting object
of study in itself. This thin layer over HOL-CSP establishes a link 
between programming languages and process-algebras, a link that had already
been present in the influential OCCAM language.

‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› comprises the standard elements of the IMP - language (‹SKIP›, ‹assignment›,
‹IF _ THEN _ ELSE›, ‹WHILE _ DO _› and the sequential composition ‹_ ; _›), plus 
the new features:
   ▸ semaphores with ‹lock› and ‹unlock›, and
   ▸ thread-global shared variables accessible 
     via ‹LOAD› and ‹STORE› operations.

This file contains:
   ▸ the abstract and concrete syntax of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r›
   ▸ bricks-specifications for semaphores and global shared variables,
   ▸ a denotational semantics of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› converting ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r›-program 
     systems into HOL-CSPM, and
   ▸ some examples and tests.

The general theory should be developed elsewhere; this sample file shows the 
global construction principle of a combined semantics.›


section‹The Syntax of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r››

type_synonym SV = string  ― ‹Shared Variables›
type_synonym V  = string  ― ‹(Thread-)Local Variables›
type_synonym MV = int     ― ‹Mutual exclusion variables (MUTEX ids)›

type_synonym D = int

type_synonym "σ" = ‹V ⇒ D›

type_synonym "E⇩a⇩r⇩i⇩t⇩h" = ‹σ ⇒ D›
type_synonym "E⇩b⇩o⇩o⇩l"  = ‹σ ⇒ bool›
type_synonym "F"     = "σ ⇒ σ"

datatype com = SKIP
             | assign  V E⇩a⇩r⇩i⇩t⇩h       (" _ := _" [90,90]80)
             | seq     com com       (infixr ";" 78)
             | cond   "E⇩b⇩o⇩o⇩l" com com ("IF (_)/ THEN (_)/ ELSE (_)/" 
                                               [0,0,79]79)
             | while  "E⇩b⇩o⇩o⇩l" com     ("WHILE (_)/ DO (_)" [0,80]80)
             | call    F

             | STOP
             | lock    MV
             | unlock  MV            
             | send    E⇩a⇩r⇩i⇩t⇩h SV      ("STORE _ TO  _" [90,90]80)              
             | rec     V SV          ("LOAD _ FROM _" [90,90]80)


text‹Note that it is straight forward to formulate the assert primitive in ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r›:›

definition assert where ‹assert E ≡ IF E THEN SKIP ELSE STOP ›

text‹... which reduces the checking of assertions to the proof of deedlock-freeness. ›

text‹Two (non-sensical) example threads:›

definition Thread1 where
      ‹ Thread1 ≡ SKIP ; 
                  ''a'' :=  (λσ. 1 + 2); 
                  IF (λσ. σ ''d'' > 3) THEN lock 4 ELSE lock 3;  
                  WHILE (λσ. σ ''e'' > 3) DO lock 4 ;  
                  STORE (λσ. σ ''d'' + 1) TO ''b''; 
                  LOAD ''a'' FROM  ''b''; 
                  unlock 3
      ›

definition Thread2 where
      ‹ Thread2 ≡ SKIP ; 
                  ''a'' :=  (λσ. 1 + 2); 
                  IF (λσ. σ ''d'' > 3) THEN lock 4 ELSE lock 3;  
                  WHILE (λσ. True) DO lock 4 ;  
                  STORE (λσ. σ ''d'' + 1) TO ''b''; 
                  LOAD ''a'' FROM  ''b''; 
                  unlock 3
      ›

thm Thread2_def
definition Thread3 where 
  "Thread3 = SKIP ;
             ( ''var_local'' := (λσ. 4 + 42) ;
             ( ''test'' := (λσ. 2 * σ ''var_local'') ;
             ( ''test'' := (λσ. σ ''test'' + 3) ;
              IF (λσ. σ ''x''>5)
              THEN WHILE (λσ. σ ''x'' >5) DO  ''test'' := (λσ. σ ''test'' - 3)
              ELSE  ''test'' := (λσ. σ ''test'' + 3))))"

ML‹val Thread2_term = \<^term>‹Thread2›;
   val _ $ _ $ Thread2_rhs = Thm.concl_of @{thm Thread2_def}›


section‹Events, States and Semaphores ("Bricks").›

text‹The common set of events in a thread-system›

datatype evs = lock int | unlock int | read⇩g⇩l⇩o⇩b⇩a⇩l SV D | upd⇩g⇩l⇩o⇩b⇩a⇩l  SV D 
                                     | read⇩l⇩o⇩c⇩a⇩l SV D | update⇩l⇩o⇩c⇩a⇩l SV D 

definition LOCKS where ‹LOCKS ≡ range lock ∪ range unlock›
definition GVARS where ‹GVARS ≡ {e. ∃x. ∃y. e = read⇩g⇩l⇩o⇩b⇩a⇩l x y } ∪ 
                                 {e. ∃x. ∃y. e = upd⇩g⇩l⇩o⇩b⇩a⇩l x y }›

lemma L1 [simp]: ‹lock n ∉ GVARS›   unfolding GVARS_def by auto
lemma L2 [simp]: ‹lock n ∈ LOCKS›   unfolding LOCKS_def by auto
lemma L3 [simp]: ‹unlock n ∉ GVARS› unfolding GVARS_def by auto
lemma L4 [simp]: ‹unlock n ∈ LOCKS› unfolding LOCKS_def by auto

lemma L5 [simp]: ‹read⇩g⇩l⇩o⇩b⇩a⇩l n m ∉ LOCKS›   unfolding LOCKS_def GVARS_def by auto
lemma L6 [simp]: ‹read⇩g⇩l⇩o⇩b⇩a⇩l n m ∈ GVARS›   unfolding LOCKS_def GVARS_def by auto
lemma L7 [simp]: ‹upd⇩g⇩l⇩o⇩b⇩a⇩l n m ∉ LOCKS›    unfolding LOCKS_def GVARS_def by auto
lemma L8 [simp]: ‹upd⇩g⇩l⇩o⇩b⇩a⇩l n m ∈ GVARS›    unfolding LOCKS_def GVARS_def by auto

lemma L9 [simp]: ‹read⇩l⇩o⇩c⇩a⇩l n m ∉ LOCKS›    unfolding LOCKS_def GVARS_def by auto
lemma L10[simp]: ‹read⇩l⇩o⇩c⇩a⇩l n m ∉ GVARS›    unfolding LOCKS_def GVARS_def by auto
lemma L11[simp]: ‹update⇩l⇩o⇩c⇩a⇩l n m ∉ LOCKS›  unfolding LOCKS_def GVARS_def by auto
lemma L12[simp]: ‹update⇩l⇩o⇩c⇩a⇩l n m ∉ GVARS›  unfolding LOCKS_def GVARS_def by auto



subsection‹A simple Model of a Semaphore Family›
(* (this should be a locale, see HOL-CSP-Bricks.) *)
(* datatype   sema_evs = lock int | unlock int *)


definition semaphore :: ‹int ⇒ evs process›
  where   ‹semaphore ≡ μ X. (λn. lock n → unlock n → X n)›

lemma sema_rec : ‹semaphore n = lock n → unlock n → semaphore n›
  by (subst cont_process_rec[OF semaphore_def[THEN meta_eq_to_obj_eq]]) simp_all

subsection‹A simple Model of a Global Variable Family›

definition global_vars :: ‹σ ⇒ SV ⇒ evs process› 
  where   ‹global_vars ≡ μ X.   (λ σ. (λ id.  ((read⇩g⇩l⇩o⇩b⇩a⇩l id)❙!(σ id) → X σ id ) 
                                            □ ((upd⇩g⇩l⇩o⇩b⇩a⇩l id)❙?v → X (σ(id := v)) id )))›


lemma global_vars_rec : ‹global_vars σ n =    ((read⇩g⇩l⇩o⇩b⇩a⇩l n)❙!(σ n) → global_vars σ n) 
                                           □ ((upd⇩g⇩l⇩o⇩b⇩a⇩l n)❙?v → global_vars (σ(n := v)) n)› 
  by (subst cont_process_rec[OF global_vars_def[THEN meta_eq_to_obj_eq]]) simp_all


subsection‹A simple Model of a Local Variable Family (Optional)›

definition local_vars :: " σ ⇒ SV ⇒ evs process" 
  where   ‹local_vars ≡ μ X.   (λ σ. (λ id.  ((read⇩l⇩o⇩c⇩a⇩l id)❙!(σ id) → X σ id) 
                                           □ ((update⇩l⇩o⇩c⇩a⇩l id)❙?v → X (σ(id := v)) id )))›

lemma local_vars_rec : ‹local_vars σ n =     ((read⇩l⇩o⇩c⇩a⇩l n)❙!(σ n) → local_vars σ n) 
                                           □ ((update⇩l⇩o⇩c⇩a⇩l n)❙?v → local_vars (σ(n := v)) n)› 
  by (subst cont_process_rec[OF local_vars_def[THEN meta_eq_to_obj_eq]]) simp_all


section‹Denotational Semantics of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r››

text‹The denotational semantics of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› is a straight recursive interpretation 
in the domain of HOL-CSP processes. Thread local variables were represented in this 
presentation by updates on a thread-local environment, not by interactions with processes.
The recursive definition of the semantic function fits on a post-card:›

fun Sem⇩0 :: "com ⇒ (σ ⇒ evs  process) ⇒ σ ⇒ evs process" 
  where "Sem⇩0 SKIP C                  = C" 
       |"Sem⇩0 (x := E) C              = (λ σ. C (σ(x := E σ)))"
       |"Sem⇩0 (P ; Q) C               = (Sem⇩0 P (Sem⇩0 Q C))" 
       |"Sem⇩0 (IF E THEN C1 ELSE C2) C= (λ σ. if E σ 
                                              then Sem⇩0 C1 C σ 
                                              else Sem⇩0 C2 C σ)"
       |"Sem⇩0 (WHILE E DO B) C        = (μ X. (λ σ. if E σ 
                                                    then Sem⇩0 B X σ 
                                                    else C σ))"
       |"Sem⇩0 (call F) C              = (λ σ. C (F σ))"
       |"Sem⇩0 (com.STOP) C            = (λ σ. Constant_Processes.STOP)"
       |"Sem⇩0 (com.lock n) C          = (λ σ. evs.lock n → C σ)"
       |"Sem⇩0 (com.unlock n) C        = (λ σ. evs.unlock n  → C σ)"
       |"Sem⇩0 (STORE E TO X⇩g⇩l⇩o) C      = (λ σ. upd⇩g⇩l⇩o⇩b⇩a⇩l X⇩g⇩l⇩o (E σ) → C σ)"
       |"Sem⇩0 (LOAD X⇩l⇩o⇩c FROM X⇩g⇩l⇩o) C   = (λ σ. (read⇩g⇩l⇩o⇩b⇩a⇩l X⇩g⇩l⇩o)❙?x 
                                                  → C(σ(X⇩l⇩o⇩c:=x)))"
(* Fascinating: We don't need the sequential composition of CSP in this construction;
   continuation passing is sufficient. *)

definition initial_state :: σ (‹σ⇩0›)
  where   ‹σ⇩0 ≡ (λ_. 0::int)›

definition some_state :: σ (‹σ⇩e⇩x⇩p⇩l›)
  where   ‹σ⇩e⇩x⇩p⇩l v ≡ if v = ''a'' then 3 else 0›

text‹In case that an ▩‹assume›-primitive on initial states has to be modeled
(the usual contruct for modeling preconditions), this can be done by the 
Hilbert-Choice operator \<^term>‹SOME σ. E› on initial local and global states. ›


definition Sem         where ‹Sem Thread ≡ Sem⇩0 Thread (λ_. Skip) σ⇩0›  
   ― ‹final continuation: \<^term>‹Skip›, execution starts with initialized local vars
       for simplicity. ›

section‹A Thread-System as HOL-CSPM-Architecture›

text‹An example of a global ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r›-System with 2 threads, 3 global variables and 4 semaphores:›

definition‹Thread3_sem ≡ ( ❙|❙|❙| idx ∈# mset [''a'',''b'',''c''].  global_vars σ⇩0 idx  
                           |||
                           ❙|❙|❙| idx ∈# mset [1..4]. semaphore idx )
          
                           ||
            
                           (Sem Thread1 ||| Sem Thread2)
                           ›


ML‹(* ... and this reads at the term-level as follows : *)
   val _ $ _ $ temp= Thm.concl_of @{thm Thread3_sem_def}  
   val temp2= \<^term>‹❙|❙|❙| idx ∈# mset [''a'',''b'',''c''].  global_vars σ⇩0 idx›
  ›

text‹Tests:›

lemma Thread2_sem : 
  "Sem(Thread2) =  evs.lock 3 → (μ x. (λσ::σ. evs.lock 4 → x σ)) σ⇩e⇩x⇩p⇩l"
  unfolding Thread2_def Sem_def some_state_def initial_state_def
  by (simp add: fun_upd_def)

(* symbolic evaluation : *)
schematic_goal K : "Thread3_sem = ?X"
  unfolding Thread3_sem_def Sem_def
  unfolding Thread1_def Thread2_def
   apply(rule trans)
   apply (simp add: List.upto.simps cong: HOL.if_cong)
  by (rule refl)
  


lemma Thread3_sem : 
    ‹ Thread3_sem = ((global_vars σ⇩0 ''a'' ||| (global_vars σ⇩0 ''b'' ||| global_vars σ⇩0 ''c'')) 
                     ||| (semaphore 1 ||| (semaphore 2 ||| (semaphore 3 ||| semaphore 4))))
                    || 
                    ((evs.lock 3 → (μ x. (λσ. if 3 < σ ''e'' 
                                               then evs.lock 4 → x σ
                                               else upd⇩g⇩l⇩o⇩b⇩a⇩l ''b'' (σ ''d'' + 1)
                                                     → read⇩g⇩l⇩o⇩b⇩a⇩l ''b''❙?x 
                                                     → evs.unlock 3 → Skip))
                       ((λ_. 0::int)(''a'' := 3::int))) 
                     ||| 
                     (evs.lock 3 → (μ x. (λσ. evs.lock 4 → x σ)) ((λ_. 0::int)(''a'':= 3::int)))) 
    ›
  unfolding Thread3_sem_def Sem_def Thread1_def Thread2_def initial_state_def
  by (simp add: List.upto.simps cong: HOL.if_cong)
  

(* A look into the term structure *)
ML‹
val x =HOLogic.dest_eq (HOLogic.dest_Trueprop ( Thm.concl_of  @{thm K})) ; 
val y = @{thm Thread3_sem} |> Thm.concl_of 
                           |> HOLogic.dest_Trueprop 
                           |> HOLogic.dest_eq
›

section‹A Semantic Corner-Case of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r››

text‹We study the case of three global variables and 4 locks 
and a computation that spends its time in an infinite loop without
communicating. (The result would be the same if inside the loop,
only compuations on local variables were done.›

definition Thread4 where 
  "Thread4 = WHILE (λσ. True) DO  SKIP"

definition Thread4_sem where 
"Thread4_sem ≡ ( ❙|❙|❙| idx ∈# mset [''a'',''b'',''c''].  global_vars σ⇩0 idx  
                  |||
                  ❙|❙|❙| idx ∈# mset [1..4]. semaphore idx )
                 
                ||
   
                  (Sem Thread4)"

text‹The following theory shows that this type of programs collapses to \<^term>‹⊥›. ›
theorem bang : ‹Thread4_sem = ⊥›
  unfolding Thread4_sem_def Thread4_def Sem_def
  by (simp add: List.upto.simps Fixrec.fix_id cong: HOL.if_cong) (* Eh bim ! *)


section‹Another Semantic Corner-Case: Deadlock›

text‹For simplicity of the subsequent proof, we model a system without global variables:›

definition Thread5 where 
  "Thread5 = WHILE (λσ. True) DO (com.lock 1)"

definition Thread5_sem where 
"Thread5_sem ≡  ( ❙|❙|❙| idx ∈# mset [1..4]. semaphore idx )  
                 
                  ||
 
                   Sem Thread5"

lemma Thread5_while_rec : "(μ x::'b ⇒ evs process. (λσ. evs.lock (1::int) → x σ)) A 
             = evs.lock 1 → (μ x. (λσ. evs.lock (1::int) → x σ)) A"
  by(subst cont_process_rec[where P = ‹(μ x. (λσ. evs.lock (1::int) → x σ))›, OF refl]) simp_all 

text‹This process system will deadlock after the first attempt to get \<^term>‹com.lock 0›.
This can be formally proven in HOL-CSP by stating: 

@{cartouche [indent=10] ‹¬ deadlock_free Thread5_sem›}.

The proof is shown in the following subsection.
›

subsection‹A Technique to rewrite Interleaves to MPrefixes›

text‹Note that the following description is not necessarily the most effective manner to establish
deadlock-freeness via fixed-point induction; it is  clear that it will not scale up to large
process systems. (For a more powerful and automated approach, we refer to the handling via Proc-Omata 
\cite{BallenghienW24} or the approach in \cite{ITP2026}). Our proceeding has, though, the advantage 
to use only very basic means and is therefore a self-contained demonstration.
›

text‹A key obstacle for the establishment of deadlock-properties is that we need to bring
both sides of the parallel composition operator ‹_ || _› into the form \<^term>‹Mprefix A P› in order
to apply the rule:

 @{thm [indent=10, display] Mprefix_Par_Mprefix} 

The  \<^term>‹Mprefix›-terms are typically
quite large if-then-else cascades representing some form of decision diagram that collapse to 
small terms after synchronization.›

lemma inter2Mprefix1: 
  assumes  "a ≠ b" 
  shows "(a → P ||| b → Q) 
          = Mprefix {a,b} (λx. if x = a then (P ||| b → Q) 
                                        else (a → P) ||| Q )"
  apply(simp add:write0_Inter_write0)
  by(subst (3) write0_def,subst write0_Det_Mprefix,simp add: assms)


lemma inter2Mprefix2: 
  assumes * : "a ∉ A"
  shows "((a → P) ||| Mprefix A Q) 
          = Mprefix (insert a A) (λx. if x = a then (P ||| Mprefix A Q) 
                                               else ((a → P) ||| Q x) )"
  apply(subst write0_def,simp add: Mprefix_Inter_Mprefix)
  apply(subst Mprefix_Det_Mprefix, simp add: assms)
  by(fold write0_def, simp)

lemma inter2Mprefix3:
  "a ≠ b ⟹ ((a → P a) □ (b → Q b)) 
             = Mprefix {a,b} (λx. if x= a then P a else Q b)"
  apply(simp add: Mprefix_singl[symmetric] )
  by (smt (verit, ccfv_threshold) Mprefix_Un_distrib Mprefix_singl 
          Un_insert_right insert_commute sup_bot.right_neutral)

text‹After these generalities, we turn to the core lemmas relevant to the subsequent proofs.
They construct compact normalforms for states (represented by CSPM-expressions) linked
by the events \<^term>‹evs.lock 1› and  \<^term>‹evs.unlock 1›. They proceed by blowing both sides
up into a lower-level normalform in which their equality can be demonstrated.›

lemma contractMultiInter1 : 
  "MultiInter (mset [1..4]) semaphore || evs.lock 1 → P 
   =  evs.lock 1 → ((evs.unlock 1 → semaphore 1  ||| MultiInter (mset [2..4]) semaphore) || P)"
  (is "?lhs = evs.lock 1 → ?rhs")
proof -
  have * : "?lhs = evs.lock 1 →
                    ((evs.unlock 1 → semaphore 1 
                     ||| □x∈{evs.lock 2, evs.lock 3, evs.lock 4}
                                → (if x = evs.lock 2
                                    then evs.unlock 2 → semaphore 2 
                                         ||| 
                                         □x∈{evs.lock 3, evs.lock 4}
                                               → (if x = evs.lock 3 
                                                   then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                                   else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                                    else semaphore 2 
                                         ||| 
                                         (if x = evs.lock 3 
                                          then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                          else semaphore 3 ||| evs.unlock 4 → semaphore 4))) || P)"
    (is "_ = evs.lock 1 → ?rhs'")
           apply(rule trans)
           apply(simp add: List.upto.simps)
           apply(subst sema_rec[where n=‹1›],
                 subst sema_rec[where n=‹2›],
                 subst sema_rec[where n=‹3›],
                 subst sema_rec[where n=‹4›]) 
           apply(rule trans)
            apply(simp add: inter2Mprefix1 inter2Mprefix2)
             apply(simp add: sema_rec[where n=‹1›,symmetric] 
                             sema_rec[where n=‹2›,symmetric] 
                             sema_rec[where n=‹3›,symmetric] 
                             sema_rec[where n=‹4›,symmetric] 
                        cong: HOL.if_cong)
             apply(subst write0_def[THEN meta_eq_to_obj_eq, of"evs.lock (1::int)"])
             by(subst Mprefix_Par_Mprefix, simp add: Mprefix_singl) ― ‹et bang!›
  define X where "X = ?rhs'"
  have ** : "?rhs = X" 
           apply(subst write0_def[THEN meta_eq_to_obj_eq])
           apply(simp add: List.upto.simps)  
           apply(subst sema_rec[where n=‹1›],subst sema_rec[where n=‹2›],
                 subst sema_rec[where n=‹3›],subst sema_rec[where n=‹4›]) 
           apply(simp add: inter2Mprefix1 inter2Mprefix2) 
           by (metis X_def sema_rec Mprefix_singl)
  show ?thesis
    by (metis * ** X_def)
qed


lemma contractMultiInter2: 
      "  ((evs.unlock 1 → semaphore 1  ||| MultiInter (mset [2..4]) semaphore) 
         ||  evs.lock 1 → P) 
       = Constant_Processes.STOP"
         (is "(?R || ?S) = _")
proof - 
  have 1 : "?R = □x∈{evs.unlock 1, evs.lock 2, evs.lock 3, evs.lock 4}
       → (if x = evs.unlock 1
           then semaphore 1
                ||| □x∈{evs.lock 2, evs.lock 3, evs.lock 4}
                          → (if x = evs.lock 2
                              then evs.unlock 2 → semaphore 2
                              ||| □x∈{evs.lock 3, evs.lock 4}
                                      → (if x = evs.lock 3 
                                          then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                          else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                              else semaphore  2
                                   ||| (if x = evs.lock 3 
                                        then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                        else semaphore 3 ||| evs.unlock 4 → semaphore 4))
           else evs.unlock 1 → semaphore 1
               ||| (if x = evs.lock 2
                    then evs.unlock 2 → semaphore 2
                         ||| □x∈{evs.lock 3, evs.lock 4}
                             → (if x = evs.lock 3 then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                    else semaphore 2 
                         ||| (if x = evs.lock 3
                              then evs.unlock 3 → semaphore 3 ||| semaphore 4
                              else semaphore 3 ||| evs.unlock 4 → semaphore 4)))"
         apply(simp add: List.upto.simps)
         apply(subst sema_rec[where n=‹1›],subst sema_rec[where n=‹2›],
               subst sema_rec[where n=‹3›],subst sema_rec[where n=‹4›]) 
         apply(simp add: inter2Mprefix1 inter2Mprefix2)
         by(simp add: sema_rec[where n=‹1›,symmetric] 
                      sema_rec[where n=‹2›,symmetric] 
                      sema_rec[where n=‹3›,symmetric] 
                      sema_rec[where n=‹4›,symmetric] 
                 cong: HOL.if_cong)
  show ?thesis
    apply(subst(2) write0_def[THEN meta_eq_to_obj_eq])
    apply(subst 1)
    by (simp add: Mprefix_Par_Mprefix)
qed


text‹After these preparatory lemmas, the path to the deadlock is straight-forward:
it proceeds by unroling the while-loop two times; unfolding
\<^term>‹semaphore 1› and its fixpoint two times; simplifying to \<^term>‹STOP›
since \<^term>‹lock 0› and \<^term>‹unlock 0› are forced  to be synchronized, 
propagating this result to the refinement level and reduce it to a contradiction
of the refinement statement with the \<^term>‹DF UNIV› process.
We skip the formal proof here since it is out of scope of this presentation. ›


theorem bullocks: ‹¬ deadlock_free Thread5_sem›
  unfolding Thread5_sem_def Sem_def Thread5_def
proof - 
  show ‹¬ deadlock_free
               ( MultiInter (mset [1..4]) semaphore
                || Sem⇩0 (WHILE λσ. True DO com.lock 1) (λ_. Skip) σ⇩0)›
                (is ‹¬ deadlock_free (?SEMA || ?P )›)
  proof - 
    have 1 : ‹?P = evs.lock 1 → ?P› using Thread5_while_rec by auto
    have 2 : ‹(?SEMA || evs.lock 1 → ?P) 
              =  evs.lock 1 → ((evs.unlock 1 → semaphore 1  
                                ||| MultiInter (mset [2..4]) semaphore) || ?P)›
             (is "?lhs = evs.lock 1 → ?R'")
      by (metis contractMultiInter1)
    have 3 : ‹(¬ deadlock_free Thread5_sem) = (¬ deadlock_free ?R')›
      by (metis 1 2 Sem_def Thread5_def Thread5_sem_def deadlock_free_write0_iff)
    have 4: ‹?R' = Constant_Processes.STOP› 
      by (metis 1 contractMultiInter2)
    show ?thesis
      using 3 4 Sem_def Thread5_def Thread5_sem_def non_deadlock_free_STOP by auto
  qed
qed


text‹This proof can be drastically shortened / automatized if we would use a more advanced 
background theory of HOL-CSP, for example:›

term‹Initials Q ⊆ ev ` S 
     ⟹ Initials Q ∩ ev ` T = {} 
     ⟹  ((P □ Q) ⟦S⟧ (Mprefix T R)) = P ⟦S⟧ (Mprefix T R)›

term‹α(Q) ⊆ S 
     ⟹ α(Q) ∩ T = {} 
     ⟹ α(Q) ∩ α(R) = {} 
     ⟹ ((P ||| Q) ⟦S⟧ R) = P ⟦S⟧ R›

term‹α(Q) ⊆ S 
     ⟹ α(Q) ∩ T = {} 
     ⟹ Initials Q ∩ α((Mprefix T R)) = {} 
     ⟹ ((P ||| Q) ⟦S⟧ (Mprefix T R)) = P ⟦S⟧ (Mprefix T R)›

section‹Yet another Semantic Corner-Case: A Deadlock-Freeness Proof›

text‹We slightly mofify the previous example by adding the following thread into the
architecture:›

definition Thread6 where 
  "Thread6 = WHILE (λσ. True) DO (com.unlock 1)"

lemma Thread6_while_rec : 
          "(μ x::'b ⇒ evs process. (λσ. evs.unlock (1::int) → x σ)) A 
            = evs.unlock 1 → (μ x. (λσ. evs.unlock (1::int) → x σ)) A"
  by(subst cont_process_rec[where P = ‹(μ x. (λσ. evs.unlock (1::int) → x σ))›, 
                            OF refl]) simp_all


definition Thread6_sem where 
"Thread6_sem ≡ ( ❙|❙|❙| idx ∈# mset [1..4]. semaphore idx )  
                 
                 ||
 
                 (Sem Thread5 ||| Sem Thread6)"

text‹The architecture \<^term>‹Thread6›, however, will not deadlock, although each single thread will.
This shows that in ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› locks can mutually deblock each other and have ---
together with the global variables --- global  visibility inside the thread system.›


text‹The statement for this claim looks as follows:›

term  ‹deadlock_free Thread6_sem›  

text‹We will present in this theory a straight-forward proof approach (HOL-CSP has more
sophisticated and also more automatic methods than the suggested one). We need a little
background theory concerning \<^term>‹deadlock_free›'ness here; in principle, it can be 
established via a consequence of the fixpoint induction. A complication to be tackled
is that we need a format of this induction that takes two events --- instead of just one ---
to arrive at the anchor of the induction, namely \<^term>‹lock› and \<^term>‹unlock›. ›

subsection‹On Coinduction for deadlock-freeness.› 

text‹In the following, we derive the necessary deadlock-coinduction:›

lemma lasso_equiv1: "DF UNIV = (μ x. ⊓a∈UNIV →  ⊓a∈UNIV → x)"
unfolding DF_def
proof(rule FD_antisym)
  have * : ‹X = (X ∧ X)› for X by simp
  show ‹(μ x. ⊓a∈UNIV → x) ⊑⇩F⇩D (μ x. ⊓a∈UNIV → ⊓a∈UNIV → x)›
    apply(subst *)
    apply(subst cont_process_rec[where P = ‹(μ x. ⊓a∈UNIV → x)› 
                                   and f = ‹λx. ⊓a∈UNIV → x›],simp_all)
    apply(rule fix_ind[where F = ‹(Λ x. ⊓a∈UNIV → x)›], simp,simp) 
     apply(subst cont_process_rec[where P = ‹(μ x. ⊓a∈UNIV → ⊓a∈UNIV → x)› 
                                    and f = ‹λx. ⊓a∈UNIV → ⊓a∈UNIV → x›], simp_all)
     apply(rule mono_Mndetprefix_FD, simp) 
    apply(subst cont_process_rec[where P = ‹(μ x. ⊓a∈UNIV → ⊓a∈UNIV → x)› 
                                       and f = ‹λx. ⊓a∈UNIV → ⊓a∈UNIV → x›], simp_all)
    by (simp add: mono_Mndetprefix_FD)
next 
  show ‹(μ x. ⊓a∈UNIV → ⊓a∈UNIV → x) ⊑⇩F⇩D (μ x. ⊓a∈UNIV → x)› 
    apply(rule fix_ind[where F = ‹(Λ x. ⊓a∈UNIV → ⊓a∈UNIV → x)›] )  
      apply (simp_all)
    apply(subst cont_process_rec[where P = ‹(μ x. ⊓a∈UNIV → x)› 
                                       and f = ‹λx. ⊓a∈UNIV → x›], simp_all)
    apply(subst cont_process_rec[where P = ‹(μ x. ⊓a∈UNIV → x)› 
                                       and f = ‹λx. ⊓a∈UNIV → x›], simp_all)
    apply(rule mono_Mndetprefix_FD, simp) 
    by(rule mono_Mndetprefix_FD, simp) 
qed



text‹Here is the neccessary versions of \<^term>‹deadlock_free›-ness induction for
cases with a lasso-length 1 and 2:›
lemma deadlock_free_1_coinduct :
          ‹    (⋀x. x ⊑⇩F⇩D P ⟹ ⊓a∈UNIV → x ⊑⇩F⇩D P)
           ⟹ deadlock_free (P::('α, 'δ) process⇩p⇩t⇩i⇩c⇩k)›
  apply(rule DF_Univ_freeness[of UNIV], simp,unfold DF_def)
  by(rule fix_ind)(simp_all)
 
lemma deadlock_free_2_coinduct :
       ‹ (⋀x. x ⊑⇩F⇩D P ⟹ ⊓a∈UNIV → ⊓a∈UNIV → x ⊑⇩F⇩D P)
         ⟹ deadlock_free (P::('α, 'δ) process⇩p⇩t⇩i⇩c⇩k)›
  apply(rule DF_Univ_freeness[of UNIV],simp_all add: lasso_equiv1)
  by(rule fix_ind)(simp_all)

text‹And we need two more technical lemmas (analogously to the proofs in the previous session)
that enable us to represent the intermediate process states by compact process expressions 
in ▩‹HOL-CSPM›.›


lemma contractMultiInter1':
  assumes ‹evs.unlock 1 → P2 = P2›
  shows   ‹MultiInter (mset [1..4]) semaphore
           || 
           □x∈{evs.lock 1, evs.unlock 1}
              → (if x = evs.lock 1 then P1 ||| evs.unlock 1 → P2 else evs.lock 1 → P1 ||| P2) =
           evs.lock 1 →
           (   (evs.unlock 1 → semaphore 1 ||| MultiInter (mset [2..4]) semaphore) 
           || (P1 ||| P2))›
  (is "?lhs = evs.lock 1 → ?rhs")
proof - 
   have * : "?lhs = evs.lock 1 →
                    ((evs.unlock 1 → semaphore 1 
                     ||| □x∈{evs.lock 2, evs.lock 3, evs.lock 4}
                                → (if x = evs.lock 2
                                    then evs.unlock 2 → semaphore 2 
                                         ||| 
                                         □x∈{evs.lock 3, evs.lock 4}
                                               → (if x = evs.lock 3 
                                                   then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                                   else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                                    else semaphore 2 
                                         ||| 
                                         (if x = evs.lock 3 
                                          then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                          else semaphore 3 ||| evs.unlock 4 → semaphore 4))) 
                    || (P1 ||| evs.unlock 1 → P2))"
    (is "_ = evs.lock 1 → ?rhs'")
          apply(rule trans)
           apply(simp add: List.upto.simps)
          apply(subst sema_rec[where n=‹1›],subst sema_rec[where n=‹2›],
                subst sema_rec[where n=‹3›],subst sema_rec[where n=‹4›]) 
          apply(rule trans)
          apply(simp add: inter2Mprefix1 inter2Mprefix2)
          apply(simp add: sema_rec[where n=‹1›,symmetric] 
                          sema_rec[where n=‹2›,symmetric] 
                          sema_rec[where n=‹3›,symmetric] 
                          sema_rec[where n=‹4›,symmetric]
                     cong: HOL.if_cong)
          apply(subst write0_def[THEN meta_eq_to_obj_eq, of"evs.lock (1::int)"])
          by(subst Mprefix_Par_Mprefix, simp add: Mprefix_singl)
  define X where "X = ?rhs'"
  have ** : "?rhs = X" 
          apply(subst write0_def[THEN meta_eq_to_obj_eq])
          apply(simp add: List.upto.simps)  
          apply(subst sema_rec[where n=‹1›],subst sema_rec[where n=‹2›],
                subst sema_rec[where n=‹3›],subst sema_rec[where n=‹4›]) 
          apply(simp add: inter2Mprefix1 inter2Mprefix2) 
          apply(simp only: X_def) 
          by (metis sema_rec assms Mprefix_singl)
  show ?thesis
    by (metis * ** X_def)
qed


lemma contractMultiInter1'' : 
  assumes "evs.lock 1 → P1 = P1"
  shows ‹
          (evs.unlock 1 → semaphore 1  ||| MultiInter (mset [2..4]) semaphore) 
        || □x∈{evs.lock 1, evs.unlock 1}
              → (if x = evs.lock 1 
                  then P1 ||| evs.unlock 1 → P2 
                  else evs.lock 1 → P1 ||| P2) 
        = 
          (evs.unlock 1 → ((MultiInter (mset [1..4]) semaphore) 
                            || (P1  ||| P2)))
        ›
       (is "(?R || ?S) = evs.unlock 1 → ?rhs") 
proof -
  have 1 : "?R = □x∈{evs.unlock 1, evs.lock 2, evs.lock 3, evs.lock 4}
                 → (if x = evs.unlock 1
                     then semaphore 1
                          ||| □x∈{evs.lock 2, evs.lock 3, evs.lock 4}
                              → (if x = evs.lock 2
                                  then evs.unlock 2 → semaphore 2
                                       ||| □x∈{evs.lock 3, evs.lock 4}
                                           → (if x = evs.lock 3 
                                               then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                               else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                                  else semaphore  2
                                       ||| (if x = evs.lock 3 
                                            then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                            else semaphore 3 ||| evs.unlock 4 → semaphore 4))
                     else evs.unlock 1 → semaphore 1
                          ||| (if x = evs.lock 2
                               then evs.unlock 2 → semaphore 2
                                    ||| □x∈{evs.lock 3, evs.lock 4}
                                        → (if x = evs.lock 3 
                                            then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                            else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                               else semaphore 2 
                                    ||| (if x = evs.lock 3
                                         then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                         else semaphore 3 ||| evs.unlock 4 → semaphore 4)))"
           apply(simp add: List.upto.simps)
           apply(subst sema_rec[where n=‹1›],subst sema_rec[where n=‹2›],
                 subst sema_rec[where n=‹3›],subst sema_rec[where n=‹4›]) 
           apply(simp add: inter2Mprefix1 inter2Mprefix2)
           by(simp add: sema_rec[where n=‹1›,symmetric] 
                        sema_rec[where n=‹2›,symmetric] 
                        sema_rec[where n=‹3›,symmetric] 
                        sema_rec[where n=‹4›,symmetric] 
                   cong: HOL.if_cong)
  have 2: "evs.unlock 1 → ?rhs = □x∈{evs.unlock 1} → ?rhs" by (metis write0_def)
  have 3: "?rhs = □x∈{evs.lock 1, evs.lock 2, evs.lock 3, evs.lock 4}
                    → (if x = evs.lock 1
                        then evs.unlock 1 → semaphore  1 
                             ||| □x∈{evs.lock 2, evs.lock 3, evs.lock 4}
                                 → (if x = evs.lock 2
                                     then evs.unlock 2 → semaphore 2 
                                          ||| □x∈{evs.lock 3, evs.lock 4}
                                              → (if x = evs.lock 3 
                                                  then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                                  else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                                     else semaphore 2 
                                          ||| (if x = evs.lock 3 
                                               then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                               else semaphore 3 ||| evs.unlock 4 → semaphore 4))
                      else semaphore 1 
                           ||| (if x = evs.lock 2
                                then evs.unlock 2 →  semaphore 2 
                                     ||| □x∈{evs.lock 3, evs.lock 4}
                                         → (if x = evs.lock 3 
                                             then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                             else semaphore 3 ||| evs.unlock 4 → semaphore 4)
                                else semaphore 2 
                                     ||| (if x = evs.lock 3 
                                          then evs.unlock 3 → semaphore 3 ||| semaphore 4
                                          else semaphore 3 ||| evs.unlock 4 → semaphore 4))) 
                        || (P1 ||| P2)"
         apply(simp add: List.upto.simps)
         apply(subst sema_rec[where n=‹1›],subst sema_rec[where n=‹2›],
               subst sema_rec[where n=‹3›],subst sema_rec[where n=‹4›]) 
         apply(simp add: inter2Mprefix1 inter2Mprefix2)
         by(simp add: sema_rec[where n=‹1›,symmetric] 
                      sema_rec[where n=‹2›,symmetric] 
                      sema_rec[where n=‹3›,symmetric] 
                      sema_rec[where n=‹4›,symmetric] 
                 cong: HOL.if_cong)
  show ?thesis
    apply(subst 1, subst 2)
    apply(subst Mprefix_Par_Mprefix, simp_all)
    apply(simp_all add: Mprefix_singl  cong: HOL.if_cong)
    apply(subst sema_rec[where n=‹1›])
    apply(subst inter2Mprefix2, simp)
    apply(subst inter2Mprefix2, simp)
    apply(subst assms)
    apply(subst sema_rec[where n=‹1›, symmetric])
    apply(subst 3)
    by (metis (no_types,lifting) empty_iff evs.distinct(1) insert_iff 
              inter2Mprefix2 mono_Mprefix_eq)
  qed


text‹And now we attack the main theorem:›

theorem bullocks2 :  ‹deadlock_free Thread6_sem›  
  unfolding Thread6_sem_def Sem_def Thread5_def Thread6_def
proof - 
  show ‹deadlock_free
               ( MultiInter (mset [1..4]) semaphore
                || (    Sem⇩0 (WHILE λσ. True DO com.lock 1) (λ_. Skip) σ⇩0 
                    ||| Sem⇩0 (WHILE λσ. True DO com.unlock 1) (λ_. Skip) σ⇩0))›
                (is ‹deadlock_free (?SEMA || (?P1  ||| ?P2))›)
  proof -
    have 1 : ‹?P1 = evs.lock 1 → ?P1› using Thread5_while_rec by auto
    have 2 : ‹?P2 = evs.unlock 1 → ?P2› using Thread6_while_rec by auto
    have 3 : ‹?P1  ||| ?P2 = □x∈{evs.lock 1, evs.unlock 1}
                             → (if x = evs.lock 1 then ?P1 ||| evs.unlock 1 → ?P2
                                                   else evs.lock 1 → ?P1 ||| ?P2)›
             apply(subst 1, subst 2) by(subst inter2Mprefix1,simp_all)
    have 4 : ‹(?SEMA || ...) 
              = evs.lock 1 → ((evs.unlock 1 → semaphore 1  ||| MultiInter (mset [2..4]) semaphore) 
                || (?P1 ||| ?P2))›
             (is ‹_ = evs.lock 1 → ?P3›)
             using 2 contractMultiInter1' by auto
    have 5 : ‹ (evs.unlock 1 → semaphore 1  ||| MultiInter (mset [2..4]) semaphore) || (?P1|||?P2) 
              = 
               (evs.unlock 1 → ((MultiInter (mset [1..4]) semaphore) || (?P1|||?P2)))›
             using 1 3 contractMultiInter1'' by fastforce
    show ?thesis
      apply(rule deadlock_free_2_coinduct) 
      apply(subst 3, subst 4)
      apply(rule Mndetprefix_FD_write0[of ‹evs.lock 1›, THEN trans_FD],simp)
      apply(rule mono_write0_FD)
      apply(subst 5) 
      by (metis Mndetprefix_FD UNIV_I mono_write0_FD)
  qed
qed


section‹A more serious Example: An MPI Program›

text‹The example is drawn from Steven F. Siegels paper:
``Parameterized Verification of Deterministic MPI Programs''
🌐‹https://arxiv.org/pdf/2607.18049›, 2026. It addresses 
the verification of message passing programs (MPI) 
⁋‹Message-Passing Interface Forum. 2025. MPI: A Message-Passing
Interface Standard, Version 5.0. 
🌐‹https://www.mpi-forum.org/docs/mpi-5.0/mpi50-report.pdf›.›

The informal spec of the running example reads as follows:
The program ▩‹cycsum› is a cyclic sum reduction to all processes. Each
process stores a int number in ‹x›, then repeatedly sends to
its left, receives from its right, and adds the received value to
sum. At the end, each process holds the sum of the original
array ‹A› of values.

A bit more formally, this reads as follows:
@{cartouche [indent=10, display]
‹1  param A;
2  var i, x, sum, left, right;
3  assume isRealArray(A,NP) ∧ x = A[pid];
4  left := (pid + NP−1)%NP;
5  right := (pid + 1)%NP;
6  i := 1;
7  sum := x;
8  while ( i < NP ) {
9     send x to left;
10    recv x from right;
11    sum := sum + x;
12    x := x+1;
13 }
14 assert sum = Σ⇧N⇧P⇧−⇧1⇩i⇩=⇩0 A[i];›}

Note that this is a conceptual notation. The full fledged proof in Frama-C
involves several transformations and an unverfied VCG in the tool-chain; however, it
offers automated proofs of the  program code annotated by assertions, which 
comprises 17 pages of dense Frama-C code. 

Our modeling in ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› reads as follows:› 

consts NP:: int ― ‹Parameter of spec as unspecified constant›

consts array :: ‹string × int ⇒ string› 
                ― ‹array-name + offset :
                    the only thing we need to know: array is injective.›
consts array_offset :: ‹string × int ⇒ int›
                ― ‹the only thing we need to know: ‹array_offset(array(X,i)) = i›.›

term‹[1..N]›
definition sums where  ‹sums A = fold (+) A (0::int) ›

definition Thread7 where
‹Thread7 pid A = ( ''left''  := (λσ. (pid + NP - 1) mod NP)) ;
                 ( ''right'' := (λσ. (pid + 1) mod NP)) ;
                 ( ''i''     := (λσ. 1)) ;
                 com.lock pid;
                 LOAD ''x'' FROM array(''A'',pid);
                 com.unlock pid ;
                 ( ''sum''     := (λσ. σ ''x'')) ;
                 WHILE (λσ. σ ''i'' < NP) DO
                      (com.lock ((pid - 1 + NP) mod NP);
                       STORE (λσ. σ ''x'') TO (array(''A'',(pid - 1 + NP) mod NP));
                       com.unlock ((pid - 1 + NP) mod NP) ;
                       com.lock ((pid + 1) mod NP);
                       LOAD ''x'' FROM array(''A'',(pid + 1) mod NP);
                       com.unlock ((pid + 1) mod NP);
                       (''sum'' := (λσ. σ ''sum'' + σ ''x''));
                       (''i'' := (λσ. σ ''i'' + 1))
                      );
                  assert (λσ. σ ''sum'' = sums A)
›

text‹Some remarks: we assume that the ‹send› and ‹recv› semantics of the
above informal notation implies an implicit lock-unlock mechanism  of these
global variables. Moreover, the notation is not quite consequent: while MPI programs
are explicitely designed for fixed architectures (in our case: a ring), the notation
implies access to the local variables which could be modified. In our example ▩‹cycsum›,
‹left› and ‹right› are constants which have obviously been introduced just to increase
readability. The assertion syntax is, as common in PL-annotation languages, a mixture
of logical variables and program variables which are syntactically identified: the array ‹A› is
referring to the ∗‹content› of the state of the array ‹A›. This has to be made explicit
in the correctness statement.
›


definition Thread7_sem where 
"Thread7_sem A A' ≡ 
          ( ❙|❙|❙| idx ∈# mset [''a'',''b'',''c''].  global_vars σ⇩0 idx  
            |||
            ❙|❙|❙| idx ∈# mset [1..4]. semaphore idx )  
                 
          ||

          ( ❙|❙|❙| idx ∈# mset [1..NP]. semaphore idx )"

text‹... where ‹A'›, the array-cell-environment, should be set to its content ‹A›: 
     ‹A'(array(''A'',idx)) = A!(idx-1)› for all idx in ‹[1..NP]›. 
     See remark on the difference between array and its content above.›

text‹Again, the functional correctness proof boils down to a deadlock-freeness proof:›

theorem correct: 
  assumes ‹∀ i ∈ set[1..NP]. A'(array(''A'',idx)) = A!(nat(idx-1))› 
   and    ‹length A = nat NP›
  shows   ‹deadlock_free (Thread7_sem A A')›
  unfolding deadlock_free_def Thread7_sem_def Sem_def Thread7_def
  oops

text‹We consider a formal proof here as out of scope.›


section‹An Architectural Extension: Parameterized Threads›

text‹With a tiny bit of tinkering, we can extend the language ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› to a language
allowing to express dynamic calculations of architectural connections:›

type_synonym "LV⇩e⇩x⇩p⇩r"  = ‹σ ⇒ V›       ― ‹Local Variable Expr›
type_synonym "SV⇩e⇩x⇩p⇩r"  = ‹σ ⇒ MV›      ― ‹Semaphore Expr›
type_synonym  GV⇩e⇩x⇩p⇩r   = ‹σ ⇒ string›  ― ‹Global Variable Expr›

datatype com⇩a = SKIP
             | assign  LV⇩e⇩x⇩p⇩r E⇩a⇩r⇩i⇩t⇩h        (" _ :=⇩a _" [90,90]80)
             | seq     com⇩a com⇩a          (infixl ";;" 78)
             | cond   "E⇩b⇩o⇩o⇩l" com⇩a com⇩a    ("IF⇩a (_)/ THEN (_)/ ELSE (_)/" [0,0,79]79)
             | while  "E⇩b⇩o⇩o⇩l" com⇩a         ("WHILE⇩a (_)/ DO (_)" [0,80]80)
             | call    F

             | lock    SV⇩e⇩x⇩p⇩r
             | unlock  SV⇩e⇩x⇩p⇩r            
             | send    E⇩a⇩r⇩i⇩t⇩h GV⇩e⇩x⇩p⇩r        ("STORE⇩a _ TO  _" [90,90]80)              
             | rec     E⇩a⇩r⇩i⇩t⇩h GV⇩e⇩x⇩p⇩r        ("LOAD⇩a _ FROM _" [90,90]80)


section‹Denotational Semantics of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r›-P, a parametric version of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r››

consts VarName :: ‹int ⇒ string› ― ‹converts a reference to a global var name›

fun Sem⇩a⇩0 :: "com⇩a ⇒ (σ ⇒ evs  process) ⇒ σ ⇒ evs process" 
  where ‹Sem⇩a⇩0 SKIP C                    = C› 
       |‹Sem⇩a⇩0 (x :=⇩a E) C               = (λ σ. C (σ((x σ) := E σ)))›
       |‹Sem⇩a⇩0 (P ;; Q) C                = (Sem⇩a⇩0 P (Sem⇩a⇩0 Q C))› 
       |‹Sem⇩a⇩0 (IF⇩a E THEN C1 ELSE C2) C = (λ σ. if E σ 
                                                then Sem⇩a⇩0 C1 C σ 
                                                else Sem⇩a⇩0 C2 C σ)›
       |‹Sem⇩a⇩0 (WHILE⇩a E DO B) C         = (μ X. (λ σ. if E σ 
                                                      then Sem⇩a⇩0 B X σ 
                                                      else C σ))›
       |‹Sem⇩a⇩0 (com⇩a.call F) C           = (λ σ. C (F σ))›
       |‹Sem⇩a⇩0 (com⇩a.lock n) C           = (λ σ. evs.lock (n σ) → C σ)›
       |‹Sem⇩a⇩0 (com⇩a.unlock n) C         = (λ σ. evs.unlock (n σ)  → C σ)›
       |‹Sem⇩a⇩0 (STORE⇩a E TO X⇩g⇩l⇩o) C       = (λ σ. upd⇩g⇩l⇩o⇩b⇩a⇩l (X⇩g⇩l⇩o σ) (E σ) → C σ)›
       |‹Sem⇩a⇩0 (LOAD⇩a X⇩l⇩o⇩c FROM  X⇩g⇩l⇩o) C   = (λ σ. (read⇩g⇩l⇩o⇩b⇩a⇩l (X⇩g⇩l⇩o σ))❙?x
                                                     → C(σ((VarName(X⇩l⇩o⇩c σ)):=x)))›

section‹Conclusion and Future Work›

text‹We have shown the language and semantics of ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r›, a thin layer over HOL-CSP
giving this process-algebra a more programming language flavor. It is conceived to 
show the close link between both worlds considered quite distinct by many.

The embedding provides:
   ▸ a clear semantic foundation via HOL-CSP to HOL,
     comprising  computation and concurrency, 
   ▸ an end-to-end verification of a verification method inside 
     a highly trustable interactive proof assistant, 
   ▸ a path to theorem proving of functional properties,
     via deadlock-freeness proofs,
   ▸ a path to model-checking of functional properties,
     via deadlock-freeness inside FDR4 (unpublished so far).
›

text‹
An interesting direction for future work is, for example, how  a Hoare Calculus for ‹IMP⇩c⇩o⇩n⇩c⇩u⇩r› 
would look like, or how a conversion to FDR4 could be used in a SPIN-like manner 
for finitized programs as model-checking-based backend for practical purposes.›


(*<*) 
end
(*>*)