• Robbert Krebbers's avatar
    Add non-deterministic expressions with side-effects. · e82cda6c
    Robbert Krebbers authored
    The following things have been changed in this revision:
    
    * We now give a small step semantics for expressions. The denotational semantics
      only works for side-effect free expressions.
    * Dynamically allocated memory through alloc and free is now supported.
    * The following expressions are added: assignment, function call, unary
      operators, conditional, alloc, and free.
    * Some customary induction schemes for expressions are proven.
    * The axiomatic semantics (and its interpretation) have been changed in order
      to deal with non-deterministic expressions.
    * We have added inversion schemes based on small inversions for the operational
      semantics. Inversions using these schemes are much faster.
    * We improved the statement preservation proof of the operational semantics.
    * We now use a variant of SsReflect's [by] and [done], instead of Coq's [now]
      and [easy]. The [done] tactic is much faster as it does not perform
      inversions.
    * Add theory, definitions and notations on vectors.
    * Separate theory on contexts.
    * Change [Arguments] declarations to ensure better unfolding.
    e82cda6c
option.v 6.54 KB