source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2796

Last change on this file since 2796 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 
1include "ERTLptr/ERTLptrToLTL.ma".
2include "ERTLptr/ERTLptr_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6
7definition 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
12axiom ERTLptrToLTL_ok :
13∀fix_comp : fixpoint_computer.
14∀colour : coloured_graph_computer.
15∀p_in : ertlptr_program.
16let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in
17(* what should we do with n? *)
18let 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.