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 a ∈ Addr.
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 := (Var → Class) × Meth → PC.

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 : PC → option 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 := Var → option Addr.
  Definition Object := (Class × (Field → option Addr))%type.
  Definition Heap := Addr → option 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) : Var → Class :=
    fun r ⇒ match l r with
               | None ⇒ Udf
               | Some a ⇒ match h a with
                             | None ⇒ Udf
                             | Some (t,o) ⇒ t
                           end
             end.

Definition Null : Field → option 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 [ r ↦ e r'] , h)
| read : ∀ f e h o t a, e(v0) = Some a → h a = Some (t,o) →
  intra (Read f) (e,h) (e [ v0 ↦ o f] , h)
| write : ∀ f e h o t a, e(v0) = Some a → h a = Some (t,o) →
  intra (Write f) (e,h) (e, h [ a ↦ Some (t, o [f ↦ e(v1) ]) ] )
| alloc : ∀ t a e h, h a = None →
  intra (New t) (e,h) (e [ v0 ↦ Some a] , h [ a ↦ Some ( t, Null) ]).

The sos semantics
Inductive sos : State → State → Prop :=
| sos_intra : ∀ pc i e h e' h' s, nthp pc = Some i → intra 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' [v0 ↦ e(v0)])::s).

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

Definition Empty : Heap := fun x ⇒ None.

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

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

End Semantics.

This page has been generated by coqdoc