Require syntax.
Definition Location := positive.
Definition Location_dec := positive_dec.
Definition ReferenceValue := Location.
Inductive Value : Set :=
| num : integer -> Value
| ref: ReferenceValue -> Value
| null : Value.
Definition comp : integer -> integer -> integer :=
[v1,v2]Cases (le_gt_dec v2 v1) of
|(left _)=> (1)
| (right _) => (0)
end.
Definition sem_binop : Operator -> integer -> integer -> integer :=
[op,v1,v2]
Cases op of
OpMult => (mult v1 v2)|
OpPlus => (plus v1 v2)|
OpComp => (comp v1 v2)|
OpMinus => (minus v1 v2)
end.
Definition OperandStack := (list Value).
Definition LocalVar := Var -> Value.
Definition substLocalVar :
LocalVar -> Var -> Value -> LocalVar :=
[L;i0;v0;i]
Cases (Var_dec i i0) of
| (left _) => v0
| (right _) => (L i)
end.
Record ClassInst : Set := classInstConstr{
class : ClassName;
fieldValue : FieldName -> Value
}.
Definition initField : typeOfField->Value :=
[t]Cases t of
| fieldNum => (num (0))
| fieldRef => null
end.
Definition def : Class -> ClassInst :=
[c]
(classInstConstr (nameClass c)
[f:FieldName]Cases (searchField c f) of
None => null
| (Some fi) => (initField (typeField fi))
end).
Definition substField :
ClassInst -> FieldName -> Value -> ClassInst :=
[o;f0;v0]
(classInstConstr (class o)
[f]Cases (Field_dec f f0) of
| (left _) => v0
| (right _) => (fieldValue o f)
end).
Lemma substfield_equal : (o : ClassInst ; f : FieldName ; v : Value)
v = (fieldValue (substField o f v) f).
Intros.
Unfold substField.
Simpl.
Case Field_dec ; Intros ; Auto.
Elim n ; Trivial.
Qed.
Lemma substfield_diff : (o : ClassInst ; f,f' : FieldName; v : Value)
~ f = f' -> (fieldValue o f') = (fieldValue (substField o f v) f').
Intros ; Simpl.
Case Field_dec ; Intros ; Auto.
Elim H; Auto.
Qed.
Lemma substField_same_class : (o : ClassInst ; f : FieldName ; v : Value)
(class (substField o f v))=(class o).
Unfold substField; Simpl; Intros; Auto.
Qed.
Implicits Some [1].
Definition Heap := Location -> (option ClassInst).
Definition substHeap : Heap -> Location -> ClassInst -> Heap :=
[H,i0,v0,i]
Cases (Location_dec i i0) of
| (left _) => (Some v0)
| (right _) => (H i)
end.
Lemma substHeap_equal : (h : Heap ; loc : Location ; o: ClassInst)
((substHeap h loc o) loc) = (Some o).
Intros; Unfold substHeap; Case Location_dec ; Intros ; Auto.
Elim n; Auto.
Qed.
Lemma substHeap_diff : (h : Heap ; loc,loc' : Location ; o: ClassInst)
~loc = loc' -> ((substHeap h loc o) loc') = (h loc').
Intros; Unfold substHeap; Case Location_dec ; Intros ; Auto.
Elim H ; Auto.
Qed.
Axiom newObject : Program -> ClassName -> Heap -> Heap*Location.
Axiom newObject_specif : (P:Program;c:Class;H,H':Heap;loc':Location)
(In c (classes P)) ->
(H',loc')=(newObject P (nameClass c) H) ->
(H loc')=(None ?)
/\ H'=(substHeap H loc' (def c)).
Inductive Frame : Set :=
| frame : MethodName -> progCount -> LocalVar -> OperandStack -> Frame.
Definition CallStack := (list Frame).
Inductive State : Set :=
| config : Heap -> CallStack -> State.
Grammar constr constr1 :=
frame [ "<" constr7($c1) "," constr7($c2) "," constr7($c3) "," constr7($c4) ">" ] -> [(frame $c1 $c2 $c3 $c4)].
Infix RIGHTA 7 "::" cons.
Inductive SmallStepSem [P:Program] : State -> State -> Prop :=
| nop_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack)
(instructionAt P m pc)=(Some nop) ->
(SmallStepSem P (config H <m,pc,L,S>::SF)
(config H <m,(nextAddress P m pc),L,S>::SF))
| push_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;c:integer)
(instructionAt P m pc)=(Some (push c)) ->
(SmallStepSem P (config H <m,pc,L,S>::SF)
(config H <m,(nextAddress P m pc),L,(num c)::S>::SF))
| pop_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;v:Value)
(instructionAt P m pc)=(Some pop) ->
(SmallStepSem P (config H <m,pc,L,v::S>::SF)
(config H <m,(nextAddress P m pc),L,S>::SF))
| numop_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;op:Operator;n1,n2:integer)
(instructionAt P m pc)=(Some (numop op)) ->
(SmallStepSem P (config H <m,pc,L,(num n1)::(num n2)::S>::SF)
(config H <m,(nextAddress P m pc),L,(num (sem_binop op n1 n2))::S>::SF))
| load_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;i:Var)
(instructionAt P m pc)=(Some (load i)) ->
(SmallStepSem P (config H <m,pc,L,S>::SF)
(config H <m,(nextAddress P m pc),L,(L i)::S>::SF))
| store_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;i:Var;v:Value)
(instructionAt P m pc)=(Some (store i)) ->
(SmallStepSem P (config H <m,pc,L,v::S>::SF)
(config H <m,(nextAddress P m pc),(substLocalVar L i v),S>::SF))
| if_not_nul_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;pc':progCount;n:integer)
(instructionAt P m pc)=(Some (If pc')) ->
~n=(0) ->
(SmallStepSem P (config H <m,pc,L,(num n)::S>::SF)
(config H <m,(nextAddress P m pc),L,S>::SF))
| if_nul_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;pc':progCount)
(instructionAt P m pc)=(Some (If pc')) ->
(SmallStepSem P (config H <m,pc,L,(num (0))::S>::SF)
(config H <m,pc',L,S>::SF))
| putfield_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;f:FieldName;v:Value;o:ClassInst;loc:Location)
(instructionAt P m pc)=(Some (putfield f)) ->
(H loc)=(Some o) ->
(EX c:Class | (In c (classes P)) /\ (nameClass c)=(class o)) ->
(SmallStepSem P (config H <m,pc,L,v::(ref loc)::S>::SF)
(config (substHeap H loc (substField o f v)) <m,(nextAddress P m pc),L,S>::SF))
| new_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;cl:ClassName;H':Heap;loc:Location)
(instructionAt P m pc)=(Some (new cl)) ->
(EX c:Class | (searchClass P cl)=(Some c)) ->
(H',loc)=(newObject P cl H) ->
(SmallStepSem P (config H <m,pc,L,S>::SF)
(config H' <m,(nextAddress P m pc),L,(ref loc)::S>::SF))
| getfield_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;f:FieldName;o:ClassInst;loc:Location)
(instructionAt P m pc)=(Some (getfield f)) ->
(H loc)=(Some o) ->
(EX c:Class | (In c (classes P)) /\ (nameClass c)=(class o)) ->
(SmallStepSem P (config H <m,pc,L,(ref loc)::S>::SF)
(config H <m,(nextAddress P m pc),L,(fieldValue o f)::S>::SF))
| invokevirtual_rule :
(m:MethodName;pc:progCount;L,L':LocalVar;A,S:OperandStack;
H:Heap;SF:CallStack;mID:MethodID;o:ClassInst;loc:Location;
M':Method;n:nat)
(instructionAt P m pc)=(Some (invokevirtual mID)) ->
(H loc)=(Some o) ->
(EX c:Class | (In c (classes P)) /\ (nameClass c)=(class o)) ->
(methodLookup P mID (class o))=(Some M') ->
n=(nbArguments M') ->
n=(length A) ->
L'=([p:positive](nth (pred (convert p)) (ref loc)::A null)) ->
(SmallStepSem P (config H <m,pc,L,(ref loc)::(app A S)>::SF)
(config H <(nameMethod M'),xH,L',(nil ?)>::<m,pc,L,S>::SF))
| return_rule :
(m,m':MethodName;pc,pc':progCount;L,L':LocalVar;S,S':OperandStack;
H:Heap;SF:CallStack;v:Value)
(instructionAt P m' pc')=(Some return) ->
(SmallStepSem P (config H <m',pc',L',v::S'>::<m,pc,L,S>::SF)
(config H <m,(nextAddress P m pc),L,v::S>::SF))
| dup_rule : (m:MethodName;pc: progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack; v : Value)
(instructionAt P m pc)=(Some dup) ->
(SmallStepSem P (config H <m,pc,L,v::S>::SF)
(config H <m,(nextAddress P m pc),L,v::v::S>::SF))
|
goto_rule :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack;pc':progCount)
(instructionAt P m pc)=(Some (goto pc')) ->
(SmallStepSem P (config H <m,pc,L,S>::SF)
(config H <m,pc',L,S>::SF))
|swap_rule :
(m:MethodName;pc: progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack; v1,v2 : Value)
(instructionAt P m pc)=(Some swap) ->
(SmallStepSem P (config H <m,pc,L,v1::v2::S>::SF)
(config H <m,(nextAddress P m pc),L,v2::v1::S>::SF))
|dup2_rule :
(m:MethodName;pc: progCount;L:LocalVar;S:OperandStack;
H:Heap;SF:CallStack; v1,v2 : Value)
(instructionAt P m pc)=(Some dup2) ->
(SmallStepSem P (config H <m,pc,L,v1::v2::S>::SF)
(config H <m,(nextAddress P m pc),L,v1::v2::v1::v2::S>::SF)).
Inductive SmallStepSem_star [P:Program]: State -> State -> Prop :=
| SmallStepSem_star_0 : (C:State)(SmallStepSem_star P C C)
| SmallStepSem_star_rec : (C1,C2,C3:State)
(SmallStepSem_star P C1 C2) ->
(SmallStepSem P C2 C3) -> (SmallStepSem_star P C1 C3).
Definition valid_State : State -> Prop :=
[St]let (h,sf)=St in
((loc,loc0:Location;o:ClassInst;f:FieldName)
(h loc)=(Some o) -> (fieldValue o f)=(ref loc0) -> ~(h loc0)=(None ?))
/\((f:Frame)(In f sf) ->
let (m,pc,l,s)=f in
((x:Var;loc1:Location)(l x)=(ref loc1) -> ~(h loc1)=(None ?))
/\ ((loc2:Location)(In (ref loc2) s)-> ~(h loc2)=(None ?))).
Inductive initial_State [P:Program] : State -> Prop :=
init_State : (L:LocalVar)
((x:Var)(L x)=null) ->
(initial_State P (config [loc](None ?) <(main P),xH,L,(nil ?)>::(nil ?))).
Inductive reachable_State [P: Program] : State -> Prop :=
reachable_init : (st: State) (initial_State P st) -> (reachable_State P st)
|reachable_step : (st, st' : State) (reachable_State P st) ->
(SmallStepSem P st st')-> (reachable_State P st').
Inductive reachable_in [P: Program] : State -> nat-> Prop :=
reachable_in_0: (st : State) (initial_State P st) -> (reachable_in P st (0))
|reachable_in_S : (st, st' : State; n : nat) (reachable_in P st n) ->
(SmallStepSem P st st')-> (reachable_in P st' (S n)).
Lemma reachable_reachable_in : (P : Program ; st : State)
(reachable_State P st) -> (EX n : nat | (reachable_in P st n)).
Intros.
NewInduction H.
Exists (0) ; Constructor ; Trivial.
Elim IHreachable_State ; Intros m ; Exists (S m); Constructor 2 with st ; Trivial.
Qed.
Lemma reachable_in_reachable : (P : Program ; st : State)
(n : nat) (reachable_in P st n) -> (reachable_State P st).
Intros.
NewInduction H.
Constructor ; Trivial.
Constructor 2 with st ; Auto.
Qed.