Require Export RefAlgebraImplem_class.
Require Export RefAlgebraImplem_point.
Require Export NumAlgebraImplem_const.
Require Export NumAlgebraImplem_top.
Require Export ValueAlgebraImplem_sum2.
Require Export StackAlgebraImplem_struct.
Require Export LocalVarAlgebraImplem_struct.
Require Export ObjectAlgebraImplem_struct.
Require Export HeapAlgebraImplem_fs.
Require Export correct.
Section P.
Variable P : Program.
Definition R : Ref.Connect P := RefAlgebraCl P.
| We can use RefAlgebraPt instead |
Definition N : Num.Connect := NumconstAlgebra.
| We can use NumTopAlgebra instead |
Definition V : Value.Connect (Num.Pos N) (Ref.Pos R) :=
ValueAlgebraSum (Num.Pos N) (Ref.Pos R).
Definition S : Stack.Connect (Value.Pos V) :=
StackAlgebra (Value.Pos V).
Definition L : LocalVar.Connect (Value.Pos V) :=
LocalVarAlgebra1 (Value.Pos V).
Definition O : Object.Connect (Value.Pos V) :=
ObjectAlgebra (Value.Pos V).
Definition H : Heap.Connect (Ref.Pos R) (Object.Pos O) :=
HeapConnect (Ref.Pos R) (Object.Pos O).
Check (AbstractSemantic_correct P R N V S L O H).
End P.