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 | |
---|
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.