Changeset 1764


Ignore:
Timestamp:
Feb 27, 2012, 2:16:41 PM (7 years ago)
Author:
campbell
Message:

Terminating function preserve the property that the execution does not
go wrong.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1736 r1764  
    399399                 whd in H49:(??%??); @⊥ destruct
    400400               ]
     401] qed.
     402
     403lemma will_return_not_wrong : ∀ge,d,s,t,s',t'.
     404  ∀T:will_return ge d s t.
     405  not_wrong io_out io_in ge s t →
     406  will_return_end … T = ❬s', t'❭ →
     407  not_wrong io_out io_in ge s' t'.
     408#ge #d #s #t #s' #t' #T elim T
     409[ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
     410  [ inversion NW
     411    [ #H1 #H2 #H3 #H4 #H5 destruct
     412    | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
     413    ]
     414  | @E
     415  ]
     416| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
     417  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
     418  | @E
     419  ]
     420| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
     421  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
     422  | @E
     423  ]
     424| #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
     425  inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
    401426] qed.
    402427
     
    14821507  @(will_return_prepend … TERMINATES … TM1)
    14831508  cases (terminates … tlr) //
    1484 | (* FIXME: post-call not-wrong *)
     1509| @(will_return_not_wrong … TERMINATES)
     1510  [ @(still_not_wrong … EV) //
     1511  | cases (terminates … tlr) //
     1512  ]
    14851513| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
    14861514  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
Note: See TracChangeset for help on using the changeset viewer.