Changeset 1651


Ignore:
Timestamp:
Jan 23, 2012, 5:37:17 PM (6 years ago)
Author:
campbell
Message:

Start looking at non-terminating structured traces by defining soundness
of RTLabs labelling.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1638 r1651  
    714714   full version with non-termination we'll fail because calls and returns aren't
    715715   balanced.
     716 *)
     717
     718inductive inhabited (T:Type[0]) : Prop ≝
     719| witness : T → inhabited T.
     720
     721(* We also require that program's traces are soundly labelled: for any state
     722   in the execution, we can give a distance to a labelled state or termination.
    716723   
    717    The guardedness check will reject the recursive definition above; need to
    718    rearrange things so that this works properly.
     724   Note that this differs from the syntactic notions in earlier languages
     725   because it is a global property.  In principle, we would have a loop broken
     726   only by a call to a function (which necessarily has a label) and no local
     727   cost label.
    719728 *)
     729
     730let rec nth_state ge s
     731  (trace: flat_trace io_out io_in ge s)
     732  n
     733  on n : option state ≝
     734match n with
     735[ O ⇒ Some ? s
     736| S n' ⇒
     737  match trace with
     738  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
     739  | _ ⇒ None ?
     740  ]
     741].
     742
     743definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
     744λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
     745
     746lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
     747  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
     748  soundly_labelled_trace ge s' trace'.
     749#ge #s #tr #s' #EV #trace' #H
     750#n cases (H (S n)) #m #H' %{m} @H'
     751qed.
     752
     753(*
     754let corec make_label_diverges ge s
     755  (trace: flat_trace io_out io_in ge s)
     756  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     757  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
     758  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
     759  (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)
     760  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
     761  : trace_label_diverges (RTLabs_status ge) s ≝ ?
     762.
     763*)
Note: See TracChangeset for help on using the changeset viewer.