On 10/11/2012 10:23 AM, Jonathan M Davis wrote:
but there _are_ cases where you can't have an invariant because of it.
Except that you could write the invariant to be inclusive of the .init state.
On 10/11/2012 10:23 AM, Jonathan M Davis wrote:
but there _are_ cases where you can't have an invariant because of it.
Except that you could write the invariant to be inclusive of the .init state.