Skip to content

Commit

Permalink
Merge pull request WebAssembly#34 from Huxpro/cfg-valid-restype
Browse files Browse the repository at this point in the history
[spec] fixed resultype typo in configuration validity
  • Loading branch information
rossberg authored Oct 17, 2019
2 parents d5a23e3 + 0deeecb commit ed85e2c
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions document/core/appendix/properties.rst
Original file line number Diff line number Diff line change
Expand Up @@ -370,17 +370,17 @@ Finally, :ref:`frames <syntax-frame>` are classified with *frame contexts*, whic
* The :ref:`store <syntax-store>` :math:`S` must be :ref:`valid <valid-store>`.

* Under no allowed return type,
the :ref:`thread <syntax-thread>` :math:`T` must be :ref:`valid <valid-thread>` with some :ref:`result type <syntax-resulttype>` :math:`[t^?]`.
the :ref:`thread <syntax-thread>` :math:`T` must be :ref:`valid <valid-thread>` with some :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.

* Then the configuration is valid with the :ref:`result type <syntax-resulttype>` :math:`[t^?]`.
* Then the configuration is valid with the :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.

.. math::
\frac{
\vdashstore S \ok
\qquad
S; \epsilon \vdashthread T : [t^?]
S; \epsilon \vdashthread T : [t^\ast]
}{
\vdashconfig S; T : [t^?]
\vdashconfig S; T : [t^\ast]
}
Expand All @@ -397,17 +397,17 @@ Finally, :ref:`frames <syntax-frame>` are classified with *frame contexts*, whic
* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with |CRETURN| set to :math:`\resulttype^?`.

* Under context :math:`C'`,
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with some type :math:`[] \to [t^?]`.
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with some type :math:`[] \to [t^\ast]`.

* Then the thread is valid with the :ref:`result type <syntax-resulttype>` :math:`[t^?]`.
* Then the thread is valid with the :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.

.. math::
\frac{
S \vdashframe F : C
\qquad
S; C,\CRETURN~\resulttype^? \vdashinstrseq \instr^\ast : [] \to [t^?]
S; C,\CRETURN~\resulttype^? \vdashinstrseq \instr^\ast : [] \to [t^\ast]
}{
S; \resulttype^? \vdashthread F; \instr^\ast : [t^?]
S; \resulttype^? \vdashthread F; \instr^\ast : [t^\ast]
}
Expand Down

0 comments on commit ed85e2c

Please sign in to comment.