Library funcsem


Require Export semantic.

Require Export Pow.

Require Export rel.

Import List.

Import syntax.




Inductive push_op : Value -> OperandStack -> OperandStack -> Prop :=

 push_op_def : forall v s, push_op v s (v::s).

Inductive pop_op : OperandStack -> OperandStack -> Prop :=

 pop_op_def : forall v s, pop_op (v::s) s.

Inductive top_op : OperandStack -> Value -> Prop :=

 top_op_def : forall v s, top_op (v::s) v.




Inductive injN_op : integer -> Value -> Prop :=

 injN_op_def : forall n, injN_op n (num n).

Inductive injR_op : Location -> Value -> Prop :=

 injR_op_def : forall loc, injR_op loc (ref loc).

Inductive getN_op : Value -> integer -> Prop :=

 getN_op_def : forall n, getN_op (num n) n.

Inductive getR_op : Value -> Location -> Prop :=

 getR_op_def : forall loc, getR_op (ref loc) loc.




Inductive get_op (x:Var) : LocalVar -> Value -> Prop :=

 get_op_def : forall l, get_op  x l (l x).

Inductive store_op (x:Var) : LocalVar -> Value -> LocalVar -> Prop :=

 store_op_def : forall l v, store_op x l v (substLocalVar l x v).




Inductive sem_binop_op (op:Operator) : integer -> integer -> integer -> Prop :=

 sem_binop_op_def : forall n1 n2, sem_binop_op op n1 n2 (sem_binop op n1 n2).




Inductive getf_op (P:Program) (f:FieldName) : ClassInst -> Value -> Prop :=

  getf_op_def : forall o,

   In f (definedFields P (class o)) ->

   getf_op P f o (fieldValue o f).

Inductive putf_op (P:Program) (f:FieldName) : ClassInst -> Value -> ClassInst -> Prop :=

  putf_op_def : forall o v,

   In f (definedFields P (class o)) ->

   putf_op P f o v (substField o f v).

Inductive def_op (P:Program) (cl:ClassName) : OperandStack -> ClassInst -> Prop :=

  def_op_def : forall s c,

   searchClass P cl = Some c ->

   def_op P cl s (def c).




Inductive puto_op : Heap -> Location -> ClassInst -> Heap -> Prop :=

  puto_op_def : forall h loc o,

   puto_op h loc o (substHeap h loc o).

Inductive puto'_op : Heap -> Location -> ClassInst -> Heap -> Prop :=

  puto'_op_def : forall h loc o,

   h loc = None ->

   puto'_op h loc o (substHeap h loc o).

Inductive geto_op : Heap -> Location -> ClassInst -> Prop :=

  geto_op_def : forall h loc o,

   h loc = Some o ->

   geto_op h loc o.

Inductive newLoc_op (P:Program) (cl:ClassName) : Heap -> Location -> Prop :=

  newLoc_op_def : forall h loc',

   (exists c, searchClass P cl=Some c) ->

   loc'=(newObject P cl h) -> newLoc_op P cl h loc'.




Record FuncSem (P:Program) : Type := fs {

  f_pc : progCount -> progCount;

  f_h : Heap*OperandStack*LocalVar -> Heap -> Prop;

  f_s : Heap*OperandStack*LocalVar -> OperandStack -> Prop;

  f_l : Heap*OperandStack*LocalVar -> LocalVar -> Prop

}.




Load "Generated/func".




Lemma sem_func_correct : forall P i s1 s2,

 SmallStepSem P i s1 s2 ->

 let (h1,pc1,l1,s1) := s1 in

 let (h2,pc2,l2,s2) := s2 in

 f_pc P (sem_func P i) pc1 = pc2

/\

 f_h P (sem_func P i) (h1,s1,l1) h2

/\

 f_s P (sem_func P i) (h1,s1,l1) s2

/\

 f_l P (sem_func P i) (h1,s1,l1) l2.

destruct s1 as [h1 pc1 l1 s1]; destruct s2 as [h2 pc2 l2 s2].

intros Hsem; inversion_clear Hsem; simpl;

(split; [try reflexivity|

         split;[idtac|
                split]]).




Load "Generated/proof1".




Qed.
Index
This page has been generated by coqdoc