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