 Timestamp:
 Sep 5, 2012, 1:36:19 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2322 r2323 84 84 will_return' stack_cost O (stack_after prefix) interesting = Some ? max_stack ∧ 85 85 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 *) 86 96 87 97 axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)).
Note: See TracChangeset
for help on using the changeset viewer.