Library AlgebraType


Require Export LatticeLibrary.

Require Export Gamma.

Require Export funcsem.




Set Implicit Arguments.




Module Num.




Record Connect : Type := {

  t : Set;

  Pos : Lattice t;

  gamma : GammaTop (PowPoset nat) Pos;

 

  const_ab : nat -> t;

  const_ab_correct : forall n,

    (fun x:nat => x=n) <=< (gamma (const_ab n));




  sem_binop_ab : Operator -> t -> t -> t;

  sem_binop_ab_correct : forall op n1 n2,

    (Post2 (sem_binop_op op) (gamma n1) (gamma n2)) 

          <=< (gamma (sem_binop_ab op n1 n2))}.




End Num.




Module Ref.




Record Connect (P:Program) : Type := {

  C : Set;

  relC : C -> C -> Prop;

  context : VTrace P -> C;

  t : Set;

  Pos : LatticeAtom t;

  gamma : C -> GammaBestTop Location Pos;

  gamma_monotone : forall ct1 ct2,

    relC ct1 ct2 -> orderGamma (gamma ct1) (gamma ct2);




  newLoc_ab : ClassName -> progCount -> t;

  newLoc_ab_correct : forall (tr1 tr2:VTrace P) cl pc,

    SmallStepSemTrace P (new1 cl) tr1 tr2 ->

    pc = (pcSt (currentState tr1)) ->

    (Post (newLoc_op P cl) (fun h => h = hSt (currentState tr1)))

               <=< (gamma (context tr2) (newLoc_ab cl pc));




  transfert_increase_context : forall (tr1 tr2:VTrace P) r,

    SmallStepSemTrace P r tr1 tr2 ->

    relC (context tr1) (context tr2);




  transfert_decrease_context : forall (tr1 tr2:VTrace P) r,

    SmallStepSemTrace P r tr1 tr2 ->

    instr_not_new r ->

    relC (context tr2) (context tr1);




  conservation_during_new : forall cl (tr1 tr2:VTrace P) h1 r loc,

    SmallStepSemTrace P (new1 cl) tr1 tr2 ->

    h1 = hSt (currentState tr1) ->

    h1 loc <> None ->

    gamma (context tr2) r loc -> 

    gamma (context tr1) r loc

}.




End Ref.




Module Value.




Record Connect (N:Set) (R:Set) (PN:Lattice N) (PR:Lattice R) : Type := {

  t : Set;

  Pos : Lattice t;

  gamma : GammaTop (PowPoset nat) PN ->

          GammaTop (PowPoset Location) PR -> 

          GammaTop (PowPoset Value) Pos;




  gamma_functor_monotone : forall (gN1 gN2 : GammaTop (PowPoset nat) PN) (gR1 gR2 : GammaTop (PowPoset Location) PR),

    orderGamma gN1 gN2 ->

    orderGamma gR1 gR2 -> orderGamma (gamma gN1 gR1) (gamma gN2 gR2);




  null_ab : t;

  null_ab_correct : forall (gN:GammaTop (PowPoset nat) PN) (gR:GammaTop (PowPoset Location) PR),

    (fun v:Value => v=null) <=< (gamma gN gR null_ab);




  getN_ab : t -> N;

  getN_ab_correct : forall gN gR v,

    ((Post getN_op) (gamma gN gR v)) <=< (gN (getN_ab v));




  getR_ab : t -> R;

  getR_ab_correct : forall gN gR v,

    ((Post getR_op) (gamma gN gR v)) <=< (gR (getR_ab v));




  injN_ab : N -> t;

  injN_ab_correct : forall (gN:GammaTop (PowPoset nat) PN) gR n,

    ((Post injN_op) (gN n)) <=< (gamma gN gR (injN_ab n));




  injR_ab : R -> t;

  injR_ab_correct : forall gN (gR:GammaTop (PowPoset Location) PR) r,

    ((Post injR_op) (gR r)) <=< (gamma gN gR (injR_ab r))

}.




End Value.




Module Stack.




Record Connect (V:Set) (PV:Lattice V) : Type :=  {

  t : Set;

  Pos : Lattice t;

  gamma :  GammaTop (PowPoset Value) PV -> Gamma (PowPoset OperandStack) Pos;




  gamma_functor_monotone : forall (g1 g2 : GammaTop (PowPoset Value) PV),

    orderGamma g1 g2 -> orderGamma (gamma g1) (gamma g2);




  nil_ab : t; 

  nil_ab_correct : forall g,

    (fun s => s = nil) <=< (gamma g nil_ab);




  pop_ab : t -> t;

  pop_ab_correct : forall g s,

    ((Post pop_op) (gamma g s)) <=< (gamma g (pop_ab s));




  top_ab : t -> V;

  top_ab_correct : forall (g:GammaTop (PowPoset Value) PV) s,

    ((Post top_op) (gamma g s)) <=< (g (top_ab s));




  push_ab : V -> t -> t;

  push_ab_correct : forall (g:GammaTop (PowPoset Value) PV) v s,

    ((Post2 push_op) (g v) (gamma g s)) <=< (gamma g (push_ab v s))

}.




End Stack.




Module LocalVar.




Record Connect (V:Set) (PV:Lattice V) : Type := {

  t : Set;

  Pos : Lattice t;

  gamma :  Gamma (PowPoset Value) PV -> Gamma (PowPoset LocalVar) Pos;




  gamma_functor_monotone : forall g1 g2,

    orderGamma g1 g2 -> orderGamma (gamma g1) (gamma g2);




  get_ab : Var -> t -> V;

  get_ab_correct : forall (g:Gamma (PowPoset Value) PV) x l,

    ((Post (get_op x)) (gamma g l)) <=< (g (get_ab x l));




  store_ab : Var -> t -> V -> t;

  store_ab_correct : forall (g:Gamma (PowPoset Value) PV) x l v,

    ((Post2 (store_op x)) (gamma g l) (g v)) 

              <=< (gamma g (store_ab x l v));




  initLocalVar : V -> t;

  initLocalVar_correct : forall (g:Gamma (PowPoset Value) PV) AbNull,

    (fun v => v = null) <=< (g AbNull) ->

    (fun l => forall x, l x = null) <=< (gamma g (initLocalVar AbNull))

}.




End LocalVar.




Module Object.




Record Connect (V:Set) (PV:Lattice V) : Type := {

  t : Set;

  Pos : Lattice t;

  gamma :  Program -> GammaTop (PowPoset Value) PV -> GammaTop (PowPoset ClassInst) Pos;




  gamma_functor_monotone : forall P (g1 g2:GammaTop (PowPoset Value) PV),

    orderGamma g1 g2 -> orderGamma (gamma P g1) (gamma P g2);




  getf_ab : FieldName -> t -> V;

  getf_ab_correct : forall g P f o,

    ((Post (getf_op P f)) (gamma P g o))

         <=< (g (getf_ab f o));




  putf_ab : FieldName -> t -> V -> t;

  putf_ab_correct : forall g P f o v,

    ((Post2 (putf_op P f)) (gamma P g o) (g v)) 

              <=< (gamma P g (putf_ab f o v));




  def_ab : Program -> ClassName -> V -> V -> t;

  def_ab_correct : forall (g:GammaTop (PowPoset Value) PV) P cl (AbZero AbNull:V),

    (fun v => v = null) <=< (g AbNull) ->

    (fun v => v = num (0)) <=< (g AbZero) ->

    (Post (def_op P cl) (fun _ => True)) <=< (gamma P g (def_ab P cl AbZero AbNull))

}.




End Object.




Module Heap.




Record Connect (R:Set) (O:Set) (PR:LatticeAtom R) (PO:Lattice O) : Type := {

  t : Set;

  Pos : Lattice t;

  gamma : GammaBestTop Location PR ->

          GammaTop (PowPoset ClassInst) PO -> Gamma (PowPoset Heap) Pos;




  gamma_functor_monotone : forall (gR1 gR2 : GammaBestTop Location PR)

                          (gO1 gO2 : GammaTop (PowPoset ClassInst) PO),

    orderGamma gR2 gR1 ->

    orderGamma gO1 gO2 -> orderGamma (gamma gR1 gO1) (gamma gR2 gO2);




  puto_ab : t -> R -> O -> t;

  puto_ab_correct : forall gR gO h r o,

    (Post3 puto_op (gamma gR gO h) (gR r) (gO o))

               <=< (gamma gR gO (puto_ab h r o));

  puto_ab_correct' : forall (gR1 gR2 : GammaBestTop Location PR) gO h r o,

    forall hh rr oo hh',

    puto_op hh rr oo hh' ->

    gamma gR1 gO h hh ->

    gR2 r rr ->

    gO o oo ->

    (forall Loc loc, hh loc <> None ->

                      gR2 Loc loc -> gR1 Loc loc) ->

    gamma gR2 gO (puto_ab h r o) hh';




  geto_ab : t -> R -> O;

  geto_ab_correct : forall gR gO h r,

    (Post2 geto_op (gamma gR gO h) (gR r))

               <=< (gO  (geto_ab h r));

 

  emptyHeap : t;

  emptyHeap_correct : forall gR gO,

    (fun h => forall loc, h loc = None) <=< (gamma gR gO emptyHeap)




}.

 

End Heap.
Index
This page has been generated by coqdoc