source: src/ASM/AssemblyAxiom.ma @ 3341

Last change on this file since 3341 was 3096, checked in by tranquil, 7 years ago

preliminary work on closing correctness.ma

File size: 1.5 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "ASM/Interpret2.ma".
16include "ASM/Policy.ma".
17include "common/StatusSimulation.ma".
18
19axiom assembly_ok :
20∀p_in : pseudo_assembly_program.
21∀sigma_pol.
22jump_expansion' p_in = Some ? sigma_pol →
23let sigma ≝ λx.\fst sigma_pol x in
24let policy ≝ λx.\snd sigma_pol x in
25let p_out ≝ pi1 ?? (assembly p_in sigma policy) in
26let init_in ≝ initialise_status … p_in in
27let init_out ≝ initialise_status … (cm p_out) in
28∃[1]R.
29  status_simulation_with_init
30    (ASM_status p_in sigma policy)
31    (OC_abstract_status p_out)
32    R init_in init_out.
33
34
Note: See TracBrowser for help on using the repository browser.