 Timestamp:
 Feb 27, 2012, 5:55:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1782 r1784 1579 1579 ] qed. 1580 1580 1581 (* 1581 definition soundly_labelled_fn : internal_function → Prop ≝ 1582 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n. 1583 1584 definition soundly_labelled_ge : genv → Prop ≝ 1585 λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f. 1586 1587 definition soundly_labelled_state : state → Prop ≝ 1588 λs. match s with 1589 [ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs 1590  Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn  External _ ⇒ True ] ∧ 1591 All ? (λf. soundly_labelled_fn (func f)) fs 1592  Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs 1593  Finalstate _ ⇒ True 1594 ]. 1595 1596 lemma steps_from_sound : ∀s. 1597 RTLabs_cost s = true → 1598 soundly_labelled_state s → 1599 ∃n. state_bound_on_steps_to_cost s n. 1600 * [ #f #fs #m #CS  #a #b #c #d #e #E normalize in E; destruct  #a #b #c #d #E normalize in E; destruct  #a #E normalize in E; destruct ] 1601 whd in ⊢ (% → ?); * #SLF #_ 1602 cases (SLF (next f) (next_ok f)) #n #B1 1603 %{n} % @B1 1604 qed. 1605 1582 1606 let corec make_label_diverges ge s 1583 1607 (trace: flat_trace io_out io_in ge s) 1608 (ORACLE: termination_oracle) 1584 1609 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1610 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1585 1611 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 1612 (STATE_SOUNDLY_LABELLED: soundly_labelled_state s) 1586 1613 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 1587 (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)1588 1614 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) 1589 : trace_label_diverges (RTLabs_status ge) s ≝ ? 1590 . 1591 *) 1615 (NOT_UNDEFINED: not_wrong … trace) 1616 (NOT_FINAL: RTLabs_is_final s = None ?) 1617 : ∃T:trace_label_diverges (RTLabs_status ge) s. True ≝ 1618 match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with 1619 [ ex_intro n B ⇒ 1620 match finite_segment ge s n trace ORACLE ENV_COSTLABELLED STATE_COSTLABELLED NO_TERMINATION NOT_UNDEFINED B NOT_FINAL 1621 return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True 1622 with 1623 [ fp_tal s s' T t ⇒ λSTATEMENT_COSTLABEL. 1624 match make_label_diverges ge s' t ORACLE ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?????? with 1625 [ ex_intro T' _ ⇒ 1626 ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I 1627 ] 1628  fp_tac s s' T t ⇒ λSTATEMENT_COSTLABEL. 1629 match t return λs',t. trace_any_call ? s s' → ∃T:trace_label_diverges (RTLabs_status ge) s. True 1630 with 1631 [ ft_step s' tr next EV t' ⇒ λT. 1632 match make_label_diverges ge next t' ORACLE ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?????? with 1633 [ ex_intro T' _ ⇒ 1634 ex_intro ?? (tld_base (RTLabs_status ge) s s' next (tlc_base … T STATEMENT_COSTLABEL) ?? T') ? 1635 ] 1636  _ ⇒ λT. ⊥ 1637 ] T 1638 ] STATEMENT_COSTLABEL 1639 ].
Note: See TracChangeset
for help on using the changeset viewer.