Skip to content

Commit

Permalink
Merge pull request #1641 from michaelhkay/1554-formal-specification-h…
Browse files Browse the repository at this point in the history
…eading

1554-change-formal-specification-heading
  • Loading branch information
ndw authored Dec 10, 2024
2 parents 64262c2 + b7fae33 commit 340d25e
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 10 deletions.
24 changes: 15 additions & 9 deletions specifications/xpath-functions-40/src/xpath-functions.xml
Original file line number Diff line number Diff line change
Expand Up @@ -620,33 +620,39 @@ for transition to Proposed Recommendation. </p>'>
</div3>

<div3 id="id-function-signatures-formal-specification">
<head>Formal Specification</head>
<head>Formal Equivalents</head>

<p>Some functions supplement the prose rules with a formal specification that describes the effect
<p>Some functions supplement the prose rules with a more formal specification that describes the effect
of the function in terms of an equivalent XPath or XQuery implementation. This is intended to take
precedence over the prose rules in the event of any conflict; however, both sections are intended
to be complete and not to rely on each other.</p>

<p>In writing the formal specifications, a number of guidelines have been followed:</p>
<p>In writing the formal equivalents, a number of guidelines have been followed:</p>

<olist>
<item><p>Where the equivalent code calls other functions, these should either be primitives
defined in the data model specification (see <bibref ref="xpath-datamodel-31"/>), or
functions that themselves have a formal specification; and the dependencies should not
functions that themselves have a formal equivalent; and the dependencies should not
be circular.</p></item>
<item><p>There should be minimal reliance on XPath or XQuery language features.
Although no attempt has been made to precisely define a core set of language constructs,
the specifications try to avoid relying on features other than function calls
and a few basic operators including the comma operator, equality testing, and
simple integer arithmetic.</p></item>
<item><p>There is no suggestion that the formal equivalent is a practical
implementation; in many cases it might have very poor performance.</p></item>
<item><p>In some cases the formal equivalent does not attempt to replicate
correct behavior in error cases; if so, this is always clearly stated.</p></item>
<item><p>The formal equivalent will always produce a conformant result for the
function, but in some cases this will not be the only possible conformant result.</p></item>
</olist>

<ednote><edtext>This worthy intent is not yet fully achieved; for example there are
formal specifications that invoke fn:atomic-equal.</edtext></ednote>

<p>There is no attempt to write formal specifications for functions that have complex logic
<p>There is no attempt to write formal equivalents for functions that have complex logic
(such as <code>fn:format-number</code>) or dependencies (such as <code>fn:doc</code>); the aim
of the formal specifications is to define as rigorously as possible a platform of basic
of the formal equivalents is to define as rigorously as possible a platform of basic
functionality that can be used as a solid foundation for more complex features.</p>


Expand Down Expand Up @@ -7639,12 +7645,12 @@ return <table>
<p>There is one exception to this rule: for convenience, the notation <code>{}</code> is used to represent
an empty map, in preference to a call on <code>dm:empty-map()</code>.</p>

<p>The formal specifications are not intended to provide a realistic way of implementating the
<p>The formal equivalents are not intended to provide a realistic way of implementating the
functions (in particular, any real implementation might be expected to implement <code>map:get</code>
and <code>map:put</code> much more efficiently). They do, however, provide a framework that allows
the correctness of a practical implementation to be verified.</p>

<ednote><edtext>TODO: as yet there is no formal specification of <code>map:find()</code>.</edtext></ednote>
<ednote><edtext>TODO: as yet there is no formal equivalent for <code>map:find()</code>.</edtext></ednote>
</div2>

<div2 id="map-functions">
Expand Down Expand Up @@ -9271,7 +9277,7 @@ return <table>
<p>There is one exception to this rule: for convenience, the notation <code>[]</code> is used to represent
an empty array, in preference to a call on <code>dm:empty-array()</code>.</p>

<p>The formal specifications are not intended to provide a realistic way of implementating the
<p>The formal equivalents are not intended to provide a realistic way of implementating the
functions (in particular, any real implementation might be expected to implement <code>array:get</code>
much more efficiently). They do, however, provide a framework that allows
the correctness of a practical implementation to be verified.</p>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@
</gitem>
<xsl:if test="$fspec/fos:equivalent">
<gitem>
<label>Formal Specification</label>
<label>Formal Equivalent</label>
<def>
<xsl:copy-of select="$fspec/fos:eqivalent/(@diff, @at)"/>
<xsl:apply-templates select="$fspec/fos:equivalent"/>
Expand Down

0 comments on commit 340d25e

Please sign in to comment.