Adds validation for exception results.

document/core/appendix/properties.rst

@@ -58,8 +58,31 @@ Results
      S \vdashresult \TRAP : [t^\ast]
    }
 
-.. todo::
-   Add validation for exception results.
+
+:ref:`Results <syntax-result>` :math:`\val^\ast~(\THROWadm~\tagaddr)`
+.....................................................................
+
+* The :ref:`external value <syntax-externval>` :math:`\EVTAG~\tagaddr` must be :ref:`valid <valid-externval-tag>` with some :ref:`external type <syntax-externtype>` :math:`\ETTAG~\tagtype`.
+
+* Let :math:`[t^\ast]\to[t_0^\ast]` be the :ref:`tag type <syntax-tagtype>` |tagtype|.
+
+* Assert: due to :ref:`validation <valid-externval-tag>` the type sequence :math:`t_0^\ast` must be empty.
+
+* For each :ref:`value <syntax-val>` :math:`\val_i` in :math:`\val^\ast`:
+
+  * The value :math:`\val_i` must be :ref:`valid <valid-val>` with :ref:`value type <syntax-valtype>` :math:`t_i`.
+
+* Then the result is valid with :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]`, for any sequence :math:`{t'}^\ast` of :ref:`value types <syntax-valtype>`.
+
+
+.. math::
+   \frac{
+     S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t^\ast] \to []
+     \qquad
+     (S \vdashval \val : t)^\ast
+   }{
+     S \vdashresult \val^\ast~(\THROWadm~\tagaddr) : [{t'}^\ast]
+   }
 
 
 .. _module-context: