📝 Notice about subtleties of inversion semantics of ForStatement

docs/syrec_language_semantics.md

@@ -275,6 +275,39 @@ The parser will not report an overlap in the assignment due to the index of the
 
 - The value of the step size of a ForStatement cannot be defined as or evaluate to 0 to prevent an infinite loop.
 
+````{warning}
+
+Uncalling modules containing a _ForStatement_ could lead to unexpected index-out-of-range errors if one is not familiar with the semantics of how a _ForStatement_ or more specifically its value range is inverted, with the inversion semantics being inherited by SyReC from its reversible programming language predecessor Janus {cite:p}`yokoyama2007janus`.
+
+A loop (_ForStatement_) defined as {math}`for \ e_1 \ to \ e_2 \ step \ s \ do \ s_1, s_2, \dots, s_n \ rof`
+is inverted by inverting not only the sequence of statements in its loop body but also by inverting its value range thus the inversion of the given loop is equal to
+{math}`for \ e_2 \ to \ e_1 \ step \ s \ do \ {s_n}^{-1}, \dots, {s_2}^{-1}, {s_1}^{-1} \ rof`.
+
+The inversion result of the _ForStatement_ as well as its enclosing module `basicBitwiseIncr` is equal to the module `invrBasicBitwiseIncr` with both modules being shown in the example below:
+
+```text
+module basicBitwiseIncr(inout a(4), inout b(4))
+for $i = 0 to #a do
+  ++= a.$i;
+  --= b.$i
+rof
+
+// Inversion of basicBitwiseIncr equal to "uncall basicBitwiseIncr(a, b)"
+module invrBasicBitwiseIncr(inout a(4), inout b(4))
+for $i = #a to 0 do
+   ++= b.$i;
+   --= a.$i
+rof
+
+module main(inout a(4), inout b(4))
+ // An index-out-of-range error would be reported here due to the value range of the ForStatement of the uncalled module
+ // being inverted with the loop variable $i being initialized with #a instead of 0 in the inverted ForStatement thus the assignments
+ // ++= b.$i and --= a.$i would both result in an index-out-of-range error.
+ uncall basicBitwiseIncr(a, b)
+```
+
+````
+
 ### IfStatement
 
 - The components of an IfStatement will be referred to as _if <GUARD_CONDITION> then <TRUE_BRANCH> else <FALSE_BRANCH> fi <CLOSING_GUARD_CONDITION_. To be able to identify the matching guard condition for a closing guard condition, the expressions used to define both of these components must consist of the same characters (with an expression evaluating to the same value while consisting of different or additional characters not being considered equal). An example of an IfStatement violating this rule is the following: