Recently `member_env` was simplified in the object model, and the
corresponding changes should be done in the operational semantics.
Additionally, the existence theorem now can be fully proven.
Change-Id: I30f86bd5d7e9b89eefc02fd51d928a9af139eee1
Reviewed-on: https://dart-review.googlesource.com/9341
Reviewed-by: Samir Jindel <sjindel@google.com>
The changes in the object model that introduce getters are reflected in
`value_of_type`, `step`, and `configuration_wf` relationships. Additionally,
the program well-formedness hypothesis is updated, so that it uses `lib_to_env`
function defined in the object model. A few other well-formedness hypotheses
are added. The existence proof for the next configuration is adjusted.
Change-Id: I14ca8aac5830a6ea0fc96f3f37818fdda3fa2c07
Reviewed-on: https://dart-review.googlesource.com/8880
Reviewed-by: Samir Jindel <sjindel@google.com>
Previously, we inferred the return type of statements in a way that made it
impossible to prove the statement typing consistency. Now, we use just the
stated return type for checking statements.
The proofs of statement typing are complete, except for one result generalizing
the expression typing consistency result to multiple variables changing; this
result is obvious to see directly from the provided lemmas but very tedious to
prove in Coq.
Bug:
Change-Id: I0bbcfb613df7510015f278fa85021ba0b3e57503
Reviewed-on: https://dart-review.googlesource.com/9020
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
* The definition of the well-formedness property for
configurations is added.
* The theorem that states that the abstract CESK-machine can
make one transition step from any well-formed configuration
is defined and proven.
* Execution of a variable declaration statement is added to
the operational semantics formalization with all necessary
changes (one new eval configuration, three new transition
rules).
* Some auxiliary theorems are added. One of them states that
any runtime value has its method bodies in the function
environment.
Change-Id: I95f233a4db498ce0df76983d9e605c3c263100bb
Reviewed-on: https://dart-review.googlesource.com/7266
Reviewed-by: Samir Jindel <sjindel@google.com>
Dmitry Stefantsov