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‹First, some operations for association lists›

primrec lookup :: "('a × 'b) list  'a  'b option"
"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

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

text‹Abstract types of variables, class names, field names, and

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"
"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"
"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 =
  | 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

consts body :: OBJ

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

inductive_set Semn :: "(State × OBJ × nat × State) set"
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"

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

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

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›