Library Cool

Syntax and semantics of the Core Object-Oriented Language

We consider sets of class names Class, method names Meth, field names Field, variable names Var and addresses Addr
Parameters Class Meth Field Var: Set.
There are at least two variables v0 and v1 and a class name Udf (for undefined)
Parameters v0 v1 : Var.
There are finitely many variables. The analysis is sound even if there infinitly many variables. Yet, finitness is useful for Kleene fixpoint theorem which provides us an induction principle.
Parameter Vars : list Var.
Parameters finVar : ∀ v, In v Vars.

Udf can be thought as the class of the null pointer. The null pointer is modelled by None and a genuine address by Some a where aAddr.
Parameter Udf : Class.
Parameter Addr : Set.

A program is a pair list of statements (∈ St) and a lookup function
Inductive St :=
| Copy (v : Var) (v' : Var)
| New (c: Class)
| Read (f: Field)
| Write(f: Field)
| Call(m:Meth)
| Ret.

Definition PC := nat.

Definition Lkup := (VarClass) × MethPC.

Definition Program := ((list St) × Lkup)%type.

Section Semantics.
We consider a program P, the program statements are p and the lookup function is lk
  Hypothesis P : Program.
  Definition p := fst P.
  Definition lk := snd P.

The function nthp pc returns the statement at index pc or None if the index is out-of-bounds
  Definition nthp : PCoption St
The Semantics domains are the following:
  • Env is an environment mapping variables to addresses
  • An object o:Object is a pair made (c,o) where c is a class name and o a mapping from field to addresses
  • A heap h:Heap is a mapping from addresses to objects
  • A frame f:Frame is a pair made of a program counter and an environment
  • A program state s:State is a pair (h,s) where h is a heap and s:Frame+ is a list of frames

  Definition Env := Varoption Addr.
  Definition Object := (Class × (Fieldoption Addr))%type.
  Definition Heap := Addroption Object.
  Definition Frame := (PC × Env)%type.
Semantics invariants will ensure that the list of frames is never empty
  Definition State := (Heap × list Frame)%type.

Auxiliary semantic definitions
  Definition dp (h:Heap) (l:Env) : VarClass :=
    fun rmatch l r with
               | NoneUdf
               | Some amatch h a with
                             | NoneUdf
                             | Some (t,o) ⇒ t

Definition Null : Fieldoption Addr := fun (f:Field) ⇒ None.

The semantics of intra-procedural statements
Inductive intra : St → (Env × Heap) → (Env × Heap) → Prop :=
| copy : ∀ r r' e h, intra (Copy r r') (e,h) (e [ re r'] , h)
| read : ∀ f e h o t a, e(v0) = Some ah a = Some (t,o) →
  intra (Read f) (e,h) (e [ v0o f] , h)
| write : ∀ f e h o t a, e(v0) = Some ah a = Some (t,o) →
  intra (Write f) (e,h) (e, h [ aSome (t, o [fe(v1) ]) ] )
| alloc : ∀ t a e h, h a = None
  intra (New t) (e,h) (e [ v0Some a] , h [ aSome ( t, Null) ]).

The sos semantics
Inductive sos : StateStateProp :=
| sos_intra : ∀ pc i e h e' h' s, nthp pc = Some iintra i (e,h) (e',h') →
    sos (h , (pc, e)::s) (h', (pc+1,e')::s)
| sos_call : ∀ pc m e h s ,
  nthp pc = Some (Call m) →
  sos (h,(pc,e)::s) (h,(lk (dp h e,m),e)::(pc,e) ::s)
| sos_ret : ∀ pc e h pc' e' s, nthp pc = Some Ret
  sos (h,(pc,e)::(pc',e')::s) (h,(pc'+1, e' [v0e(v0)])::s).

Notation "S ⊳ T" := (sos S T) (at level 50).

Definition Empty : Heap := fun xNone.

The semantics starts from an initial state s0
Definition s0 : State := (Empty, (0 , fun vNone)::nil).

The set Acc is the set of states reachable from s0 by the reflexive transitive closure of
Inductive Acc : StateProp :=
| Acc0 : Acc s0
| AccSos : ∀ s s', Acc sss'Acc s'.

End Semantics.

This page has been generated by coqdoc