Changeset 2224
 Timestamp:
 Jul 20, 2012, 4:29:31 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2223 r2224 1919 1919 ] qed. 1920 1920 1921 (* 1921 lemma 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 1932 qed. 1933 1934 definition 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] ?. 1936 cases (init_state_is p s I) #b 1937 cases 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 1922 1944 theorem program_trace_exists : 1923 1945 termination_oracle → … … 1929 1951 1930 1952 ∀NOIO:exec_no_io … plain_trace. 1953 ∀NW:not_wrong … plain_trace. 1931 1954 1932 let flat_trace ≝ make_whole_flat_trace p s NOIO I in1955 let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in 1933 1956 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 1935 1959 #ORACLE #p #s #I 1936 1960 letin 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 1962 letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I) 1963 whd 1964 @(whole_structured_trace_exists (make_global p) p ? ORACLE) 1965 [ 3: @flat_trace  4: @I 1966  *: cases daemon 1967 ] qed. 1968 1944 1969 1945 1970 lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
Note: See TracChangeset
for help on using the changeset viewer.