Last change
on this file since 2832 was
2796,
checked in by tranquil, 7 years ago

 added global notation for existence in Type[1] (\exists[1] x.P)
 in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
 in joint_semantics, moved out and around some parameters in primitive semantics functions
 fixed all back end semantics
 added skeleton files for single passes correctness proofs

File size:
778 bytes

Line  

1  include "ERTLptr/ERTLptrToLTL.ma". 

2  include "ERTLptr/ERTLptr_semantics.ma". 

3  include "LTL/LTL_semantics.ma". 

4  include "joint/Traces.ma". 

5  include "common/StatusSimulation.ma". 

6  

7  definition stacksizes_from_model : stack_cost_model → (ident → option ℕ) ≝ 

8  λm,id.find ?? 

9  (λid_stack.let 〈id', stack〉 ≝ id_stack in 

10  if id' == id then Some ? stack else None ?) m. 

11  

12  axiom ERTLptrToLTL_ok : 

13  ∀fix_comp : fixpoint_computer. 

14  ∀colour : coloured_graph_computer. 

15  ∀p_in : ertlptr_program. 

16  let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in 

17  (* what should we do with n? *) 

18  let stacksizes ≝ stacksizes_from_model m in 

19  ∃[1] R. 

20  status_simulation 

21  (joint_status ERTLptr_semantics p_in stacksizes) 

22  (joint_status LTL_semantics p_out stacksizes) 

23  R. 

Note: See
TracBrowser
for help on using the repository browser.