Library JMLOpSem
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Require Export JMLSemantics.
Require Import List.
Require Import Relation_Operators.
Import Dom.
Import Prog.
Import METHODSPEC.
The Java Operational Semantics
As parameter, we pass the module that defines the jml annotations to use (semantics or rac)
Retrieve values from StepValues, abort if no normal step happened
Fixpoint nv2v (nv : list StepValue) : list Value :=
match nv with
| ((normal_step_v v)::t) => (v::(nv2v t))
| _ => nil
end.
If the list of values is as long as the list of StepValue
all step values come from normal steps, used in ExprStep
Lemma nv2v_implication :
forall nvl vl,
(forall nv, exists v, In nv nvl -> nv = (normal_step_v v))->
nv2v nvl = vl ->
length nvl = length vl.
Proof.
intros.
inversion_clear H0.
induction nvl.
compute;reflexivity.
destruct (H a).
rewrite H0.
simpl.
apply f_equal.
apply IHnvl.
intros.
destruct (H nv).
exists x0.
auto with datatypes.
apply in_eq.
Qed.
Evaluation of one step of an expression
Assignment to an instance field: target.fsig = expr
| assignment_instance_field_ok:
forall e v obj fsig expr target st st1 st2 st' st3 loc cn um,
e = Assignment (field fsig (Some target)) expr ->
loc = (Heap.InstanceField obj fsig) ->
ExpressionStep p target st st1 (normal_step_v (Ref obj)) ->
FieldUpdateCheck p loc st1 ->
ExpressionStep p expr st1 st2 (normal_step_v v) ->
Heap.typeof st2@h obj = Some (Heap.ObjectObject cn um) ->
defined_field p cn fsig ->
assign_compatible p st2@h v (FIELDSIGNATURE.type (snd fsig)) ->
FieldUpdateAction p loc v st2 = st3 ->
st' = st3[h:= Heap.update st2@h loc v] ->
ExpressionStep p e st st' (normal_step_v v)
forall e v obj fsig expr target st st1 st2 st' st3 loc cn um,
e = Assignment (field fsig (Some target)) expr ->
loc = (Heap.InstanceField obj fsig) ->
ExpressionStep p target st st1 (normal_step_v (Ref obj)) ->
FieldUpdateCheck p loc st1 ->
ExpressionStep p expr st1 st2 (normal_step_v v) ->
Heap.typeof st2@h obj = Some (Heap.ObjectObject cn um) ->
defined_field p cn fsig ->
assign_compatible p st2@h v (FIELDSIGNATURE.type (snd fsig)) ->
FieldUpdateAction p loc v st2 = st3 ->
st' = st3[h:= Heap.update st2@h loc v] ->
ExpressionStep p e st st' (normal_step_v v)
Method call: target.msig(params)
| method_vcall_ok:
forall e st st1 st2 st3 st_c st_c' st' fr_c1 msig
o cn um this ps psnv psv v cn' m' c' b body,
e = method msig (Some o) ps ->
ExpressionStep p o st st1 (normal_step_v (Ref this)) ->
Heap.typeof st1@h this = Some (Heap.ObjectObject cn um) ->
lookup p cn (snd msig) (cn' , m') ->
PROG.class p cn = Some c' ->
ListSteps p ps st1 st2 psnv ->
psv = nv2v psnv ->
length psv = length psnv ->
fr_c1 = NewFrame m' (lv2params m' ((Ref this)::psv)) st2 ->
st3 = st2[fr:=fr_c1] ->
MethodCallAction p c' m' st3 = st_c ->
METHOD.body m' = Some body ->
STATEMENT.type (METHODBODY.compound body) = Compound b ->
BlockStep p m' b st_c st_c' normal_step ->
Normal (Some v) = Frame.ret st_c'@fr ->
MethodReturnAction p st_c' st2 = st' ->
ExpressionStep p e st st' (normal_step_v v)
forall e st st1 st2 st3 st_c st_c' st' fr_c1 msig
o cn um this ps psnv psv v cn' m' c' b body,
e = method msig (Some o) ps ->
ExpressionStep p o st st1 (normal_step_v (Ref this)) ->
Heap.typeof st1@h this = Some (Heap.ObjectObject cn um) ->
lookup p cn (snd msig) (cn' , m') ->
PROG.class p cn = Some c' ->
ListSteps p ps st1 st2 psnv ->
psv = nv2v psnv ->
length psv = length psnv ->
fr_c1 = NewFrame m' (lv2params m' ((Ref this)::psv)) st2 ->
st3 = st2[fr:=fr_c1] ->
MethodCallAction p c' m' st3 = st_c ->
METHOD.body m' = Some body ->
STATEMENT.type (METHODBODY.compound body) = Compound b ->
BlockStep p m' b st_c st_c' normal_step ->
Normal (Some v) = Frame.ret st_c'@fr ->
MethodReturnAction p st_c' st2 = st' ->
ExpressionStep p e st st' (normal_step_v v)
Allocate new object: o = new t
| new_object_ok:
forall e o st st' st1 h' cn um,
e = new (ReferenceType (TypeDefType cn um)) ->
Heap.new st@h p (Heap.ObjectObject cn um) = Some (o , h') ->
NewObjectAction p o st = st1 ->
st' = st1[h:= h'] ->
ExpressionStep p e st st' (normal_step_v (Ref o))
forall e o st st' st1 h' cn um,
e = new (ReferenceType (TypeDefType cn um)) ->
Heap.new st@h p (Heap.ObjectObject cn um) = Some (o , h') ->
NewObjectAction p o st = st1 ->
st' = st1[h:= h'] ->
ExpressionStep p e st st' (normal_step_v (Ref o))
ListSteps evaluate a whole list of expressions, used in method calls, circular dependency
with ListSteps (p : Program): list Expression -> State.t -> State.t -> list StepValue -> Prop :=
| ListSteps_nil:
forall st st',
st = st' ->
ListSteps p nil st st' nil
| ListSteps_cons_ok:
forall e le elist st st1 st' v lr ,
elist = e::le ->
ExpressionStep p e st st1 (normal_step_v v) ->
ListSteps p le st1 st' lr ->
ListSteps p elist st st' ((normal_step_v v)::lr)
| ListSteps_nil:
forall st st',
st = st' ->
ListSteps p nil st st' nil
| ListSteps_cons_ok:
forall e le elist st st1 st' v lr ,
elist = e::le ->
ExpressionStep p e st st1 (normal_step_v v) ->
ListSteps p le st1 st' lr ->
ListSteps p elist st st' ((normal_step_v v)::lr)
Evaluation function for statements
Expression-Statement
| expr_stmt_ok : forall st st' v e,
forall m b,
statement_at m (Frame.pc st@fr) = Some (ExprStmt e) ->
ExpressionStep p e st st' (normal_step_v v) ->
StatementStep p m b st st' normal_step
forall m b,
statement_at m (Frame.pc st@fr) = Some (ExprStmt e) ->
ExpressionStep p e st st' (normal_step_v v) ->
StatementStep p m b st st' normal_step
Evaluation of a block, sequencial composition
If there is a next instruction, do sequencial composition
| BlockStep_ok_next: forall m b pc' st st1 st' fr2 ,
BLOCK.next b (Frame.pc st@fr) = Some pc' ->
StatementStep p m b st st1 normal_step ->
fr2 = Frame.set_pc st1@fr pc' ->
BlockStep p m b st1[fr:=fr2] st' normal_step ->
BlockStep p m b st st' normal_step
BLOCK.next b (Frame.pc st@fr) = Some pc' ->
StatementStep p m b st st1 normal_step ->
fr2 = Frame.set_pc st1@fr pc' ->
BlockStep p m b st1[fr:=fr2] st' normal_step ->
BlockStep p m b st st' normal_step
Last statement in block, just evaluate statement
| BlockStep_ok_last: forall m b st st' ,
BLOCK.next b (Frame.pc st@fr) = None ->
StatementStep p m b st st' normal_step ->
BlockStep p m b st st' normal_step.
Scheme expr_step_ind := Minimality for ExpressionStep Sort Prop
with expr_steps_ind := Minimality for ListSteps Sort Prop
with stmt_step_ind := Minimality for StatementStep Sort Prop
with block_step_ind := Minimality for BlockStep Sort Prop.
Combined Scheme mutual_ind from expr_step_ind, expr_steps_ind, stmt_step_ind, block_step_ind.
Theorem OpSem_deterministic:
forall p,
(forall e st st' r',
ExpressionStep p e st st' r' ->
forall st'' r'',
ExpressionStep p e st st'' r'' ->
st' = st'' /\ r' = r'')
/\
(forall l st st' r',
ListSteps p l st st' r' ->
forall st'' r'',
ListSteps p l st st'' r'' ->
st' = st'' /\ r' = r'')
/\
(forall m b st st' r',
StatementStep p m b st st' r' ->
forall st'' r'',
StatementStep p m b st st'' r'' ->
st' = st'' /\ r' = r'')
/\
(forall m b st st' r',
BlockStep p m b st st' r' ->
forall st'' r'',
BlockStep p m b st st'' r'' ->
st' = st'' /\ r' = r'').
Proof.
intro p.
apply mutual_ind; intros; simpl in *.
inversion H11; try (rewrite H12 in H; discriminate H).
subst.
inversion H12.
subst.
destruct H2 with st4 (normal_step_v (Ref obj0)); trivial.
inversion H0.
subst.
destruct H5 with st5 (normal_step_v v0); trivial.
inversion H9.
rewrite H in |- *.
tauto.
inversion H18; try (rewrite H19 in H; discriminate H).
subst.
inversion H19.
subst.
destruct H1 with st4 (normal_step_v (Ref this1)); trivial.
inversion H7.
subst.
destruct H6 with st5 psnv0; trivial.
subst.
rewrite H2 in H21.
inversion H21.
subst.
assert ((cn', m') = (cn'0, m'0)).
apply (lookup_deterministic p cn0 (snd msig0) (cn', m') (cn'0, m'0));
trivial.
inversion H.
subst.
rewrite H12 in H30; inversion H30; subst.
rewrite H13 in H31; inversion H31; subst.
rewrite H4 in H23; inversion H23; subst.
destruct H15 with st_c'0 normal_step; trivial.
subst.
rewrite <- H16 in H33; inversion H33; subst.
tauto.
inversion H3; try (rewrite H4 in H; discriminate H).
rewrite H4 in H.
inversion H.
subst.
rewrite H0 in H5; inversion H5; subst.
tauto.
inversion H0.
subst.
tauto.
discriminate H1.
inversion H4; try (rewrite <- H6 in H; discriminate H).
subst.
inversion H5.
subst.
destruct H1 with st2 (normal_step_v v0); trivial.
subst.
inversion H8.
subst.
destruct H3 with st'' lr0; trivial.
subst.
tauto.
inversion H2; try (rewrite H4 in H; discriminate H).
subst.
rewrite H3 in H; inversion H; subst.
destruct H1 with st'' (normal_step_v v0); trivial.
tauto.
inversion H5; try (rewrite H6 in H; discriminate H).
subst.
destruct H1 with st2 normal_step; trivial.
subst.
rewrite H6 in H; inversion H; subst.
destruct H4 with st'' normal_step; trivial.
tauto.
inversion H2; try (rewrite H3 in H; discriminate H).
subst.
destruct H1 with st'' normal_step; trivial.
tauto.
Qed.
End OperationalSemantics.
BLOCK.next b (Frame.pc st@fr) = None ->
StatementStep p m b st st' normal_step ->
BlockStep p m b st st' normal_step.
Scheme expr_step_ind := Minimality for ExpressionStep Sort Prop
with expr_steps_ind := Minimality for ListSteps Sort Prop
with stmt_step_ind := Minimality for StatementStep Sort Prop
with block_step_ind := Minimality for BlockStep Sort Prop.
Combined Scheme mutual_ind from expr_step_ind, expr_steps_ind, stmt_step_ind, block_step_ind.
Theorem OpSem_deterministic:
forall p,
(forall e st st' r',
ExpressionStep p e st st' r' ->
forall st'' r'',
ExpressionStep p e st st'' r'' ->
st' = st'' /\ r' = r'')
/\
(forall l st st' r',
ListSteps p l st st' r' ->
forall st'' r'',
ListSteps p l st st'' r'' ->
st' = st'' /\ r' = r'')
/\
(forall m b st st' r',
StatementStep p m b st st' r' ->
forall st'' r'',
StatementStep p m b st st'' r'' ->
st' = st'' /\ r' = r'')
/\
(forall m b st st' r',
BlockStep p m b st st' r' ->
forall st'' r'',
BlockStep p m b st st'' r'' ->
st' = st'' /\ r' = r'').
Proof.
intro p.
apply mutual_ind; intros; simpl in *.
inversion H11; try (rewrite H12 in H; discriminate H).
subst.
inversion H12.
subst.
destruct H2 with st4 (normal_step_v (Ref obj0)); trivial.
inversion H0.
subst.
destruct H5 with st5 (normal_step_v v0); trivial.
inversion H9.
rewrite H in |- *.
tauto.
inversion H18; try (rewrite H19 in H; discriminate H).
subst.
inversion H19.
subst.
destruct H1 with st4 (normal_step_v (Ref this1)); trivial.
inversion H7.
subst.
destruct H6 with st5 psnv0; trivial.
subst.
rewrite H2 in H21.
inversion H21.
subst.
assert ((cn', m') = (cn'0, m'0)).
apply (lookup_deterministic p cn0 (snd msig0) (cn', m') (cn'0, m'0));
trivial.
inversion H.
subst.
rewrite H12 in H30; inversion H30; subst.
rewrite H13 in H31; inversion H31; subst.
rewrite H4 in H23; inversion H23; subst.
destruct H15 with st_c'0 normal_step; trivial.
subst.
rewrite <- H16 in H33; inversion H33; subst.
tauto.
inversion H3; try (rewrite H4 in H; discriminate H).
rewrite H4 in H.
inversion H.
subst.
rewrite H0 in H5; inversion H5; subst.
tauto.
inversion H0.
subst.
tauto.
discriminate H1.
inversion H4; try (rewrite <- H6 in H; discriminate H).
subst.
inversion H5.
subst.
destruct H1 with st2 (normal_step_v v0); trivial.
subst.
inversion H8.
subst.
destruct H3 with st'' lr0; trivial.
subst.
tauto.
inversion H2; try (rewrite H4 in H; discriminate H).
subst.
rewrite H3 in H; inversion H; subst.
destruct H1 with st'' (normal_step_v v0); trivial.
tauto.
inversion H5; try (rewrite H6 in H; discriminate H).
subst.
destruct H1 with st2 normal_step; trivial.
subst.
rewrite H6 in H; inversion H; subst.
destruct H4 with st'' normal_step; trivial.
tauto.
inversion H2; try (rewrite H3 in H; discriminate H).
subst.
destruct H1 with st'' normal_step; trivial.
tauto.
Qed.
End OperationalSemantics.