Re: [xml-dev] Are there invariants in XML processing?

[Roger L Costello <costello@mitre.org>]

Hi Ken,

What is an invariant?

I will first give an example of an invariant and then a definition.

Example: Suppose you are working on a very old computer that does not support integer division. You are writing a program that, among other things, needs to divide x by y. Your program wants the quotient q and the remainder r. For example, if x = 7 and y = 2, then q = 3 and r = 1 (two goes into seven three times with a remainder of one).

One way to solve this division problem is through repeated subtraction. Store a copy of x into t ("t" for temp). Keep subtracting y from t until t is less than y. 

So there is a loop. Before the loop q is initialized to zero and each time through the loop q is incremented by 1. When the loop is completed q has the quotient and whatever remains in t is the remainder r.

Here's the cool thing: every time the loop is executed this expression must hold true:

    x = q * y + t

Further, that expression must hold true before the loop is executed, at the start of the loop, at the end of the loop, and after the loop. 

So we can pepper the code with this assertion:

    assert(x = q * y + t)

At any point, if the assertion fails, then there is a bug in the code.

In XSLT the assertion would be expressed as:
 
    <xsl:assert test="$x = $q * $y + $t" />

The expression (the relation) that must always hold true is called an "invariant."

Definition: an invariant is an expression/relation that must hold true throughout the course of processing.

How do invariants differ from constraints?

An XML Schema specifies a set of constraints. We may write an XML Schema for the input data and validate the input against the XML Schema. That is a static, before run-time, check on the input data. During processing the input data likely will be changed, twisted, contorted, and no longer conform to the XML Schema. 

So the constraints expressed in an XML Schema are static constraints. The constraint/relation expressed by an invariant is a dynamic constraint/relation.

At least, that's how I think of it. I hope others will correct any errors I may have made and add additional insights.

/Roger


-----Original Message-----
From: G. Ken Holman <gkholman@CraneSoftwrights.com> 
Sent: Sunday, May 1, 2022 9:45 AM
To: Rick Jelliffe <rjelliffe@allette.com.au>; xml-dev <xml-dev@lists.xml.org>
Subject: Re: [xml-dev] Are there invariants in XML processing?

Forgive me, but I'm trying to understand the use 
of the noun "invariant". This is the first I've 
seen it used, and it is being bandied about. 
Rick's post using it extensively is dated 2016, 
so I feel very much out of the loop.

Is an invariant any different than a constraint?

Does the use of this noun come from another discipline where the use is common?

When does it help the listener/reader to use the 
noun "invariant" rather than "constraint" or some other word?

Thanks for your patience with my questions ... I'm just curious.

. . . . . Ken

At 2022-05-01 14:08 +1000, Rick Jelliffe wrote:
>For a Schematron introduction to this, including 
>document invariants (fixed and co-occurrence) 
>and input/output invariants, and round-trip 
>invariants, see Six Kinds of Validation using 
>Schematron at 
><https://www.schematron.com/document/279.html>https://www.schematron.com/document/279.html
>
>For people interest in the practical theory of 
>invariants, Bertam Meyers' work on Design by 
>Contact still is a great place to start: he 
>couches it in functional terms of pre-condition, 
>invariant,  post-condition, which I think is 
>more systematic than just "invariants".
>
>For the example, the Schematron IO validation 
>(output to input) might be (roughly)
>
><sch:pattern 
>id="publicMilitaryIndicator-nullTransform" documents="'input.xml'">
>
>Â  Â  Â <sch:rule context="publicMilitaryIndicator">
>Â  Â  Â  Â  Â  Â  Â <sch:let 
>name="matching-output" value="myFunc:findMatchingRow(., 'output.xml')" />
>Â  Â  Â  Â  Â Â
>Â  Â  Â  Â  Â  Â  Â  <sch:assert test="TYPE = 
>'A' or TYPE = 'B' or TYPE = 'C'" 
>role="pre-condition" >Every 
>publicMilitaryIndicator input should have a 
>TYPEÂ  with value A, b, or C (i.e., Civil, Joint, Military)</sch:assert>
>
>Â  Â  Â  Â  Â  Â  Â Â Â <sch:assert 
>test="$matching-output/TYPE = 'A' or 
>$matching-output/TYPE = 'B' or 
>$matching-output/TYPE = 'C'" 
>role="post-condition" >Every 
>publicMilitaryIndicator output should have a 
>TYPEÂ  with value A, b, or C (i.e., Civil, Joint, Military)</sch:assert>
>
>Â  Â  Â Â Â  Â  Â  Â <sch:assert 
>test="$matching-output" role="invariant">Every 
>input publicMilitaryIndicator should have a matching output</sch:assert>
>
>Â  Â  Â  Â Â Â Â  Â Â <sch:assert 
>test="$matching-output/TYPE= ./TYPE" 
>role="invariant" >Every input 
>publicMilitaryIndicator TYPE value should be 
>carried through to the output</sch:assert>
>
></sch:rule></sch:pattern>
>
>Rick


--
Contact info, blog, articles, etc. http://www.CraneSoftwrights.com/x/ |
Check our site for free XML, XSLT, XSL-FO and UBL developer resources |
Streaming hands-on XSLT/XPath 2 training class @US$125 (5 hours free) |
Essays (UBL, XML, etc.) http://www.linkedin.com/today/author/gkholman |


_______________________________________________________________________

XML-DEV is a publicly archived, unmoderated list hosted by OASIS
to support XML implementation and development. To minimize
spam in the archives, you must subscribe before posting.

[Un]Subscribe/change address: http://www.oasis-open.org/mlmanage/
Or unsubscribe: xml-dev-unsubscribe@lists.xml.org
subscribe: xml-dev-subscribe@lists.xml.org
List archive: http://lists.xml.org/archives/xml-dev/
List Guidelines: http://www.oasis-open.org/maillists/guidelines.php