Changeset 2323


Ignore:
Timestamp:
Sep 5, 2012, 1:36:19 PM (7 years ago)
Author:
campbell
Message:

Some correctness proof comments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2322 r2323  
    8484  will_return' stack_cost O (stack_after prefix) interesting = Some ? max_stack ∧
    8585  max_stack < max_allowed_stack.
     86
     87(* From measurable on Clight, we will end up with an RTLabs flat trace where
     88   we know that there are some m' and n' such that the prefix in Clight matches
     89   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
     90   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
     91   for those n' steps so that we can build a corresponding structured trace.
     92   
     93   "Equivalent" here means, in particular, that the observables will be the same,
     94   and those observables will include the stack space costs.
     95 *)
    8696
    8797axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)).
Note: See TracChangeset for help on using the changeset viewer.