Theory OBJ

(*File: OBJ.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory OBJ imports Main begin

section‹Base-line non-interference with objects›

text‹\label{sec:Objects} We now extend the encoding for base-line
non-interference to a language with objects.  The development follows
the structure of Sections \ref{sec:IMP} to
\ref{sec:BaseLineNI}. Syntax and operational semantics are defined in
Section \ref{sec:ObjLanguage}, the axiomatic semantics in Section
\ref{sec:ObjLogic}. The generalised definition of non-interference is
given in \ref{sec:ObjNI}, the derived proof rules in Section
\ref{sec:ObjDerivedRules}, and a type system in the style of Volpano
et al.~in Section \ref{sec:ObjTypeSystem}. Finally, Section
\ref{sec:contextObj} concludes with results on contextual closure.›

subsection ‹Syntax and operational semantics›
text‹\label{sec:ObjLanguage}›

text‹First, some operations for association lists›

primrec lookup :: "('a × 'b) list ⇒ 'a ⇒ 'b option"
where
"lookup [] l = None" |
"lookup (h # t) l = (if (fst h)=l then Some (snd h) else lookup t l)" 

definition Dom::"('a × 'b) list ⇒ 'a set"
where "Dom L = {l . ∃ a . lookup L l = Some a}"

(*<*)
lemma lookupNoneAppend[rule_format]: 
"∀ l L2. (lookup L1 l = None ⟶ lookup L2 l = None ⟶ lookup (L1 @ L2) l = None)"
by (induct L1, simp+)

lemma DomAppendUnion[rule_format]: "∀ ab. Dom (a @ ab) = Dom a ∪ Dom ab"
apply (induct a)
apply (simp add: Dom_def)
apply (simp add: Dom_def)
apply clarsimp apply fast
done

lemma DomAppend: "Dom L ⊆ Dom((a, b) # L)"
by (simp add: Dom_def, auto)

lemma lookupSomeAppend1[rule_format]:
"∀ L2 l c . lookup L1 l = Some c ⟶ lookup (L1 @ L2) l = Some c"
by (induct L1, simp, simp)

lemma DomUnion[rule_format]:"Dom ((a,b) # L) = {a} ∪ Dom L"
by (simp add: Dom_def DomAppendUnion, fast)

lemma lookupSomeAppend2[rule_format]:
"∀ l c L2 . lookup L2 l = Some c ⟶ Dom L1 ∩ Dom L2 = {} ⟶ lookup (L1 @ L2) l = Some c"
apply (induct L1)
apply (simp add: Dom_def)
apply clarsimp
  apply rule
    apply clarsimp apply (subgoal_tac "l:Dom L2") apply (simp add: DomUnion) 
   apply (simp add: Dom_def) 
apply clarsimp
  apply (erule_tac x=l in allE)
  apply (erule_tac x=c in allE)
  apply (erule_tac x=L2 in allE)
  apply simp apply (erule impE) apply (simp add: DomUnion) 
  apply simp
done
(*>*)

text‹Abstract types of variables, class names, field names, and
locations.›

typedecl Var
typedecl Class
typedecl Field
typedecl Location

text‹References are either null or a location. Values are either
integers or references.›

datatype Ref = Nullref | Loc Location

datatype Val = RVal Ref | IVal int 

text‹The heap is a finite map from locations to objects. Objects have
a dynamic class and a field map.›

type_synonym Object = "Class × ((Field × Val) list)"
type_synonym Heap = "(Location × Object) list"

text‹Stores contain values for all variables, and states are pairs of
stores and heaps.›

type_synonym Store = "Var ⇒ Val"

definition update :: "Store ⇒ Var ⇒ Val ⇒ Store"
where "update s x v = (λ y . if x=y then v else s y)"

type_synonym State = "Store × Heap"

text‹Arithmetic and boolean expressions are as before.›

datatype Expr = 
    varE Var 
  | valE Val
  | opE "Val ⇒ Val ⇒ Val" Expr Expr

datatype BExpr = compB "Val ⇒ Val ⇒ bool" Expr Expr

text‹The same applies to their semantics.›

primrec evalE::"Expr ⇒ Store ⇒ Val"
where
"evalE (varE x) s = s x" |
"evalE (valE v) s = v" |
"evalE (opE f e1 e2) s = f (evalE e1 s) (evalE e2 s)"

primrec evalB::"BExpr ⇒ Store ⇒ bool"
where
"evalB (compB f e1 e2) s = f (evalE e1 s) (evalE e2 s)"

text‹The category of commands is extended by instructions for
allocating a fresh object, obtaining a value from a field and assigning
a value to a field.›

datatype OBJ =
    Skip 
  | Assign Var Expr
  | New Var Class
  | Get Var Var Field
  | Put Var Field Expr
  | Comp OBJ OBJ
  | While BExpr OBJ
  | Iff BExpr OBJ OBJ
  | Call

text‹The body of the procedure is identified by the same constant as
before.›

consts body :: OBJ

text‹The operational semantics is again a standard big-step
relation.›

inductive_set Semn :: "(State × OBJ × nat × State) set"
where
SemSkip: "s=t ⟹ (s,Skip,1, t):Semn"

| SemAssign:
  "⟦ t = (update (fst s) x (evalE e (fst s)), snd s)⟧ 
  ⟹ (s, Assign x e, 1, t):Semn"

| SemNew:
  "⟦l ∉ Dom (snd s); 
       t = (update (fst s) x (RVal (Loc l)), (l,(C,[])) # (snd s))⟧ 
  ⟹ (s, New x C, 1, t):Semn"

| SemGet:
  "⟦(fst s) y = RVal(Loc l); lookup (snd s) l = Some(C,Flds); 
       lookup Flds F = Some v; t = (update (fst s) x v, snd s)⟧ 
  ⟹ (s, Get x y F, 1, t):Semn"

| SemPut:
  "⟦(fst s) x = RVal(Loc l); lookup (snd s) l = Some(C,Flds); 
       t = (fst s, (l,(C,(F,evalE e (fst s)) # Flds)) # (snd s))⟧ 
  ⟹ (s, Put x F e, 1, t):Semn"

| SemComp:
  "⟦ (s, c, n, r):Semn; (r,d, m, t):Semn; k=(max n m)+1⟧
  ⟹ (s, Comp c d, k, t):Semn"

| SemWhileT:
  "⟦evalB b (fst s); (s,c, n, r):Semn; (r, While b c, m, t):Semn; k=((max n m)+1)⟧
  ⟹ (s, While b c, k, t):Semn"

| SemWhileF:
  "⟦¬ (evalB b (fst s)); t=s⟧ ⟹ (s, While b c, 1, t):Semn"

| SemTrue:
  "⟦evalB b (fst s); (s,c1, n, t):Semn⟧ 
  ⟹ (s, Iff b c1 c2, n+1, t):Semn"

| SemFalse:
  "⟦¬ (evalB b (fst s)); (s,c2, n, t):Semn⟧
  ⟹ (s, Iff b c1 c2, n+1, t):Semn"

| SemCall: "⟦ (s,body,n, t):Semn⟧ ⟹ (s,Call,n+1, t):Semn"

abbreviation
  SemN  :: "[State, OBJ, nat, State] ⇒ bool"   (" _ , _ →⇩_  _ ")
where
"s,c →⇩n t == (s,c,n,t) : Semn"

text‹Often, the height index does not matter, so we define a notion
hiding it.›

definition
Sem :: "[State, OBJ, State] ⇒ bool" ("_ , _ ⇓ _ " 1000)
where "s,c ⇓ t = (∃ n. s,c →⇩n t)"

inductive_cases Sem_eval_cases: 
 "s,Skip →⇩n t"
 "s,(Assign x e) →⇩n t"
 "s,(New x C) →⇩n t"
 "s,(Get x y F) →⇩n t"
 "s,(Put x F e) →⇩n t"
 "s,(Comp c1 c2) →⇩n t"
 "s,(While b c) →⇩n t"
 "s,(Iff b c1 c2) →⇩n t"
 "s, Call →⇩n t"

(*<*)
lemma Sem_no_zero_height_derivsAux: "∀ s t. ((s, c →⇩0 t) ⟶ False)"
by (induct_tac c, auto elim: Sem_eval_cases)
(*>*)
lemma Sem_no_zero_height_derivs: "(s, c →⇩0 t) ⟹ False"
(*<*)by (insert Sem_no_zero_height_derivsAux, fastforce)(*>*)

text‹Determinism does not hold as allocation is nondeterministic.›

text‹End of theory OBJ›
end