Changeset 2224


Ignore:
Timestamp:
Jul 20, 2012, 4:29:31 PM (7 years ago)
Author:
campbell
Message:

Proper whole program result in RTLabs/Traces

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2223 r2224  
    19191919] qed.
    19201920
    1921 (*
     1921lemma init_state_is : ∀p,s.
     1922  make_initial_state p = OK ? s →
     1923  𝚺b. match s with [ Callstate fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
     1924   | _ ⇒ False ].
     1925#p #s
     1926@bind_ok #m #Em
     1927@bind_ok #b #Eb
     1928@bind_ok #f #Ef
     1929#E whd in E:(??%%); destruct
     1930%{b} whd
     1931% // @Ef
     1932qed.
     1933
     1934definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_state (make_global p) ≝
     1935λp,s,I. mk_RTLabs_state (make_global p) s [init_state_is p s I] ?.
     1936cases (init_state_is p s I) #b
     1937cases s
     1938[ #f #fs #m *
     1939| #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
     1940| #rv #rr #fs #m *
     1941| #r *
     1942] qed.
     1943
    19221944theorem program_trace_exists :
    19231945  termination_oracle →
     
    19291951 
    19301952  ∀NOIO:exec_no_io … plain_trace.
     1953  ∀NW:not_wrong … plain_trace.
    19311954 
    1932   let flat_trace ≝ make_whole_flat_trace p s NOIO I in
     1955  let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in
    19331956 
    1934   trace_whole_program_exists (RTLabs_status (make_global p)) s.
     1957  trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
     1958
    19351959#ORACLE #p #s #I
    19361960letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
    1937 #NOIO
    1938 letin flat_trace ≝ (make_whole_flat_trace p s NOIO I)
    1939 whd
    1940 @(whole_structured_trace_exists … flat_trace)
    1941 //
    1942 [ whd
    1943 *)
     1961#NOIO #NW
     1962letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
     1963whd
     1964@(whole_structured_trace_exists (make_global p) p ? ORACLE)
     1965[ 3: @flat_trace | 4: @I
     1966| *: cases daemon
     1967] qed.
     1968
    19441969
    19451970lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
Note: See TracChangeset for help on using the changeset viewer.