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
