-
- Downloads
Simplify module Complements and add separate compilation (#121)
* Simplify the theorems about preservation of specifications (section 2) There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand. Plus, the "liveness" and "safety" terminology wasn't very good. Replaced by two theorems: - transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors; - transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces. Added named definitions for properties of interest. Added more explanations. * Added theorems that talk about separate compilation (section 3) These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together.
Loading
Please register or sign in to comment